Theorems · Theorem · category theory

CategoryTheory.SmallObject.SuccStruct.Iteration.mk.inj

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  {inst_1 : LinearOrder J} {inst_2 : SuccOrder J} {inst_3 : OrderBot J}
  {inst_4 : CategoryTheory.Limits.HasIterationOfShape J C} {inst_5 : WellFoundedLT J} {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iic j)) C} {obj_bot : F.obj ⟨⊥, ⋯⟩ = Φ.X₀}
  {arrowSucc_eq :
    ∀ (i : J) (hi : i < j), CategoryTheory.SmallObject.SuccStruct.arrowSucc F i hi = Φ.toSuccArrow (F.obj ⟨i, ⋯⟩)}
  {arrowMap_limit :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i),
      CategoryTheory.SmallObject.SuccStruct.arrowMap F k i ⋯ hij =
        CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT F hij) hi k hk}
  {F_1 : CategoryTheory.Functor (↑(Set.Iic j)) C} {obj_bot_1 : F_1.obj ⟨⊥, ⋯⟩ = Φ.X₀}
  {arrowSucc_eq_1 :
    ∀ (i : J) (hi : i < j), CategoryTheory.SmallObject.SuccStruct.arrowSucc F_1 i hi = Φ.toSuccArrow (F_1.obj ⟨i, ⋯⟩)}
  {arrowMap_limit_1 :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i),
      CategoryTheory.SmallObject.SuccStruct.arrowMap F_1 k i ⋯ hij =
        CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT F_1 hij) hi k hk},
  { F := F, obj_bot := obj_bot, arrowSucc_eq := arrowSucc_eq, arrowMap_limit := arrowMap_limit } =
      { F := F_1, obj_bot := obj_bot_1, arrowSucc_eq := arrowSucc_eq_1, arrowMap_limit := arrowMap_limit_1 } →
    F = F_1

Defined in

Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Cited by

1 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound