Theorems · Definition · category theory

CategoryTheory.SmallObject.SuccStruct.extendToSucc

{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} →
            ¬IsMax j →
              (F : CategoryTheory.Functor (↑(Set.Iic j)) C) →
                {X : C} → (F.obj ⟨j, ⋯⟩ ⟶ X) → CategoryTheory.Functor (↑(Set.Iic (Order.succ j))) C

The extension to Set.Iic (Order.succ j) ⥤ C of a functor F : Set.Iic j ⥤ C, when we specify a morphism F.obj ⟨j, _⟩ ⟶ X.

Defined in

Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Cited by

10 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryLinearOrderSuccOrder