Documentation Verification Report

Connected

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

Statistics

Metric	Count
Definitions `isColimitOfIsIsoColimMapι`, `isLimitOfIsIsoLimMapπ`, `constCocone`, `constCone`, `isColimitConstCocone`, `isLimitConstCone`, `forgetCone`, `γ₁`, `γ₂`, `parallelPairInhabited`	10
Theorems `isColimit_iff_isIso_colimMap_ι`, `isLimit_iff_isIso_limMap_π`, `isIso_colimMap_ι`, `isIso_limMap_π`, `constCocone_pt`, `constCocone_ι`, `constCone_pt`, `constCone_π`, `hasColimit_const_of_isConnected`, `hasLimit_const_of_isConnected`, `forgetCone_pt`, `forgetCone_π`, `γ₁_app`, `γ₂_app`, `parallel_pair_connected`, `prod_preservesConnectedLimits`, `widePullbackShape_connected`, `widePushoutShape_connected`	18
Total	28

CategoryTheory

Definitions

Name	Category	Theorems
`parallelPairInhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`parallel_pair_connected` 📖	mathematical	—	`IsConnected` `Limits.WalkingParallelPair` `Limits.walkingParallelPairHomCategory`	—	`IsConnected.of_induct`
`prod_preservesConnectedLimits` 📖	mathematical	—	`Limits.PreservesLimitsOfShape` `Functor.obj` `Functor` `Functor.category` `Limits.prod.functor`	—	`IsConnected.is_nonempty` `Limits.prod.hom_ext` `Category.assoc` `Limits.limMap_π` `Category.comp_id` `Limits.limit.lift_π` `nat_trans_from_is_connected` `IsConnected.toIsPreconnected` `Limits.prod.lift_map` `Limits.IsLimit.fac` `Limits.prod.map_fst` `Limits.IsLimit.uniq` `Limits.prod.map_snd`
`widePullbackShape_connected` 📖	mathematical	—	`IsConnected` `Limits.WidePullbackShape` `Limits.WidePullbackShape.category`	—	`IsConnected.of_induct`
`widePushoutShape_connected` 📖	mathematical	—	`IsConnected` `Limits.WidePushoutShape` `Limits.WidePushoutShape.category`	—	`IsConnected.of_induct`

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`constCocone` 📖	CompOp	2 math math: `constCocone_ι`, `constCocone_pt`
`constCone` 📖	CompOp	2 math math: `constCone_pt`, `constCone_π`
`isColimitConstCocone` 📖	CompOp	—
`isLimitConstCone` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`constCocone_pt` 📖	mathematical	—	`Cocone.pt` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `constCocone`	—	—
`constCocone_ι` 📖	mathematical	—	`Cocone.ι` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `constCocone` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`constCone_pt` 📖	mathematical	—	`Cone.pt` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `constCone`	—	—
`constCone_π` 📖	mathematical	—	`Cone.π` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `constCone` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`hasColimit_const_of_isConnected` 📖	mathematical	—	`HasColimit` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const`	—	—
`hasLimit_const_of_isConnected` 📖	mathematical	—	`HasLimit` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const`	—	—

CategoryTheory.Limits.Cocone

Definitions

Name	Category	Theorems
`isColimitOfIsIsoColimMapι` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isColimit_iff_isIso_colimMap_ι` 📖	mathematical	—	`CategoryTheory.Limits.IsColimit` `CategoryTheory.IsIso` `CategoryTheory.Limits.colimit` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `pt` `CategoryTheory.Limits.hasColimit_const_of_isConnected` `CategoryTheory.Limits.colimMap` `ι`	—	`CategoryTheory.Limits.hasColimit_const_of_isConnected` `CategoryTheory.Limits.IsColimit.isIso_colimMap_ι`

CategoryTheory.Limits.Cone

Definitions

Name	Category	Theorems
`isLimitOfIsIsoLimMapπ` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLimit_iff_isIso_limMap_π` 📖	mathematical	—	`CategoryTheory.Limits.IsLimit` `CategoryTheory.IsIso` `CategoryTheory.Limits.limit` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `pt` `CategoryTheory.Limits.hasLimit_const_of_isConnected` `CategoryTheory.Limits.limMap` `π`	—	`CategoryTheory.Limits.hasLimit_const_of_isConnected` `CategoryTheory.Limits.IsLimit.isIso_limMap_π`

CategoryTheory.Limits.IsColimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIso_colimMap_ι` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Limits.colimit` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.hasColimit_const_of_isConnected` `CategoryTheory.Limits.colimMap` `CategoryTheory.Limits.Cocone.ι`	—	`CategoryTheory.Limits.hasColimit_const_of_isConnected` `CategoryTheory.Limits.colimit.hom_ext` `CategoryTheory.Limits.ι_colimMap` `CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom_assoc` `CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv` `CategoryTheory.Iso.isIso_hom`

CategoryTheory.Limits.IsLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIso_limMap_π` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Limits.limit` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.hasLimit_const_of_isConnected` `CategoryTheory.Limits.limMap` `CategoryTheory.Limits.Cone.π`	—	`CategoryTheory.Limits.hasLimit_const_of_isConnected` `CategoryTheory.Limits.limit.hom_ext` `CategoryTheory.Limits.limMap_π` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp` `CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp` `CategoryTheory.Iso.isIso_hom`

CategoryTheory.ProdPreservesConnectedLimits

Definitions

Name	Category	Theorems
`forgetCone` 📖	CompOp	2 math math: `forgetCone_π`, `forgetCone_pt`
`γ₁` 📖	CompOp	1 math math: `γ₁_app`
`γ₂` 📖	CompOp	2 math math: `γ₂_app`, `forgetCone_π`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forgetCone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `forgetCone` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.prod.functor`	—	—
`forgetCone_π` 📖	mathematical	—	`CategoryTheory.Limits.Cone.π` `forgetCone` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Functor.comp` `CategoryTheory.Limits.prod.functor` `γ₂`	—	—
`γ₁_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.prod.functor` `CategoryTheory.Functor.const` `γ₁` `CategoryTheory.Limits.prod.fst`	—	—
`γ₂_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.prod.functor` `γ₂` `CategoryTheory.Limits.prod.snd`	—	—

---

← Back to Index