Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {I : CategoryTheory.MorphismProperty C} {κ : Cardinal.{w}}
  {inst_1 : Fact κ.IsRegular} {inst_2 : OrderBot κ.ord.ToType} [self : I.IsCardinalForSmallObjectArgument κ]
  {A B X Y : C} (i : A ⟶ B),
  I i →
    ∀ (f : X ⟶ Y) (hf : HomotopicalAlgebra.RelativeCellComplex (fun x => I.homFamily) f),
      CategoryTheory.Limits.PreservesColimit hf.F (CategoryTheory.coyoneda.obj (Opposite.op A))

Defined in

Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument