Theorems · Definition · category theory

CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        [inst_2 : SuccOrder J] →
          {j : J} →
            (hj : ¬IsMax j) →
              (F : CategoryTheory.Functor (↑(Set.Iic j)) C) →
                {X : C} →
                  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) →
                    (i : J) →
                      (hi : i ≤ j) →
                        (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ).obj ⟨i, ⋯⟩ ≅ F.obj ⟨i, hi⟩

The isomorphism (extendToSucc hj F τ).obj ⟨i, _⟩ ≅ F.obj i when i ≤ j

Defined in

Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryLinearOrderSuccOrder