Connected

📁 Source: Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean

Statistics

Metric	Count
Definitions isLimitRaiseCone, natTransInCostructuredArrow, raiseCone, instCreatesLimitsOfShapeProjOfIsConnected, conePost, conePostIso, createsLimitsOfShapeForgetOfIsConnected, forgetCreatesConnectedLimits, isLimitConePost	9
Theorems mapCone_raiseCone, natTransInCostructuredArrow_app, raiseCone_pt, raiseCone_π_app, hasLimitsOfShape_of_isConnected, instPreservesLimitsOfShapeProjOfIsConnected, conePostIso_hom_app_hom, conePostIso_inv_app_hom, conePost_map_hom, conePost_obj_pt, conePost_obj_π_app, forgetPreservesConnectedLimits, hasLimitsOfShape_of_isConnected, preservesLimitsOfShape_forget_of_isConnected	14
Total	23

CategoryTheory.CostructuredArrow

Definitions

Name	Category	Theorems
instCreatesLimitsOfShapeProjOfIsConnected 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLimitsOfShape_of_isConnected 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.hasLimit_of_created CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
instPreservesLimitsOfShapeProjOfIsConnected 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow proj	—	CategoryTheory.Functor.mapCone_π_app CategoryTheory.Functor.map_comp CategoryTheory.Limits.IsLimit.fac CategoryTheory.IsConnected.is_nonempty CreatesConnected.raiseCone_π_app proj_map homMk_left CategoryTheory.Category.assoc CategoryTheory.CommaMorphism.w CategoryTheory.Category.comp_id CategoryTheory.Limits.IsLimit.uniq CategoryTheory.Functor.map_injective proj_faithful

CategoryTheory.CostructuredArrow.CreatesConnected

Definitions

Name	Category	Theorems
isLimitRaiseCone 📖	CompOp	—
natTransInCostructuredArrow 📖	CompOp	1 math math: natTransInCostructuredArrow_app
raiseCone 📖	CompOp	3 math math: mapCone_raiseCone, raiseCone_pt, raiseCone_π_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCone_raiseCone 📖	mathematical	—	CategoryTheory.Functor.mapCone CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj raiseCone	—	—
natTransInCostructuredArrow_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const natTransInCostructuredArrow CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
raiseCone_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow raiseCone CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj Classical.arbitrary CategoryTheory.IsConnected.is_nonempty CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
raiseCone_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj Classical.arbitrary CategoryTheory.IsConnected.is_nonempty CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Limits.Cone.π CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit raiseCone CategoryTheory.CostructuredArrow.homMk	—	CategoryTheory.IsConnected.is_nonempty

CategoryTheory.Over

Definitions

Name	Category	Theorems
conePost 📖	CompOp	5 math math: conePost_obj_π_app, conePostIso_hom_app_hom, conePost_map_hom, conePostIso_inv_app_hom, conePost_obj_pt
conePostIso 📖	CompOp	2 math math: conePostIso_hom_app_hom, conePostIso_inv_app_hom
createsLimitsOfShapeForgetOfIsConnected 📖	CompOp	—
forgetCreatesConnectedLimits 📖	CompOp	—
isLimitConePost 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conePostIso_hom_app_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Functor.obj post forget CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category conePost CategoryTheory.Limits.Cones.functoriality CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.Cones.whiskering conePostIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
conePostIso_inv_app_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Functor.obj post forget CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category conePost CategoryTheory.Limits.Cones.functoriality CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.Cones.whiskering conePostIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt	—	—
conePost_map_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj post CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π homMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.map CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category conePost	—	—
conePost_obj_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj post CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category conePost CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π	—	—
conePost_obj_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.Cone.π post CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category conePost homMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit	—	—
forgetPreservesConnectedLimits 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Over CategoryTheory.instCategoryOver forget	—	preservesLimitsOfShape_forget_of_isConnected
hasLimitsOfShape_of_isConnected 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Over CategoryTheory.instCategoryOver	—	CategoryTheory.hasLimit_of_created CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
preservesLimitsOfShape_forget_of_isConnected 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Over CategoryTheory.instCategoryOver forget	—	CategoryTheory.CostructuredArrow.instPreservesLimitsOfShapeProjOfIsConnected

---

← Back to Index