Theorems · Inductive type · category theory

CategoryTheory.IsCardinalLocallyPresentable

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

Given a regular cardinal κ, a category C is κ-locally presentable if it is cocomplete and admits a (small) family G : ι → C of κ-presentable objects such that any object identifies as a κ-filtered colimit of these objects.

Defined in

Mathlib.CategoryTheory.Presentable.LocallyPresentable

Cited by

7 results in Mathlib

Foundations

Depth 20 from the axioms · uses Quot.sound

Assumes

CategoryTheory.CategoryFact