Theorems · Inductive type · category theory

CategoryTheory.HasCardinalFilteredGenerator

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

The property that a category C and a regular cardinal κ satisfy P.IsCardinalFilteredGenerators κ for a suitable essentially small P : ObjectProperty C.

Defined in

Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Cited by

9 results in Mathlib

Foundations

Depth 20 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryFact