Theorems · Definition · category theory

CategoryTheory.IsCardinalPresentable

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

An object X in a category is κ-presentable (for κ a regular cardinal) when the functor Hom(X, _) preserves colimits indexed by κ-filtered categories.

Defined in

Mathlib.CategoryTheory.Presentable.Basic

Cited by

39 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFact