Transfinite iterations of a functor

In this file, given a functor Φ : C ⥤ C and a natural transformation ε : 𝟭 C ⟶ Φ, we shall define the transfinite iterations of Φ (TODO).

Given j : J where J is a well ordered set, we first introduce a category Iteration ε j. An object in this category consists of a functor F : Set.Iic j ⥤ C ⥤ C equipped with the data which makes it the ith-iteration of Φ for all i such that i ≤ j. Under suitable assumptions on C, we shall show that this category Iteration ε j is equivalent to the punctual category (TODO). In this file, we show that the there is at most one morphism between two objects. In SmallObject.Iteration.UniqueHom, we shall show that there does always exist a unique morphism between two objects (TODO). Then, we shall show the existence of an object (TODO). In these proofs, which are all done using transfinite induction, we have to treat three cases separately:

• the case j = ⊥;
• the case j is a successor;
• the case j is a limit element.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Functor.Iteration.mapSucc' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [Preorder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) [SuccOrder J] (i : J) (hi : i < j) : F.obj ⟨i, ⋯⟩ ⟶ F.obj ⟨Order.succ i, ⋯⟩

The map F.obj ⟨i, _⟩ ⟶ F.obj ⟨Order.succ i, _⟩ when F : Set.Iic j ⥤ C and i : J is such that i < j.

Equations

• CategoryTheory.Functor.Iteration.mapSucc' F i hi = F.map (CategoryTheory.homOfLE ⋯)

def CategoryTheory.Functor.Iteration.restrictionLT {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [Preorder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) : CategoryTheory.Functor (↑(Set.Iio i)) C

The functor Set.Iio i ⥤ C obtained by "restriction" of F : Set.Iic j ⥤ C when i ≤ j.

Equations

• CategoryTheory.Functor.Iteration.restrictionLT F hi = ⋯.functor.comp F

@[simp]

theorem CategoryTheory.Functor.Iteration.restrictionLT_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [Preorder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) (k : J) (hk : k < i) : (CategoryTheory.Functor.Iteration.restrictionLT F hi).obj ⟨k, hk⟩ = F.obj ⟨k, ⋯⟩

@[simp]

theorem CategoryTheory.Functor.Iteration.restrictionLT_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [Preorder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) {k₁ k₂ : ↑(Set.Iio i)} (φ : k₁ ⟶ k₂) : (CategoryTheory.Functor.Iteration.restrictionLT F hi).map φ = F.map (CategoryTheory.homOfLE ⋯)

def CategoryTheory.Functor.Iteration.coconeOfLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [Preorder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.Iteration.restrictionLT F hi)

Given F : Set.Iic j ⥤ C, i : J such that hi : i ≤ j, this is the cocone consisting of all maps F.obj ⟨k, hk⟩ ⟶ F.obj ⟨i, hi⟩ for k : J such that k < i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.Iteration.coconeOfLE_ι_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [Preorder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) (x✝ : ↑(Set.Iio i)) : (CategoryTheory.Functor.Iteration.coconeOfLE F hi).ι.app x✝ = match x✝ with | ⟨k, hk⟩ => F.map (CategoryTheory.homOfLE ⋯)

@[simp]

theorem CategoryTheory.Functor.Iteration.coconeOfLE_pt {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [Preorder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) : (CategoryTheory.Functor.Iteration.coconeOfLE F hi).pt = F.obj ⟨i, hi⟩

def CategoryTheory.Functor.Iteration.restrictionLE {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [Preorder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) : CategoryTheory.Functor (↑(Set.Iic i)) C

The functor Set.Iic i ⥤ C obtained by "restriction" of F : Set.Iic j ⥤ C when i ≤ j.

Equations

• CategoryTheory.Functor.Iteration.restrictionLE F hi = ⋯.functor.comp F

@[simp]

theorem CategoryTheory.Functor.Iteration.restrictionLE_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [Preorder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) (k : J) (hk : k ≤ i) : (CategoryTheory.Functor.Iteration.restrictionLE F hi).obj ⟨k, hk⟩ = F.obj ⟨k, ⋯⟩

@[simp]

theorem CategoryTheory.Functor.Iteration.restrictionLE_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [Preorder J] {j : J} (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) {k₁ k₂ : ↑(Set.Iic i)} (φ : k₁ ⟶ k₂) : (CategoryTheory.Functor.Iteration.restrictionLE F hi).map φ = F.map (CategoryTheory.homOfLE ⋯)

structure CategoryTheory.Functor.Iteration {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} (ε : CategoryTheory.Functor.id C ⟶ Φ) {J : Type u} [Preorder J] [OrderBot J] [SuccOrder J] (j : J) : Type (max (max u u_1) u_2)

The category of jth iterations of a functor Φ equipped with a natural transformation ε : 𝟭 C ⟶ Φ. An object consists of the data of all iterations of Φ for i : J such that i ≤ j (this is the field F). Such objects are equipped with data and properties which characterizes the iterations up to a unique isomorphism for the three types of elements: ⊥, successors, limit elements.

• F : CategoryTheory.Functor (↑(Set.Iic j)) (CategoryTheory.Functor C C)

  The data of all ith iterations for i : J such that i ≤ j.

• isoZero : self.F.obj ⟨⊥, ⋯⟩ ≅ CategoryTheory.Functor.id C

  The zeroth iteration is the identity functor.

• isoSucc : (i : J) → (hi : i < j) → self.F.obj ⟨Order.succ i, ⋯⟩ ≅ (self.F.obj ⟨i, ⋯⟩).comp Φ

  The iteration on a successor element is obtained by composition of the previous iteration with Φ.

• mapSucc'_eq : ∀ (i : J) (hi : i < j), CategoryTheory.Functor.Iteration.mapSucc' self.F i hi = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (self.F.obj ⟨i, ⋯⟩) ε) (self.isoSucc i hi).inv

  The natural map from an iteration to its successor is induced by ε.

• isColimit : (i : J) → Order.IsSuccLimit i → (hij : i ≤ j) → CategoryTheory.Limits.IsColimit (CategoryTheory.Functor.Iteration.coconeOfLE self.F hij)

  If i is a limit element, the ith iteration is the colimit of kth iterations for k < i.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Functor.Iteration.mapSucc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] (iter : CategoryTheory.Functor.Iteration ε j) (i : J) (hi : i < j) : iter.F.obj ⟨i, ⋯⟩ ⟶ iter.F.obj ⟨Order.succ i, ⋯⟩

For iter : Φ.Iteration.ε j, this is the map iter.F.obj ⟨i, _⟩ ⟶ iter.F.obj ⟨Order.succ i, _⟩ if i : J is such that i < j.

Equations

• iter.mapSucc i hi = CategoryTheory.Functor.Iteration.mapSucc' iter.F i hi

theorem CategoryTheory.Functor.Iteration.mapSucc_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] (iter : CategoryTheory.Functor.Iteration ε j) (i : J) (hi : i < j) : iter.mapSucc i hi = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft (iter.F.obj ⟨i, ⋯⟩) ε) (iter.isoSucc i hi).inv

structure CategoryTheory.Functor.Iteration.Hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] (iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j) : Type (max (max u u_1) u_2)

A morphism between two objects iter₁ and iter₂ in the category Φ.Iteration ε j of jth iterations of a functor Φ equipped with a natural transformation ε : 𝟭 C ⟶ Φ consists of a natural transformation natTrans : iter₁.F ⟶ iter₂.F which is compatible with the isomorphisms isoZero and isoSucc.

• natTrans : iter₁.F ⟶ iter₂.F

  A natural transformation iter₁.F ⟶ iter₂.F

• natTrans_app_zero : self.natTrans.app ⟨⊥, ⋯⟩ = CategoryTheory.CategoryStruct.comp iter₁.isoZero.hom iter₂.isoZero.inv
• natTrans_app_succ : ∀ (i : J) (hi : i < j), self.natTrans.app ⟨Order.succ i, ⋯⟩ = CategoryTheory.CategoryStruct.comp (iter₁.isoSucc i hi).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (self.natTrans.app ⟨i, ⋯⟩) Φ) (iter₂.isoSucc i hi).inv)

theorem CategoryTheory.Functor.Iteration.Hom.natTrans_app_zero_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j} (self : iter₁.Hom iter₂) {Z : CategoryTheory.Functor C C} (h : iter₂.F.obj ⟨⊥, ⋯⟩ ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.natTrans.app ⟨⊥, ⋯⟩) h = CategoryTheory.CategoryStruct.comp iter₁.isoZero.hom (CategoryTheory.CategoryStruct.comp iter₂.isoZero.inv h)

def CategoryTheory.Functor.Iteration.Hom.id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] (iter₁ : CategoryTheory.Functor.Iteration ε j) : iter₁.Hom iter₁

The identity morphism in the category Φ.Iteration ε j.

Equations

• CategoryTheory.Functor.Iteration.Hom.id iter₁ = { natTrans := CategoryTheory.CategoryStruct.id iter₁.F, natTrans_app_zero := ⋯, natTrans_app_succ := ⋯ }

@[simp]

theorem CategoryTheory.Functor.Iteration.Hom.id_natTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] (iter₁ : CategoryTheory.Functor.Iteration ε j) : (CategoryTheory.Functor.Iteration.Hom.id iter₁).natTrans = CategoryTheory.CategoryStruct.id iter₁.F

theorem CategoryTheory.Functor.Iteration.Hom.ext' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j} {f g : iter₁.Hom iter₂} (h : f.natTrans = g.natTrans) : f = g

def CategoryTheory.Functor.Iteration.Hom.comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {iter₁ iter₂ iter₃ : CategoryTheory.Functor.Iteration ε j} (f : iter₁.Hom iter₂) (g : iter₂.Hom iter₃) : iter₁.Hom iter₃

The composition of morphisms in the category Iteration ε j.

Equations

• f.comp g = { natTrans := CategoryTheory.CategoryStruct.comp f.natTrans g.natTrans, natTrans_app_zero := ⋯, natTrans_app_succ := ⋯ }

@[simp]

theorem CategoryTheory.Functor.Iteration.Hom.comp_natTrans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {iter₁ iter₂ iter₃ : CategoryTheory.Functor.Iteration ε j} (f : iter₁.Hom iter₂) (g : iter₂.Hom iter₃) : (f.comp g).natTrans = CategoryTheory.CategoryStruct.comp f.natTrans g.natTrans

instance CategoryTheory.Functor.Iteration.Hom.instCategory {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] : CategoryTheory.Category.{max (max u u_1) u_2, max (max u_2 u_1) u} (CategoryTheory.Functor.Iteration ε j)

Equations

• CategoryTheory.Functor.Iteration.Hom.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

instance CategoryTheory.Functor.Iteration.Hom.instSubsingletonHomOfWellFoundedLT {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u_2} {j : J} [PartialOrder J] [OrderBot J] [WellFoundedLT J] [SuccOrder J] {iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j} : Subsingleton (iter₁ ⟶ iter₂)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.Iteration.natTrans_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] (iter₁ : CategoryTheory.Functor.Iteration ε j) : (CategoryTheory.CategoryStruct.id iter₁).natTrans = CategoryTheory.CategoryStruct.id iter₁.F

@[simp]

theorem CategoryTheory.Functor.Iteration.natTrans_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {iter₁ iter₂ iter₃ : CategoryTheory.Functor.Iteration ε j} (φ : iter₁ ⟶ iter₂) (ψ : iter₂ ⟶ iter₃) : (CategoryTheory.CategoryStruct.comp φ ψ).natTrans = CategoryTheory.CategoryStruct.comp φ.natTrans ψ.natTrans

theorem CategoryTheory.Functor.Iteration.natTrans_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {iter₁ iter₂ iter₃ : CategoryTheory.Functor.Iteration ε j} (φ : iter₁ ⟶ iter₂) (ψ : iter₂ ⟶ iter₃) {Z : CategoryTheory.Functor (↑(Set.Iic j)) (CategoryTheory.Functor C C)} (h : iter₃.F ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ ψ).natTrans h = CategoryTheory.CategoryStruct.comp φ.natTrans (CategoryTheory.CategoryStruct.comp ψ.natTrans h)

theorem CategoryTheory.Functor.Iteration.natTrans_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j} (φ : iter₁ ⟶ iter₂) (i₁ i₂ : J) (h : i₁ ≤ i₂) (h' : i₂ ≤ j) : CategoryTheory.CategoryStruct.comp (iter₁.F.map (CategoryTheory.homOfLE h)) (φ.natTrans.app ⟨i₂, h'⟩) = CategoryTheory.CategoryStruct.comp (φ.natTrans.app ⟨i₁, ⋯⟩) (iter₂.F.map (CategoryTheory.homOfLE h))

theorem CategoryTheory.Functor.Iteration.natTrans_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j} (φ : iter₁ ⟶ iter₂) (i₁ i₂ : J) (h : i₁ ≤ i₂) (h' : i₂ ≤ j) {Z : CategoryTheory.Functor C C} (h✝ : iter₂.F.obj ⟨i₂, h'⟩ ⟶ Z) : CategoryTheory.CategoryStruct.comp (iter₁.F.map (CategoryTheory.homOfLE h)) (CategoryTheory.CategoryStruct.comp (φ.natTrans.app ⟨i₂, h'⟩) h✝) = CategoryTheory.CategoryStruct.comp (φ.natTrans.app ⟨i₁, ⋯⟩) (CategoryTheory.CategoryStruct.comp (iter₂.F.map (CategoryTheory.homOfLE h)) h✝)

def CategoryTheory.Functor.Iteration.eval {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} (ε : CategoryTheory.Functor.id C ⟶ Φ) {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {i : J} (hi : i ≤ j) : CategoryTheory.Functor (CategoryTheory.Functor.Iteration ε j) (CategoryTheory.Functor C C)

The evaluation functor Iteration ε j ⥤ C ⥤ C at i : J when i ≤ j.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.Iteration.eval_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} (ε : CategoryTheory.Functor.id C ⟶ Φ) {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {i : J} (hi : i ≤ j) {X✝ Y✝ : CategoryTheory.Functor.Iteration ε j} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Functor.Iteration.eval ε hi).map φ = φ.natTrans.app ⟨i, hi⟩

@[simp]

theorem CategoryTheory.Functor.Iteration.eval_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} (ε : CategoryTheory.Functor.id C ⟶ Φ) {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {i : J} (hi : i ≤ j) (iter : CategoryTheory.Functor.Iteration ε j) : (CategoryTheory.Functor.Iteration.eval ε hi).obj iter = iter.F.obj ⟨i, hi⟩

def CategoryTheory.Functor.Iteration.trunc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] (iter : CategoryTheory.Functor.Iteration ε j) {i : J} (hi : i ≤ j) : CategoryTheory.Functor.Iteration ε i

Given iter : Iteration ε j and i : J such that i ≤ j, this is the induced element in Iteration ε i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.Iteration.trunc_isoSucc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] (iter : CategoryTheory.Functor.Iteration ε j) {i : J} (hi : i ≤ j) (k : J) (hk : k < i) : (iter.trunc hi).isoSucc k hk = iter.isoSucc k ⋯

@[simp]

theorem CategoryTheory.Functor.Iteration.trunc_isoZero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] (iter : CategoryTheory.Functor.Iteration ε j) {i : J} (hi : i ≤ j) : (iter.trunc hi).isoZero = iter.isoZero

@[simp]

theorem CategoryTheory.Functor.Iteration.trunc_F {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] (iter : CategoryTheory.Functor.Iteration ε j) {i : J} (hi : i ≤ j) : (iter.trunc hi).F = CategoryTheory.Functor.Iteration.restrictionLE iter.F hi

def CategoryTheory.Functor.Iteration.truncFunctor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} (ε : CategoryTheory.Functor.id C ⟶ Φ) {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {i : J} (hi : i ≤ j) : CategoryTheory.Functor (CategoryTheory.Functor.Iteration ε j) (CategoryTheory.Functor.Iteration ε i)

The truncation functor Iteration ε j ⥤ Iteration ε i when i ≤ j.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.Iteration.truncFunctor_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} (ε : CategoryTheory.Functor.id C ⟶ Φ) {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {i : J} (hi : i ≤ j) (iter : CategoryTheory.Functor.Iteration ε j) : (CategoryTheory.Functor.Iteration.truncFunctor ε hi).obj iter = iter.trunc hi

@[simp]

theorem CategoryTheory.Functor.Iteration.truncFunctor_map_natTrans_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [Preorder J] [OrderBot J] [SuccOrder J] {iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j} (φ : iter₁ ⟶ iter₂) {i : J} (hi : i ≤ j) (k : J) (hk : k ≤ i) : ((CategoryTheory.Functor.Iteration.truncFunctor ε hi).map φ).natTrans.app ⟨k, hk⟩ = φ.natTrans.app ⟨k, ⋯⟩

theorem CategoryTheory.Functor.Iteration.Hom.congr_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} {j : J} [PartialOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] {iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j} (φ φ' : iter₁ ⟶ iter₂) (i : J) (hi : i ≤ j) : φ.natTrans.app ⟨i, hi⟩ = φ'.natTrans.app ⟨i, hi⟩