Theorems · Theorem · category theory

CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C) (j : κ.ord.ToType),
  CategoryTheory.Arrow.Hom.left (CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso I κ f j).hom =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.Arrow.mk
          (((CategoryTheory.SmallObject.iterationFunctor I κ).map (CategoryTheory.homOfLE ⋯)).app f)).left

Defined in

Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactOrderBotCategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument