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 : { i // i ≤ 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). We shall study morphisms in this category, showing first that there is at most one morphism between two morphisms (done), and secondly, 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} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i ≤ j } C) [IsWellOrder J fun (x1 x2 : J) => x1 < x2] (i : J) (hi : i < j) : F.obj ⟨i, ⋯⟩ ⟶ F.obj ⟨wellOrderSucc i, ⋯⟩

The map F.obj ⟨i, _⟩ ⟶ F.obj ⟨wellOrderSucc i, _⟩ when F : { i // i ≤ 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} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i ≤ j } C) {i : J} (hi : i ≤ j) : CategoryTheory.Functor { k : J // k < i } C

The functor { k // k < i } ⥤ C obtained by "restriction" of F : { i // i ≤ 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} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i ≤ 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} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i ≤ j } C) {i : J} (hi : i ≤ j) {k₁ : { k : J // k < i }} {k₂ : { k : J // k < i }} (φ : k₁ ⟶ k₂) : (CategoryTheory.Functor.Iteration.restrictionLT F hi).map φ = F.map (CategoryTheory.homOfLE ⋯)

@[simp]

theorem CategoryTheory.Functor.Iteration.coconeOfLE_ι_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {J : Type u} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i ≤ j } C) {i : J} (hi : i ≤ j) : ∀ (x : { k : J // k < 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} [LinearOrder J] {j : J} (F : CategoryTheory.Functor { i : J // i ≤ j } C) {i : J} (hi : i ≤ j) : (CategoryTheory.Functor.Iteration.coconeOfLE F hi).pt = F.obj ⟨i, hi⟩

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

Given F : { i // i ≤ 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.

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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot 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 { i : J // i ≤ 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 ⟨wellOrderSucc 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) → [inst : IsWellOrderLimitElement i] → (hi : i ≤ j) → CategoryTheory.Limits.IsColimit (CategoryTheory.Functor.Iteration.coconeOfLE self.F hi)

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

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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} (self : CategoryTheory.Functor.Iteration ε j) (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 ε.

@[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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} (iter : CategoryTheory.Functor.Iteration ε j) (i : J) (hi : i < j) : iter.F.obj ⟨i, ⋯⟩ ⟶ iter.F.obj ⟨wellOrderSucc i, ⋯⟩

For iter : Φ.Iteration.ε j, this is the map iter.F.obj ⟨i, _⟩ ⟶ iter.F.obj ⟨wellOrderSucc 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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : 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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} (iter₁ : CategoryTheory.Functor.Iteration ε j) (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 ⟨wellOrderSucc i, ⋯⟩ = CategoryTheory.CategoryStruct.comp (iter₁.isoSucc i hi).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (self.natTrans.app ⟨i, ⋯⟩) Φ) (iter₂.isoSucc i hi).inv)

@[simp]

theorem CategoryTheory.Functor.Iteration.Hom.natTrans_app_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} (self : iter₁.Hom iter₂) : self.natTrans.app ⟨⊥, ⋯⟩ = CategoryTheory.CategoryStruct.comp iter₁.isoZero.hom iter₂.isoZero.inv

theorem CategoryTheory.Functor.Iteration.Hom.natTrans_app_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} (self : iter₁.Hom iter₂) (i : J) (hi : i < j) : self.natTrans.app ⟨wellOrderSucc 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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {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)

@[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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} (iter₁ : CategoryTheory.Functor.Iteration ε j) : (CategoryTheory.Functor.Iteration.Hom.id iter₁).natTrans = CategoryTheory.CategoryStruct.id iter₁.F

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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : 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 := ⋯ }

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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} {f : iter₁.Hom iter₂} {g : iter₁.Hom iter₂} (h : f.natTrans = g.natTrans) : f = g

theorem CategoryTheory.Functor.Iteration.Hom.ext'_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} {f : iter₁.Hom iter₂} {g : iter₁.Hom iter₂} : f = g ↔ f.natTrans = g.natTrans

@[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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} {iter₃ : CategoryTheory.Functor.Iteration ε j} (f : iter₁.Hom iter₂) (g : iter₂.Hom iter₃) : (f.comp g).natTrans = CategoryTheory.CategoryStruct.comp f.natTrans g.natTrans

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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} {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 := ⋯ }

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} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : 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.instSubsingletonHom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Φ : CategoryTheory.Functor C C} {ε : CategoryTheory.Functor.id C ⟶ Φ} {J : Type u} [LinearOrder J] [IsWellOrder J fun (x1 x2 : J) => x1 < x2] [OrderBot J] {j : J} {iter₁ : CategoryTheory.Functor.Iteration ε j} {iter₂ : CategoryTheory.Functor.Iteration ε j} : Subsingleton (iter₁ ⟶ iter₂)

Equations

• ⋯ = ⋯