Theorems · Theorem · category theory

CategoryTheory.SmallObject.SuccStruct.extendToSucc_map

∀ {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₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j),
  (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ).map (CategoryTheory.homOfLE hi) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ i₁ ⋯).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE hi))
        (CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso hj F τ i₂ hi₂).inv)

Defined in

Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryLinearOrderSuccOrder