Theorems · Theorem · category theory

CategoryTheory.ObjectProperty.ColimitOfShape.isCardinalPresentable

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : C} {J : Type w}
  [inst_1 : CategoryTheory.SmallCategory J] (p : P.ColimitOfShape J X) {κ : Cardinal.{w}} [inst_2 : Fact κ.IsRegular],
  P ≤ CategoryTheory.isCardinalPresentable C κ →
    ∀ [CategoryTheory.LocallySmall.{w, v, u} C] (κ' : Cardinal.{w}) [inst_4 : Fact κ'.IsRegular],
      κ ≤ κ' → HasCardinalLT (CategoryTheory.Arrow J) κ' → CategoryTheory.IsCardinalPresentable X κ'

Defined in

Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.SmallCategoryFactCategoryTheory.LocallySmallFact