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).
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
jis a successor; - the case
jis 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 ⋯)
Instances For
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
Instances For
@[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₁ : ↑(Set.Iio i)}
{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)
:
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.
Instances For
@[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
Instances For
@[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₁ : ↑(Set.Iic i)}
{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 fori : Jsuch thati ≤ 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
iis a limit element, theith iteration is the colimit ofkth iterations fork < i.
Instances For
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}
[Preorder J]
[OrderBot J]
[SuccOrder 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}
{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
Instances For
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₁ : 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
- 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)
Instances For
@[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}
{j : J}
[Preorder J]
[OrderBot J]
[SuccOrder 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}
{j : J}
[Preorder J]
[OrderBot J]
[SuccOrder J]
{iter₁ : CategoryTheory.Functor.Iteration ε j}
{iter₂ : CategoryTheory.Functor.Iteration ε j}
(self : iter₁.Hom iter₂)
(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₁ : 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)
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 := ⋯ }
Instances For
@[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₁ : CategoryTheory.Functor.Iteration ε j}
{iter₂ : CategoryTheory.Functor.Iteration ε j}
{f : iter₁.Hom iter₂}
{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₁ : 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 := ⋯ }
Instances For
@[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₁ : 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
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]
:
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₁ : CategoryTheory.Functor.Iteration ε j}
{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₁ : CategoryTheory.Functor.Iteration ε j}
{iter₂ : CategoryTheory.Functor.Iteration ε j}
{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₁ : CategoryTheory.Functor.Iteration ε j}
{iter₂ : CategoryTheory.Functor.Iteration ε j}
{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₁ : CategoryTheory.Functor.Iteration ε j}
{iter₂ : CategoryTheory.Functor.Iteration ε j}
(φ : iter₁ ⟶ iter₂)
(i₁ : J)
(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₁ : CategoryTheory.Functor.Iteration ε j}
{iter₂ : CategoryTheory.Functor.Iteration ε j}
(φ : iter₁ ⟶ iter₂)
(i₁ : J)
(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)
:
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.
Instances For
@[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)
:
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.
Instances For
@[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)
:
The truncation functor Iteration ε j ⥤ Iteration ε i when i ≤ j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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₁ : CategoryTheory.Functor.Iteration ε j}
{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₁ : CategoryTheory.Functor.Iteration ε j)
(iter₂ : CategoryTheory.Functor.Iteration ε j)
(φ : iter₁ ⟶ iter₂)
(φ' : iter₁ ⟶ iter₂)
(i : J)
(hi : i ≤ j)
:
φ.natTrans.app ⟨i, hi⟩ = φ'.natTrans.app ⟨i, hi⟩