Limit

📁 Source: Mathlib/CategoryTheory/Category/Cat/Limit.lean

Statistics

Metric	Count
Definitions categoryObjects, homDiagram, instCategoryLimitCompObjects, limitCone, limitConeIsLimit, limitConeLift, limitConeX	7
Theorems comp_def, homDiagram_map, homDiagram_obj, id_def, limitConeLift_toFunctor, limitConeX_str, limitConeX_α, limitCone_pt, limitCone_π_app, limit_π_homDiagram_eqToHom, instHasLimits, instPreservesLimitsObjects	12
Total	19

CategoryTheory.Cat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits CategoryTheory.Cat category	—	—
instPreservesLimitsObjects 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits CategoryTheory.Cat category CategoryTheory.types objects	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self

CategoryTheory.Cat.HasLimits

Definitions

Name	Category	Theorems
categoryObjects 📖	CompOp	6 math math: homDiagram_map, limit_π_homDiagram_eqToHom, id_def, comp_def, limitConeLift_toFunctor, homDiagram_obj
homDiagram 📖	CompOp	7 math math: limitCone_π_app, homDiagram_map, limit_π_homDiagram_eqToHom, id_def, comp_def, limitConeLift_toFunctor, homDiagram_obj
instCategoryLimitCompObjects 📖	CompOp	6 math math: limitCone_π_app, limit_π_homDiagram_eqToHom, limitConeX_str, id_def, comp_def, limitConeLift_toFunctor
limitCone 📖	CompOp	2 math math: limitCone_π_app, limitCone_pt
limitConeIsLimit 📖	CompOp	—
limitConeLift 📖	CompOp	1 math math: limitConeLift_toFunctor
limitConeX 📖	CompOp	5 math math: limitCone_π_app, limitCone_pt, limitConeX_α, limitConeX_str, limitConeLift_toFunctor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_def 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.limit CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.objects CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self CategoryTheory.Category.toCategoryStruct instCategoryLimitCompObjects homDiagram CategoryTheory.Functor.obj categoryObjects CategoryTheory.Limits.limit.π	—	CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self
homDiagram_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.types homDiagram CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.objects CategoryTheory.Category.toCategoryStruct categoryObjects CategoryTheory.Limits.limit.π CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Cat.str CategoryTheory.Cat.Hom.toFunctor CategoryTheory.eqToHom	—	CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self
homDiagram_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types homDiagram Quiver.Hom CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.objects CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct categoryObjects CategoryTheory.Limits.limit.π	—	CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self
id_def 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Limits.limit CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.objects CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self CategoryTheory.Category.toCategoryStruct instCategoryLimitCompObjects homDiagram CategoryTheory.Functor.obj categoryObjects CategoryTheory.Limits.limit.π	—	CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self
limitConeLift_toFunctor 📖	mathematical	—	CategoryTheory.Cat.Hom.toFunctor CategoryTheory.Limits.Cone.pt CategoryTheory.Cat CategoryTheory.Cat.category limitConeX limitConeLift CategoryTheory.Bundled.α CategoryTheory.Category CategoryTheory.Bundled.str CategoryTheory.Limits.limit CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Cat.objects instCategoryLimitCompObjects CategoryTheory.Limits.limit.lift CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Cat.str CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π homDiagram CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct categoryObjects CategoryTheory.Limits.limit.π CategoryTheory.eqToHom CategoryTheory.Functor.map	—	—
limitConeX_str 📖	mathematical	—	CategoryTheory.Bundled.str CategoryTheory.Category limitConeX CategoryTheory.Limits.limit CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.objects instCategoryLimitCompObjects	—	—
limitConeX_α 📖	mathematical	—	CategoryTheory.Bundled.α CategoryTheory.Category limitConeX CategoryTheory.Limits.limit CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.objects	—	—
limitCone_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Cat CategoryTheory.Cat.category limitCone limitConeX	—	—
limitCone_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const limitConeX CategoryTheory.Limits.Cone.π limitCone CategoryTheory.Functor.toCatHom CategoryTheory.Limits.limit CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Cat.objects CategoryTheory.Bundled.α CategoryTheory.Category instCategoryLimitCompObjects CategoryTheory.Bundled.str CategoryTheory.Limits.limit.π homDiagram	—	—
limit_π_homDiagram_eqToHom 📖	mathematical	—	CategoryTheory.Limits.limit.π CategoryTheory.types homDiagram CategoryTheory.eqToHom CategoryTheory.Limits.limit CategoryTheory.Functor.comp CategoryTheory.Cat CategoryTheory.Cat.category CategoryTheory.Cat.objects CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self CategoryTheory.Category.toCategoryStruct instCategoryLimitCompObjects CategoryTheory.Functor.obj categoryObjects	—	CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self

---

← Back to Index