LocallyPresentable

📁 Source: Mathlib/CategoryTheory/Presentable/LocallyPresentable.lean

Statistics

Metric	Count
Definitions IsAccessibleCategory, IsCardinalAccessibleCategory, IsCardinalLocallyPresentable, IsFinitelyAccessibleCategory, IsLocallyFinitelyPresentable, IsLocallyPresentable	6
Theorems exists_cardinal, toHasCardinalFilteredColimits, toHasCardinalFilteredGenerator, toHasCardinalFilteredGenerator, toHasColimitsOfSize, exists_cardinal, instIsAccessibleCategoryOfIsLocallyPresentable, instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable, instIsPresentableOfIsAccessibleCategory	9
Total	15

CategoryTheory

Definitions

Name	Category	Theorems
IsAccessibleCategory 📖	CompData	2 math math: instIsAccessibleCategoryOfIsLocallyPresentable, Equivalence.isAccessibleCategory
IsCardinalAccessibleCategory 📖	CompData	4 math math: Adjunction.isCardinalAccessibleCategory, IsAccessibleCategory.exists_cardinal, Equivalence.isCardinalAccessibleCategory, instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable
IsCardinalLocallyPresentable 📖	CompData	7 math math: IsCardinalLocallyPresentable.iff_exists_isStrongGenerator, IsLocallyPresentable.exists_cardinal, Adjunction.isCardinalLocallyPresentable, Equivalence.isCardinalLocallyPresentable, IsCardinalLocallyPresentable.of_le, Presheaf.instIsCardinalLocallyPresentableFunctorOppositeOfHasPullbacks, MorphismProperty.isLocallyPresentable_isLocal
IsFinitelyAccessibleCategory 📖	MathDef	—
IsLocallyFinitelyPresentable 📖	MathDef	—
IsLocallyPresentable 📖	CompData	2 math math: Equivalence.isLocallyPresentable, Presheaf.instIsLocallyPresentableFunctorOppositeOfHasPullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsAccessibleCategoryOfIsLocallyPresentable 📖	mathematical	—	IsAccessibleCategory	—	IsLocallyPresentable.exists_cardinal instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable
instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable 📖	mathematical	—	IsCardinalAccessibleCategory	—	IsCardinalLocallyPresentable.toHasCardinalFilteredGenerator instHasCardinalFilteredColimitsOfHasColimitsOfSize IsCardinalLocallyPresentable.toHasColimitsOfSize
instIsPresentableOfIsAccessibleCategory 📖	mathematical	—	IsPresentable	—	IsAccessibleCategory.exists_cardinal HasCardinalFilteredGenerator.exists_generator IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator ObjectProperty.IsCardinalFilteredGenerator.presentable HasCardinalFilteredGenerator.toLocallySmall

CategoryTheory.IsAccessibleCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_cardinal 📖	mathematical	—	CategoryTheory.IsCardinalAccessibleCategory	—	—

CategoryTheory.IsCardinalAccessibleCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toHasCardinalFilteredColimits 📖	mathematical	—	CategoryTheory.HasCardinalFilteredColimits	—	—
toHasCardinalFilteredGenerator 📖	mathematical	—	CategoryTheory.HasCardinalFilteredGenerator	—	—

CategoryTheory.IsCardinalLocallyPresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toHasCardinalFilteredGenerator 📖	mathematical	—	CategoryTheory.HasCardinalFilteredGenerator	—	—
toHasColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfSize	—	—

CategoryTheory.IsLocallyPresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_cardinal 📖	mathematical	—	CategoryTheory.IsCardinalLocallyPresentable	—	—

---

← Back to Index