Finite

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

Statistics

Metric	Count
Definitions IsFinitelyAccessible, IsFinitelyPresentable, isFinitelyPresentable, isFinitelyPresentable	4
Theorems IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize, isFinitelyAccessible_iff_preservesFilteredColimits, HasCardinalFilteredColimits_iff_hasFilteredColimits, HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize, exists_eq_of_isColimit, exists_hom_of_isColimit, exists_hom_of_isColimit_under, isFinitelyPresentable_eq_isCardinalPresentable, instIsFinitelyPresentableObjFullSubcategoryIsFinitelyPresentableι, instPreservesFilteredColimitsOfSizeObjOppositeFunctorTypeCoyonedaOpOfIsFinitelyPresentable, isFinitelyPresentable_iff_preservesFilteredColimits, isFinitelyPresentable_iff_preservesFilteredColimitsOfSize	12
Total	16

CategoryTheory

Definitions

Name	Category	Theorems
IsFinitelyPresentable 📖	MathDef	7 math math: instIsFinitelyPresentableObjFullSubcategoryIsFinitelyPresentableι, SSet.Finite.instIsFinitelyPresentableObjSimplexCategoryStdSimplex, isFinitelyPresentable_iff_preservesFilteredColimitsOfSize, CommRingCat.isFinitelyPresentable_under, SSet.Finite.instIsFinitelyPresentable, isFinitelyPresentable, isFinitelyPresentable_iff_preservesFilteredColimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
HasCardinalFilteredColimits_iff_hasFilteredColimits 📖	mathematical	—	HasCardinalFilteredColimits Cardinal.aleph0 Cardinal.fact_isRegular_aleph0 Limits.HasFilteredColimits	—	HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize
HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize 📖	mathematical	—	HasCardinalFilteredColimits Cardinal.aleph0 Cardinal.fact_isRegular_aleph0 Limits.HasFilteredColimitsOfSize	—	Cardinal.fact_isRegular_aleph0
instIsFinitelyPresentableObjFullSubcategoryIsFinitelyPresentableι 📖	mathematical	—	IsFinitelyPresentable Functor.obj ObjectProperty.FullSubcategory ObjectProperty.isFinitelyPresentable ObjectProperty.FullSubcategory.category ObjectProperty.ι	—	ObjectProperty.FullSubcategory.property
instPreservesFilteredColimitsOfSizeObjOppositeFunctorTypeCoyonedaOpOfIsFinitelyPresentable 📖	mathematical	—	Limits.PreservesFilteredColimitsOfSize types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda Opposite.op	—	isFinitelyPresentable_iff_preservesFilteredColimitsOfSize
isFinitelyPresentable_iff_preservesFilteredColimits 📖	mathematical	—	IsFinitelyPresentable Limits.PreservesFilteredColimits types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda Opposite.op	—	Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize
isFinitelyPresentable_iff_preservesFilteredColimitsOfSize 📖	mathematical	—	IsFinitelyPresentable Limits.PreservesFilteredColimitsOfSize types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda Opposite.op	—	Functor.IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsFinitelyAccessible 📖	MathDef	2 math math: isFinitelyAccessible_iff_preservesFilteredColimits, IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize 📖	mathematical	—	IsFinitelyAccessible CategoryTheory.Limits.PreservesFilteredColimitsOfSize	—	Cardinal.fact_isRegular_aleph0
isFinitelyAccessible_iff_preservesFilteredColimits 📖	mathematical	—	IsFinitelyAccessible CategoryTheory.Limits.PreservesFilteredColimits	—	IsFinitelyAccessible_iff_preservesFilteredColimitsOfSize

CategoryTheory.IsFinitelyPresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq_of_isColimit 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	CategoryTheory.Functor.map	—	CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.instPreservesFilteredColimitsOfSizeObjOppositeFunctorTypeCoyonedaOpOfIsFinitelyPresentable
exists_hom_of_isColimit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.Limits.Types.jointly_surjective_of_isColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.instPreservesFilteredColimitsOfSizeObjOppositeFunctorTypeCoyonedaOpOfIsFinitelyPresentable
exists_hom_of_isColimit_under 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	—	CategoryTheory.IsFiltered.nonempty exists_hom_of_isColimit CategoryTheory.Under.w

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
isFinitelyPresentable 📖	CompOp	1 math math: CommRingCat.isFinitelyPresentable_hom

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
isFinitelyPresentable 📖	CompOp	5 math math: CategoryTheory.instIsFinitelyPresentableObjFullSubcategoryIsFinitelyPresentableι, CategoryTheory.IsFinitelyAccessibleCategory.instIsFilteredCostructuredArrowFullSubcategoryIsFinitelyPresentableι, CategoryTheory.IsFinitelyAccessibleCategory.instIsDenseFullSubcategoryIsFinitelyPresentableι, isFinitelyPresentable_eq_isCardinalPresentable, CategoryTheory.IsFinitelyAccessibleCategory.instEssentiallySmallIsFinitelyPresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFinitelyPresentable_eq_isCardinalPresentable 📖	mathematical	—	isFinitelyPresentable CategoryTheory.isCardinalPresentable Cardinal.aleph0 Cardinal.fact_isRegular_aleph0	—	—

---

← Back to Index