Uniqueness of morphisms in the category of iterations of functors #
Given a functor Φ : C ⥤ C and a natural transformation ε : 𝟭 C ⟶ Φ,
we show in this file that there exists a unique morphism
between two arbitrary objects in the category Functor.Iteration ε j
when j : J and J is a well orderered set.
def
CategoryTheory.Functor.Iteration.Hom.mkOfBot
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
(iter₁ iter₂ : CategoryTheory.Functor.Iteration ε ⊥)
:
iter₁ ⟶ iter₂
The (unique) morphism between two objects in Iteration ε ⊥
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTransApp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{i : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε (Order.succ i)}
(hi : ¬IsMax i)
(φ : iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
(k : J)
(hk : k ≤ Order.succ i)
:
iter₁.F.obj ⟨k, hk⟩ ⟶ iter₂.F.obj ⟨k, hk⟩
Auxiliary definition for mkOfSucc.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTransApp_eq_of_le
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{i : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε (Order.succ i)}
(hi : ¬IsMax i)
(φ : iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
(k : J)
(hk : k ≤ i)
:
CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTransApp hi φ k ⋯ = φ.natTrans.app ⟨k, hk⟩
@[simp]
theorem
CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTransApp_succ_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]
[OrderBot J]
[SuccOrder J]
{i : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε (Order.succ i)}
(hi : ¬IsMax i)
(φ : iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
:
CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTransApp hi φ (Order.succ i) ⋯ = CategoryTheory.CategoryStruct.comp (iter₁.isoSucc i ⋯).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (φ.natTrans.app ⟨i, ⋯⟩) Φ) (iter₂.isoSucc i ⋯).inv)
noncomputable def
CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTrans
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{i : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε (Order.succ i)}
(hi : ¬IsMax i)
(φ : iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
:
iter₁.F ⟶ iter₂.F
Auxiliary definition for mkOfSucc.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTrans_app
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{i : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε (Order.succ i)}
(hi : ¬IsMax i)
(φ : iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
(x✝ : ↑(Set.Iic (Order.succ i)))
:
(CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTrans hi φ).app x✝ = match x✝ with
| ⟨k, hk⟩ => CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTransApp hi φ k hk
noncomputable def
CategoryTheory.Functor.Iteration.Hom.mkOfSucc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{i : J}
(iter₁ iter₂ : CategoryTheory.Functor.Iteration ε (Order.succ i))
(hi : ¬IsMax i)
(φ : iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
:
iter₁ ⟶ iter₂
The (unique) morphism between two objects in Iteration ε (Order.succ i),
assuming we have a morphism between the truncations to Iteration ε i.
Equations
- CategoryTheory.Functor.Iteration.Hom.mkOfSucc iter₁ iter₂ hi φ = { natTrans := CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTrans hi φ, natTrans_app_zero := ⋯, natTrans_app_succ := ⋯ }
Instances For
def
CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{j : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j}
(φ : (i : J) → (hi : i < j) → iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
[WellFoundedLT J]
(hj : Order.IsSuccLimit j)
(i : J)
(hi : i ≤ j)
:
iter₁.F.obj ⟨i, hi⟩ ⟶ iter₂.F.obj ⟨i, hi⟩
Auxiliary definition for mkOfLimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp_eq_of_lt
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{j : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j}
(φ : (i : J) → (hi : i < j) → iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
[WellFoundedLT J]
(hj : Order.IsSuccLimit j)
(i : J)
(hi : i < j)
:
CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp φ hj i ⋯ = (φ i hi).natTrans.app ⟨i, ⋯⟩
theorem
CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp_naturality_top
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{j : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j}
(φ : (i : J) → (hi : i < j) → iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
[WellFoundedLT J]
(hj : Order.IsSuccLimit j)
(i : J)
(hi : i < j)
:
CategoryTheory.CategoryStruct.comp (iter₁.F.map (CategoryTheory.homOfLE ⋯))
(CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp φ hj j ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp φ hj i ⋯)
(iter₂.F.map (CategoryTheory.homOfLE ⋯))
def
CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTrans
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{j : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j}
(φ : (i : J) → (hi : i < j) → iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
[WellFoundedLT J]
(hj : Order.IsSuccLimit j)
:
iter₁.F ⟶ iter₂.F
Auxiliary definition for mkOfLimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTrans_app
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{j : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j}
(φ : (i : J) → (hi : i < j) → iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
[WellFoundedLT J]
(hj : Order.IsSuccLimit j)
(x✝ : ↑(Set.Iic j))
:
(CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTrans φ hj).app x✝ = match x✝ with
| ⟨k, hk⟩ => CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp φ hj k hk
def
CategoryTheory.Functor.Iteration.Hom.mkOfLimit
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{j : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j}
(φ : (i : J) → (hi : i < j) → iter₁.trunc ⋯ ⟶ iter₂.trunc ⋯)
[WellFoundedLT J]
(hj : Order.IsSuccLimit j)
:
iter₁ ⟶ iter₂
The (unique) morphism between two objects in Iteration ε j when j is a limit element,
assuming we have a morphism between the truncations to Iteration ε i for all i < j.
Equations
- CategoryTheory.Functor.Iteration.Hom.mkOfLimit φ hj = { natTrans := CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTrans φ hj, natTrans_app_zero := ⋯, natTrans_app_succ := ⋯ }
Instances For
instance
CategoryTheory.Functor.Iteration.Hom.instNonemptyHom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{j : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j}
[WellFoundedLT J]
:
Equations
- ⋯ = ⋯
noncomputable instance
CategoryTheory.Functor.Iteration.Hom.instUniqueHom
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
{j : J}
{iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j}
[WellFoundedLT J]
:
Equations
- CategoryTheory.Functor.Iteration.Hom.instUniqueHom = uniqueOfSubsingleton ⋯.some
noncomputable def
CategoryTheory.Functor.Iteration.iso
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
[WellFoundedLT J]
{j : J}
(iter₁ iter₂ : CategoryTheory.Functor.Iteration ε j)
:
iter₁ ≅ iter₂
The canonical isomorphism between two objects in the category Iteration ε j.
Equations
- iter₁.iso iter₂ = { hom := default, inv := default, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Functor.Iteration.iso_refl
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
[WellFoundedLT J]
{j : J}
(iter₁ : CategoryTheory.Functor.Iteration ε j)
:
iter₁.iso iter₁ = CategoryTheory.Iso.refl iter₁
theorem
CategoryTheory.Functor.Iteration.iso_trans
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{Φ : CategoryTheory.Functor C C}
{ε : CategoryTheory.Functor.id C ⟶ Φ}
{J : Type u}
[LinearOrder J]
[OrderBot J]
[SuccOrder J]
[WellFoundedLT J]
{j : J}
(iter₁ iter₂ iter₃ : CategoryTheory.Functor.Iteration ε j)
: