Theorems · Definition · category theory

CategoryTheory.SmallObject.SuccStruct.Iteration.casesOn

{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} →
                    {motive : Φ.Iteration j → Sort u_1} →
                      (t : Φ.Iteration 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) →
                                  motive
                                    { F := F, obj_bot := obj_bot, arrowSucc_eq := arrowSucc_eq,
                                      arrowMap_limit := arrowMap_limit }) →
                          motive t

Defined in

Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryLinearOrderSuccOrderOrderBotCategoryTheory.Limits.HasIterationOfShapeWellFoundedLT