Commit 2025-12-05 16:31 954f0771

View on Github →

feat(CategoryTheory): locally presentable categories and strong generators (#30241) Let C be category that is locally w-small and has colimits of size w. Then, C is locally κ-presentable iff it has a strong generator consisting of κ-presentable objects.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean

Created Mathlib/CategoryTheory/Presentable/StrongGenerator.lean

added theorem CategoryTheory.IsCardinalFilteredGenerator.of_isDense

added theorem CategoryTheory.IsCardinalFilteredGenerator.of_isDense_ι

added theorem CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator

added theorem CategoryTheory.IsCardinalLocallyPresentable.of_le

added theorem CategoryTheory.IsStrongGenerator.colimitsCardinalClosure_eq_isCardinalPresentable

added theorem CategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ι

added theorem CategoryTheory.ObjectProperty.colimitsCardinalClosure_le_isCardinalPresentable