Theorems · Inductive type · category theory

CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.ObjectProperty C → (κ : Cardinal.{w}) → [Fact κ.IsRegular] → Prop

The condition that P : ObjectProperty C consists of κ-presentable objects and that any object of C is a κ-filtered colimit of objects satisfying P. (This notion is particularly relevant when C is locally w-small and P is essentially w-small, see HasCardinalFilteredGenerators, which appears in the definitions of locally presentable and accessible categories.)

Defined in

Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Cited by

22 results in Mathlib

Foundations

Depth 20 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryFact