Functors

This file provides basic lemmas about Functor and Sequence constructions.

@[simp]

theorem QuasiBorelSpace.Sequence.Compose.eta {F✝ : Type u_1 → Type u_1} {S✝ : ℕ → Type u_1} {n✝ : ℕ} {x : Compose F✝ S✝ n✝} : { val := x.val } = x

@[simp]

theorem QuasiBorelSpace.Sequence.Compose.map_mk {F : Type u_1 → Type u_1} {S : ℕ → Type u_1} [Functor F] [Sequence S] {i j : ℕ} (h : i ≤ j) (x : F (S i)) : Sequence.map h { val := x } = { val := Functor.map (Sequence.map h) x }

@[simp]

theorem QuasiBorelSpace.Sequence.Compose.val_map {F : Type u_1 → Type u_1} {S : ℕ → Type u_1} [Functor F] [Sequence S] {i j : ℕ} (h : i ≤ j) (x : Compose F S i) : (Sequence.map h x).val = Functor.map (Sequence.map h) x.val

instance QuasiBorelSpace.Sequence.Iterate.instIsEmptyInternalOfNatNat {F : Type u_1 → Type u_1} : IsEmpty (Internal F 0)

instance QuasiBorelSpace.Sequence.Iterate.instSubsingletonInternalOfNatNat {F : Type u_1 → Type u_1} : Subsingleton (Internal F 0)

instance QuasiBorelSpace.Sequence.Iterate.instIsEmptyOfNatNat {F : Type u_1 → Type u_1} : IsEmpty (Iterate F 0)

instance QuasiBorelSpace.Sequence.Iterate.instSubsingletonOfNatNat {F : Type u_1 → Type u_1} : Subsingleton (Iterate F 0)

@[simp]

theorem QuasiBorelSpace.Sequence.Iterate.isHom_roll {F : Type u_1 → Type u_1} [Functor F] {n : ℕ} : IsHom roll

@[simp]

theorem QuasiBorelSpace.Sequence.Iterate.isHom_unroll {F : Type u_1 → Type u_1} [Functor F] {n : ℕ} : IsHom unroll

@[simp]

theorem QuasiBorelSpace.Sequence.Iterate.unroll_roll {F : Type u_1 → Type u_1} [Functor F] {n : ℕ} (x : F (Iterate F n)) : (roll x).unroll = x

@[simp]

theorem QuasiBorelSpace.Sequence.Iterate.roll_unroll {F : Type u_1 → Type u_1} [Functor F] {n : ℕ} (x : Iterate F (n + 1)) : roll x.unroll = x

theorem QuasiBorelSpace.Sequence.Iterate.unroll_inj {F : Type u_1 → Type u_1} [Functor F] {n : ℕ} {x y : Iterate F (n + 1)} (h : x.unroll = y.unroll) : x = y

theorem QuasiBorelSpace.Sequence.Iterate.roll_inj {F : Type u_1 → Type u_1} [Functor F] {n : ℕ} {x y : F (Iterate F n)} (h : roll x = roll y) : x = y

theorem QuasiBorelSpace.Sequence.Iterate.map_unroll {F : Type u_1 → Type u_1} [Functor F] {i j : ℕ} (h : i ≤ j) (x : Iterate F (i + 1)) : Functor.map (map h) x.unroll = (map ⋯ x).unroll

theorem QuasiBorelSpace.Sequence.Iterate.map_unroll' {F : Type u_1 → Type u_1} [Functor F] {i j : ℕ} (h : i + 1 ≤ j + 1) (x : Iterate F (i + 1)) : (map h x).unroll = Functor.map (map ⋯) x.unroll

theorem QuasiBorelSpace.Sequence.Iterate.roll_map {F : Type u_1 → Type u_1} [Functor F] {i j : ℕ} (h : i ≤ j) (x : F (Iterate F i)) : roll (Functor.map (map h) x) = map ⋯ (roll x)

@[simp]

theorem QuasiBorelSpace.Functor.Sum.toSum_inl {F G : Type u_1 → Type u_2} {a✝ : Type u_1} {x : F a✝} : (inl x).toSum = _root_.Sum.inl x

@[simp]

theorem QuasiBorelSpace.Functor.Sum.toSum_inr {F G : Type u_1 → Type u_2} {a✝ : Type u_1} {x : G a✝} : (inr x).toSum = _root_.Sum.inr x

@[simp]

theorem QuasiBorelSpace.Functor.Sum.isHom_inl {F G : Type u_2 → Type u_1} {A : Type u_2} [Functor F] [Functor G] [QuasiBorelSpace A] : IsHom inl

@[simp]

theorem QuasiBorelSpace.Functor.Sum.isHom_inr {F G : Type u_2 → Type u_1} {A : Type u_2} [Functor F] [Functor G] [QuasiBorelSpace A] : IsHom inr

@[simp]

theorem QuasiBorelSpace.Functor.Sum.map_inl {F G : Type u_1 → Type u_2} {A B : Type u_1} [Functor F] [Functor G] [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} {x : F A} (hf : IsHom f) : map f (inl x) = inl (map f x)

@[simp]

theorem QuasiBorelSpace.Functor.Sum.map_inr {F G : Type u_1 → Type u_2} {A B : Type u_1} [Functor F] [Functor G] [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} {x : G A} (hf : IsHom f) : map f (inr x) = inr (map f x)

@[simp]

theorem QuasiBorelSpace.Functor.Prod.map_mk {F G : Type u_1 → Type u_2} {A B : Type u_1} [Functor F] [Functor G] [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} (hf : IsHom f) (x : F A) (y : G A) : map f { fst := x, snd := y } = { fst := map f x, snd := map f y }

@[simp]

theorem QuasiBorelSpace.Functor.Prod.isHom_fst {F G : Type u_2 → Type u_1} {A : Type u_2} [Functor F] [Functor G] [QuasiBorelSpace A] : IsHom fst

@[simp]

theorem QuasiBorelSpace.Functor.Prod.isHom_snd {F G : Type u_2 → Type u_1} {A : Type u_2} [Functor F] [Functor G] [QuasiBorelSpace A] : IsHom snd

@[simp]

theorem QuasiBorelSpace.Functor.Prod.isHom_mk {F G : Type u_2 → Type u_1} {A : Type u_2} [Functor F] [Functor G] [QuasiBorelSpace A] : IsHom fun (x : F A × G A) => { fst := x.1, snd := x.2 }

@[simp]

theorem QuasiBorelSpace.Functor.Identity.map_mk {A B : Type u_1} [QuasiBorelSpace A] [QuasiBorelSpace B] {x : A} {f : A → B} (hf : IsHom f) : map f { val := x } = { val := f x }

@[simp]

theorem QuasiBorelSpace.Functor.Const.map_mk {A B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {C : Type u_1} {x : C} [QuasiBorelSpace C] (f : A → B) : map f { val := x } = { val := x }