Existence of the iteration of a successor structure

Given Φ : SuccStruct C, we show by transfinite induction that for any element j in a well ordered set J, the type Φ.Iteration j is nonempty.

def CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfBot {C : Type u_1} [Category.{u_2, u_1} C] (Φ : SuccStruct C) (J : Type u) [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] : Φ.Iteration ⊥

The obvious term in Φ.Iteration ε ⊥ that is given by Φ.X₀.

Equations

• CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfBot Φ J = { F := (CategoryTheory.Functor.const ↑(Set.Iic ⊥)).obj Φ.X₀, obj_bot := ⋯, arrowSucc_eq := ⋯, arrowMap_limit := ⋯ }

noncomputable def CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfSucc {C : Type u_1} [Category.{u_2, u_1} C] {Φ : SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] {j : J} (hj : ¬IsMax j) (iter : Φ.Iteration j) : Φ.Iteration (Order.succ j)

When j : J is not maximal, this is the extension in Φ.Iteration (Order.succ j) of any iter : Φ.Iteration j.

Equations

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

noncomputable def CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem {C : Type u_1} [Category.{u_2, u_1} C] {Φ : SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] {j : J} (iter : (i : J) → i < j → Φ.Iteration i) : Functor (↑(Set.Iio j)) C

Assuming j : J is a limit element and that we have ∀ (i : J), i < j → Φ.Iteration i, this is the inductive system Set.Iio j ⥤ C which sends ⟨i, _⟩ to (iter i _).F.obj ⟨i, _⟩.

Equations

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

@[simp]

theorem CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_map {C : Type u_1} [Category.{u_2, u_1} C] {Φ : SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] {j : J} (iter : (i : J) → i < j → Φ.Iteration i) {i₁ i₂ : ↑(Set.Iio j)} (f : i₁ ⟶ i₂) : (inductiveSystem iter).map f = (iter ↑i₁ ⋯).mapObj (iter ↑i₂ ⋯) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_obj {C : Type u_1} [Category.{u_2, u_1} C] {Φ : SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] {j : J} (iter : (i : J) → i < j → Φ.Iteration i) (i : ↑(Set.Iio j)) : (inductiveSystem iter).obj i = (iter ↑i ⋯).F.obj ⟨↑i, ⋯⟩

noncomputable def CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor {C : Type u_1} [Category.{u_2, u_1} C] {Φ : SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) : Functor (↑(Set.Iic j)) C

The extension of inductiveSystem iter to a functor Set.Iic j ⥤ C which sends the top element to the colimit of inductiveSystem iter.

Equations

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

theorem CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor_obj {C : Type u_1} [Category.{u_2, u_1} C] {Φ : SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) (i : J) (hi : i < j) {k : J} (iter' : Φ.Iteration k) (hk : i ≤ k) : (functor hj iter).obj ⟨i, ⋯⟩ = iter'.F.obj ⟨i, hk⟩

theorem CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor {C : Type u_1} [Category.{u_2, u_1} C] {Φ : SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) (h₂ : i₂ < j) : arrowMap (functor hj iter) i₁ i₂ h₁₂ ⋯ = Arrow.mk ((iter i₁ ⋯).mapObj (iter i₂ h₂) h₁₂ ⋯ ⋯ h₁₂)

theorem CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor_to_top {C : Type u_1} [Category.{u_2, u_1} C] {Φ : SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) (i : J) (hi : i < j) : arrowMap (functor hj iter) i j ⋯ ⋯ = Arrow.mk (Limits.colimit.ι (inductiveSystem iter) ⟨i, hi⟩)

noncomputable def CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit {C : Type u_1} [Category.{u_2, u_1} C] {Φ : SuccStruct C} {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] {j : J} (hj : Order.IsSuccLimit j) (iter : (i : J) → i < j → Φ.Iteration i) : Φ.Iteration j

When j is a limit element, this is the element in Φ.Iteration j that is constructed from elements in Φ.Iteration i for all i < j.

Equations

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

instance CategoryTheory.SmallObject.SuccStruct.Iteration.nonempty {C : Type u_1} [Category.{u_2, u_1} C] (Φ : SuccStruct C) {J : Type u} [LinearOrder J] [OrderBot J] [SuccOrder J] [WellFoundedLT J] [Limits.HasIterationOfShape J C] (j : J) : Nonempty (Φ.Iteration j)