Comma

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

Statistics

Metric	Count
Definitions coconeOfPreserves, coconeOfPreservesIsColimit, colimitAuxiliaryCocone, coneOfPreserves, coneOfPreservesIsLimit, limitAuxiliaryCone, createsColimit, createsColimitsOfShape, createsColimitsOfSize, createsLimit, createsLimitsOfShape, createsLimitsOfSize	12
Theorems hasColimit, hasColimits, hasColimitsOfShape, hasLimit, hasLimits, hasLimitsOfShape, preservesColimitsOfShape_leftFunc, preservesColimitsOfShape_rightFunc, coconeOfPreserves_pt_hom, coconeOfPreserves_pt_left, coconeOfPreserves_pt_right, coconeOfPreserves_ι_app_left, coconeOfPreserves_ι_app_right, colimitAuxiliaryCocone_pt, colimitAuxiliaryCocone_ι_app, coneOfPreserves_pt_hom, coneOfPreserves_pt_left, coneOfPreserves_pt_right, coneOfPreserves_π_app_left, coneOfPreserves_π_app_right, hasColimit, hasColimitsOfShape, hasColimitsOfSize, hasLimit, hasLimitsOfShape, hasLimitsOfSize, limitAuxiliaryCone_pt, limitAuxiliaryCone_π_app, preservesColimitsOfShape_fst, preservesColimitsOfShape_snd, epi_iff_epi_left, epi_left_of_epi, hasColimit, hasColimitsOfShape, hasColimitsOfSize, hasTerminal, instHasTerminal, hasLimit, hasLimitsOfShape, hasLimitsOfSize, mono_iff_mono_right, mono_right_of_mono	42
Total	54

CategoryTheory.Arrow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimit 📖	mathematical	—	CategoryTheory.Limits.HasColimit CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	CategoryTheory.Comma.hasColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Limits.id_preservesColimitsOfSize
hasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	hasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
hasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	hasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	CategoryTheory.Comma.hasLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.id_preservesLimitsOfSize
hasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	hasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	hasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
preservesColimitsOfShape_leftFunc 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Arrow CategoryTheory.instCategoryArrow leftFunc	—	CategoryTheory.Comma.preservesColimitsOfShape_fst CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape
preservesColimitsOfShape_rightFunc 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Arrow CategoryTheory.instCategoryArrow rightFunc	—	CategoryTheory.Comma.preservesColimitsOfShape_snd CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape

CategoryTheory.Comma

Definitions

Name	Category	Theorems
coconeOfPreserves 📖	CompOp	5 math math: coconeOfPreserves_pt_right, coconeOfPreserves_ι_app_right, coconeOfPreserves_pt_hom, coconeOfPreserves_ι_app_left, coconeOfPreserves_pt_left
coconeOfPreservesIsColimit 📖	CompOp	—
colimitAuxiliaryCocone 📖	CompOp	5 math math: colimitAuxiliaryCocone_pt, coconeOfPreserves_ι_app_right, coconeOfPreserves_pt_hom, coconeOfPreserves_ι_app_left, colimitAuxiliaryCocone_ι_app
coneOfPreserves 📖	CompOp	5 math math: coneOfPreserves_π_app_right, coneOfPreserves_pt_right, coneOfPreserves_pt_hom, coneOfPreserves_pt_left, coneOfPreserves_π_app_left
coneOfPreservesIsLimit 📖	CompOp	—
limitAuxiliaryCone 📖	CompOp	5 math math: coneOfPreserves_π_app_right, limitAuxiliaryCone_pt, limitAuxiliaryCone_π_app, coneOfPreserves_pt_hom, coneOfPreserves_π_app_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coconeOfPreserves_pt_hom 📖	mathematical	—	hom CategoryTheory.Limits.Cocone.pt CategoryTheory.Comma CategoryTheory.commaCategory coconeOfPreserves CategoryTheory.Limits.IsColimit.desc CategoryTheory.Functor.comp fst CategoryTheory.Functor.mapCocone CategoryTheory.Limits.isColimitOfPreserves colimitAuxiliaryCocone	—	—
coconeOfPreserves_pt_left 📖	mathematical	—	left CategoryTheory.Limits.Cocone.pt CategoryTheory.Comma CategoryTheory.commaCategory coconeOfPreserves CategoryTheory.Functor.comp fst	—	—
coconeOfPreserves_pt_right 📖	mathematical	—	right CategoryTheory.Limits.Cocone.pt CategoryTheory.Comma CategoryTheory.commaCategory coconeOfPreserves CategoryTheory.Functor.comp snd	—	—
coconeOfPreserves_ι_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp fst snd CategoryTheory.Limits.IsColimit.desc CategoryTheory.Functor.mapCocone CategoryTheory.Limits.isColimitOfPreserves colimitAuxiliaryCocone CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι coconeOfPreserves	—	—
coconeOfPreserves_ι_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp fst snd CategoryTheory.Limits.IsColimit.desc CategoryTheory.Functor.mapCocone CategoryTheory.Limits.isColimitOfPreserves colimitAuxiliaryCocone CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι coconeOfPreserves	—	—
colimitAuxiliaryCocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.commaCategory fst colimitAuxiliaryCocone CategoryTheory.Functor.obj snd	—	—
colimitAuxiliaryCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.commaCategory fst CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt snd CategoryTheory.Functor.mapCocone CategoryTheory.Limits.Cocone.ι colimitAuxiliaryCocone CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct left right hom CategoryTheory.Functor.map	—	—
coneOfPreserves_pt_hom 📖	mathematical	—	hom CategoryTheory.Limits.Cone.pt CategoryTheory.Comma CategoryTheory.commaCategory coneOfPreserves CategoryTheory.Limits.IsLimit.lift CategoryTheory.Functor.comp snd CategoryTheory.Functor.mapCone CategoryTheory.Limits.isLimitOfPreserves limitAuxiliaryCone	—	—
coneOfPreserves_pt_left 📖	mathematical	—	left CategoryTheory.Limits.Cone.pt CategoryTheory.Comma CategoryTheory.commaCategory coneOfPreserves CategoryTheory.Functor.comp fst	—	—
coneOfPreserves_pt_right 📖	mathematical	—	right CategoryTheory.Limits.Cone.pt CategoryTheory.Comma CategoryTheory.commaCategory coneOfPreserves CategoryTheory.Functor.comp snd	—	—
coneOfPreserves_π_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp fst snd CategoryTheory.Limits.IsLimit.lift CategoryTheory.Functor.mapCone CategoryTheory.Limits.isLimitOfPreserves limitAuxiliaryCone CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π coneOfPreserves	—	—
coneOfPreserves_π_app_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.obj CategoryTheory.Comma CategoryTheory.commaCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp fst snd CategoryTheory.Limits.IsLimit.lift CategoryTheory.Functor.mapCone CategoryTheory.Limits.isLimitOfPreserves limitAuxiliaryCone CategoryTheory.NatTrans.app CategoryTheory.Limits.Cone.π coneOfPreserves	—	—
hasColimit 📖	mathematical	—	CategoryTheory.Limits.HasColimit CategoryTheory.Comma CategoryTheory.commaCategory	—	—
hasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Comma CategoryTheory.commaCategory	—	hasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit
hasColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfSize CategoryTheory.Comma CategoryTheory.commaCategory	—	hasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Comma CategoryTheory.commaCategory	—	—
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Comma CategoryTheory.commaCategory	—	hasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize CategoryTheory.Comma CategoryTheory.commaCategory	—	hasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
limitAuxiliaryCone_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.commaCategory snd limitAuxiliaryCone CategoryTheory.Functor.obj fst	—	—
limitAuxiliaryCone_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Comma CategoryTheory.commaCategory fst CategoryTheory.Functor.mapCone snd CategoryTheory.Limits.Cone.π limitAuxiliaryCone CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct left right CategoryTheory.Functor.map hom	—	—
preservesColimitsOfShape_fst 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Comma CategoryTheory.commaCategory fst	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
preservesColimitsOfShape_snd 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Comma CategoryTheory.commaCategory snd	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape hasColimitsOfShape preservesColimitsOfShape_fst

CategoryTheory.CostructuredArrow

Definitions

Name	Category	Theorems
createsColimit 📖	CompOp	—
createsColimitsOfShape 📖	CompOp	—
createsColimitsOfSize 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_epi_left 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left	—	epi_left_of_epi epi_of_epi_left
epi_left_of_epi 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left	—	CategoryTheory.Functor.map_epi CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape
hasColimit 📖	mathematical	—	CategoryTheory.Limits.HasColimit CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.Comma.hasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.instHasColimitsOfSizeDiscretePUnit
hasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow	—	hasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit
hasColimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfSize CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow	—	hasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
hasTerminal 📖	mathematical	—	CategoryTheory.Limits.HasTerminal CategoryTheory.CostructuredArrow CategoryTheory.Functor.obj CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.Limits.IsTerminal.hasTerminal

CategoryTheory.Over

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasTerminal 📖	mathematical	—	CategoryTheory.Limits.HasTerminal CategoryTheory.Over CategoryTheory.instCategoryOver	—	CategoryTheory.CostructuredArrow.hasTerminal CategoryTheory.Functor.Faithful.id CategoryTheory.Functor.Full.id

CategoryTheory.StructuredArrow

Definitions

Name	Category	Theorems
createsLimit 📖	CompOp	—
createsLimitsOfShape 📖	CompOp	—
createsLimitsOfSize 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLimit 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow	—	CategoryTheory.Comma.hasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.instHasLimitsOfSizeDiscretePUnit
hasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow	—	hasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
hasLimitsOfSize 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow	—	hasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape
mono_iff_mono_right 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.right	—	mono_right_of_mono mono_of_mono_right
mono_right_of_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.right	—	CategoryTheory.Functor.map_mono CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape

---

← Back to Index