Theorems · Theorem · category theory

CategoryTheory.SmallObject.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] [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 44 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryFactOrderBotCategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument