Theorems · Theorem · category theory

CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.IsCardinalLocallyPresentable C κ ↔
    ∃ P,
      ∃ (_ : CategoryTheory.ObjectProperty.Small.{w, v, u} P),
        P.IsStrongGenerator ∧ P ≤ CategoryTheory.isCardinalPresentable C κ

Defined in

Mathlib.CategoryTheory.Presentable.StrongGenerator

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactCategoryTheory.Limits.HasColimitsOfSizeCategoryTheory.LocallySmall