ConeCategory

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

Statistics

Metric	Count
Definitions toCostructuredArrowIsoToCostructuredArrow, toStructuredArrowIsoToStructuredArrow, equivStructuredArrow, fromCostructuredArrow, fromStructuredArrow, isColimitEquivIsInitial, mapCoconeToOver, toCostructuredArrow, toCostructuredArrowCocone, toCostructuredArrowCompProj, toCostructuredArrowCompToOverCompForget, toCostructuredArrowIsoToCostructuredArrow, toOver, toStructuredArrow, equivCostructuredArrow, fromCostructuredArrow, fromStructuredArrow, isLimitEquivIsTerminal, mapConeToUnder, toCostructuredArrow, toStructuredArrow, toStructuredArrowCompProj, toStructuredArrowCompToUnderCompForget, toStructuredArrowCone, toStructuredArrowIsoToStructuredArrow, toUnder, ofPreservesCoconeInitial, ofReflectsCoconeInitial, ofPreservesConeTerminal, ofReflectsConeTerminal, toCostructuredArrow, toOver, toStructuredArrow, toUnder	34
Theorems equivStructuredArrow_counitIso, equivStructuredArrow_functor, equivStructuredArrow_inverse, equivStructuredArrow_unitIso, fromCostructuredArrow_pt, fromCostructuredArrow_ι_app, fromStructuredArrow_map_hom, fromStructuredArrow_obj_pt, fromStructuredArrow_obj_ι, mapCoconeToOver_hom_hom, mapCoconeToOver_inv_hom, toCostructuredArrowCocone_pt, toCostructuredArrowCocone_ι_app, toCostructuredArrowCompProj_hom_app, toCostructuredArrowCompProj_inv_app, toCostructuredArrowCompToOverCompForget_hom_app, toCostructuredArrowCompToOverCompForget_inv_app, toCostructuredArrow_comp_proj, toCostructuredArrow_comp_toOver_comp_forget, toCostructuredArrow_map, toCostructuredArrow_obj, toOver_pt, toOver_ι_app, toStructuredArrow_map, toStructuredArrow_obj, equivCostructuredArrow_counitIso, equivCostructuredArrow_functor, equivCostructuredArrow_inverse, equivCostructuredArrow_unitIso, fromCostructuredArrow_map_hom, fromCostructuredArrow_obj_pt, fromCostructuredArrow_obj_π, fromStructuredArrow_pt, fromStructuredArrow_π_app, mapConeToUnder_hom_hom, mapConeToUnder_inv_hom, toCostructuredArrow_map, toCostructuredArrow_obj, toStructuredArrowCompProj_hom_app, toStructuredArrowCompProj_inv_app, toStructuredArrowCompToUnderCompForget_hom_app, toStructuredArrowCompToUnderCompForget_inv_app, toStructuredArrowCone_pt, toStructuredArrowCone_π_app, toStructuredArrow_comp_proj, toStructuredArrow_comp_toUnder_comp_forget, toStructuredArrow_map, toStructuredArrow_obj, toUnder_pt, toUnder_π_app, descCoconeMorphism_eq_isInitial_to, to_eq_descCoconeMorphism, liftConeMorphism_eq_isTerminal_from, from_eq_liftConeMorphism, toCostructuredArrow_map, toCostructuredArrow_obj, toOver_pt, toOver_ι_app, hasColimit_iff_hasInitial_cocone, hasColimitsOfShape_iff_isRightAdjoint_const, hasLimit_iff_hasTerminal_cone, hasLimitsOfShape_iff_isLeftAdjoint_const, toStructuredArrow_map, toStructuredArrow_obj	64
Total	98

CategoryTheory.Functor

Definitions

Name	Category	Theorems
toCostructuredArrowIsoToCostructuredArrow 📖	CompOp	—
toStructuredArrowIsoToStructuredArrow 📖	CompOp	—

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimit_iff_hasInitial_cocone 📖	mathematical	—	HasColimit HasInitial Cocone Cocone.category	—	IsInitial.hasInitial
hasColimitsOfShape_iff_isRightAdjoint_const 📖	mathematical	—	HasColimitsOfShape CategoryTheory.Functor.IsRightAdjoint CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const	—	HasColimitsOfShape.has_colimit hasColimit_iff_hasInitial_cocone CategoryTheory.Equivalence.hasInitial_iff CategoryTheory.isRightAdjoint_iff_hasInitial_structuredArrow
hasLimit_iff_hasTerminal_cone 📖	mathematical	—	HasLimit HasTerminal Cone Cone.category	—	IsTerminal.hasTerminal
hasLimitsOfShape_iff_isLeftAdjoint_const 📖	mathematical	—	HasLimitsOfShape CategoryTheory.Functor.IsLeftAdjoint CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const	—	HasLimitsOfShape.has_limit hasLimit_iff_hasTerminal_cone CategoryTheory.Equivalence.hasTerminal_iff CategoryTheory.isLeftAdjoint_iff_hasTerminal_costructuredArrow

CategoryTheory.Limits.Cocone

Definitions

Name	Category	Theorems
equivStructuredArrow 📖	CompOp	4 math math: equivStructuredArrow_unitIso, equivStructuredArrow_inverse, equivStructuredArrow_functor, equivStructuredArrow_counitIso
fromCostructuredArrow 📖	CompOp	2 math math: fromCostructuredArrow_ι_app, fromCostructuredArrow_pt
fromStructuredArrow 📖	CompOp	6 math math: equivStructuredArrow_unitIso, fromStructuredArrow_obj_pt, fromStructuredArrow_map_hom, equivStructuredArrow_inverse, fromStructuredArrow_obj_ι, equivStructuredArrow_counitIso
isColimitEquivIsInitial 📖	CompOp	2 math math: CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism, CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to
mapCoconeToOver 📖	CompOp	2 math math: mapCoconeToOver_inv_hom, mapCoconeToOver_hom_hom
toCostructuredArrow 📖	CompOp	16 math math: toOver_ι_app, toCostructuredArrow_comp_proj, toCostructuredArrow_comp_toOver_comp_forget, toCostructuredArrow_map, toCostructuredArrowCompProj_hom_app, toCostructuredArrowCompToOverCompForget_inv_app, CategoryTheory.Presheaf.final_toCostructuredArrow_comp_pre, toOver_pt, CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_map_left, toCostructuredArrowCocone_ι_app, toCostructuredArrowCompToOverCompForget_hom_app, toCostructuredArrow_obj, mapCoconeToOver_inv_hom, toCostructuredArrowCompProj_inv_app, toCostructuredArrowCocone_pt, mapCoconeToOver_hom_hom
toCostructuredArrowCocone 📖	CompOp	2 math math: toCostructuredArrowCocone_ι_app, toCostructuredArrowCocone_pt
toCostructuredArrowCompProj 📖	CompOp	2 math math: toCostructuredArrowCompProj_hom_app, toCostructuredArrowCompProj_inv_app
toCostructuredArrowCompToOverCompForget 📖	CompOp	2 math math: toCostructuredArrowCompToOverCompForget_inv_app, toCostructuredArrowCompToOverCompForget_hom_app
toCostructuredArrowIsoToCostructuredArrow 📖	CompOp	—
toOver 📖	CompOp	4 math math: toOver_ι_app, toOver_pt, mapCoconeToOver_inv_hom, mapCoconeToOver_hom_hom
toStructuredArrow 📖	CompOp	5 math math: toStructuredArrow_obj, equivStructuredArrow_unitIso, toStructuredArrow_map, equivStructuredArrow_functor, equivStructuredArrow_counitIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivStructuredArrow_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Limits.Cocone CategoryTheory.StructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const category CategoryTheory.instCategoryStructuredArrow equivStructuredArrow CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp fromStructuredArrow toStructuredArrow CategoryTheory.Functor.id CategoryTheory.Iso.symm CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.StructuredArrow.eta	—	—
equivStructuredArrow_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Limits.Cocone CategoryTheory.StructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const category CategoryTheory.instCategoryStructuredArrow equivStructuredArrow toStructuredArrow	—	—
equivStructuredArrow_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Limits.Cocone CategoryTheory.StructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const category CategoryTheory.instCategoryStructuredArrow equivStructuredArrow fromStructuredArrow	—	—
equivStructuredArrow_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Limits.Cocone CategoryTheory.StructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const category CategoryTheory.instCategoryStructuredArrow equivStructuredArrow CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp toStructuredArrow fromStructuredArrow CategoryTheory.Limits.Cocones.eta	—	—
fromCostructuredArrow_pt 📖	mathematical	—	pt CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.proj fromCostructuredArrow	—	—
fromCostructuredArrow_ι_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 ι fromCostructuredArrow CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
fromStructuredArrow_map_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.const CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Limits.Cocone category fromStructuredArrow CategoryTheory.CommaMorphism.right	—	—
fromStructuredArrow_obj_pt 📖	mathematical	—	pt CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.instCategoryStructuredArrow CategoryTheory.Limits.Cocone category fromStructuredArrow CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
fromStructuredArrow_obj_ι 📖	mathematical	—	ι CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.instCategoryStructuredArrow CategoryTheory.Limits.Cocone category fromStructuredArrow CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
mapCoconeToOver_hom_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Functor.comp CategoryTheory.Over pt CategoryTheory.instCategoryOver CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.toOver CategoryTheory.Over.forget CategoryTheory.Functor.mapCocone toOver CategoryTheory.Iso.hom CategoryTheory.Limits.Cocone category mapCoconeToOver CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
mapCoconeToOver_inv_hom 📖	mathematical	—	CategoryTheory.Limits.CoconeMorphism.hom CategoryTheory.Functor.comp CategoryTheory.Over pt CategoryTheory.instCategoryOver CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.toOver CategoryTheory.Over.forget CategoryTheory.Functor.mapCocone toOver CategoryTheory.Iso.inv CategoryTheory.Limits.Cocone category mapCoconeToOver CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
toCostructuredArrowCocone_pt 📖	mathematical	—	pt CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp CategoryTheory.Functor.mapCocone toCostructuredArrow CategoryTheory.CostructuredArrow.map CategoryTheory.CostructuredArrow.pre toCostructuredArrowCocone	—	—
toCostructuredArrowCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Functor.comp pt CategoryTheory.Functor.mapCocone toCostructuredArrow CategoryTheory.CostructuredArrow.map CategoryTheory.CostructuredArrow.pre CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const ι toCostructuredArrowCocone CategoryTheory.CostructuredArrow.homMk	—	—
toCostructuredArrowCompProj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow pt CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id toCostructuredArrowCompProj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
toCostructuredArrowCompProj_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow pt CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id toCostructuredArrowCompProj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
toCostructuredArrowCompToOverCompForget_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow pt CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.CostructuredArrow.toOver CategoryTheory.Over.forget CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category toCostructuredArrowCompToOverCompForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
toCostructuredArrowCompToOverCompForget_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow pt CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.CostructuredArrow.toOver CategoryTheory.Over.forget CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category toCostructuredArrowCompToOverCompForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
toCostructuredArrow_comp_proj 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow pt CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.proj CategoryTheory.Functor.id	—	—
toCostructuredArrow_comp_toOver_comp_forget 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow pt CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.CostructuredArrow.toOver CategoryTheory.Over.forget	—	—
toCostructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CostructuredArrow pt CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.homMk CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const ι	—	—
toCostructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow pt CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const ι	—	—
toOver_pt 📖	mathematical	—	pt CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.toOver toOver CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
toOver_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over pt CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.toOver CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct ι toOver CategoryTheory.Over.homMk	—	—
toStructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Limits.Cocone category CategoryTheory.StructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.homMk pt ι CategoryTheory.Limits.CoconeMorphism.hom	—	—
toStructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.Cocone category CategoryTheory.StructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.instCategoryStructuredArrow toStructuredArrow pt ι	—	—

CategoryTheory.Limits.Cone

Definitions

Name	Category	Theorems
equivCostructuredArrow 📖	CompOp	4 math math: equivCostructuredArrow_inverse, equivCostructuredArrow_functor, equivCostructuredArrow_counitIso, equivCostructuredArrow_unitIso
fromCostructuredArrow 📖	CompOp	6 math math: fromCostructuredArrow_map_hom, fromCostructuredArrow_obj_π, equivCostructuredArrow_inverse, equivCostructuredArrow_counitIso, fromCostructuredArrow_obj_pt, equivCostructuredArrow_unitIso
fromStructuredArrow 📖	CompOp	2 math math: fromStructuredArrow_π_app, fromStructuredArrow_pt
isLimitEquivIsTerminal 📖	CompOp	2 math math: CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from, CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism
mapConeToUnder 📖	CompOp	2 math math: mapConeToUnder_inv_hom, mapConeToUnder_hom_hom
toCostructuredArrow 📖	CompOp	5 math math: toCostructuredArrow_obj, toCostructuredArrow_map, equivCostructuredArrow_functor, equivCostructuredArrow_counitIso, equivCostructuredArrow_unitIso
toStructuredArrow 📖	CompOp	14 math math: toUnder_pt, toStructuredArrowCompProj_inv_app, toStructuredArrowCompToUnderCompForget_hom_app, toStructuredArrow_comp_toUnder_comp_forget, toStructuredArrowCone_π_app, mapConeToUnder_inv_hom, toStructuredArrowCompProj_hom_app, toStructuredArrow_obj, toUnder_π_app, toStructuredArrow_comp_proj, mapConeToUnder_hom_hom, toStructuredArrow_map, toStructuredArrowCompToUnderCompForget_inv_app, toStructuredArrowCone_pt
toStructuredArrowCompProj 📖	CompOp	2 math math: toStructuredArrowCompProj_inv_app, toStructuredArrowCompProj_hom_app
toStructuredArrowCompToUnderCompForget 📖	CompOp	2 math math: toStructuredArrowCompToUnderCompForget_hom_app, toStructuredArrowCompToUnderCompForget_inv_app
toStructuredArrowCone 📖	CompOp	2 math math: toStructuredArrowCone_π_app, toStructuredArrowCone_pt
toStructuredArrowIsoToStructuredArrow 📖	CompOp	—
toUnder 📖	CompOp	4 math math: toUnder_pt, mapConeToUnder_inv_hom, toUnder_π_app, mapConeToUnder_hom_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivCostructuredArrow_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Limits.Cone CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const category CategoryTheory.instCategoryCostructuredArrow equivCostructuredArrow CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp fromCostructuredArrow toCostructuredArrow CategoryTheory.Functor.id CategoryTheory.Iso.symm CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.CostructuredArrow.eta	—	—
equivCostructuredArrow_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Limits.Cone CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const category CategoryTheory.instCategoryCostructuredArrow equivCostructuredArrow toCostructuredArrow	—	—
equivCostructuredArrow_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Limits.Cone CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const category CategoryTheory.instCategoryCostructuredArrow equivCostructuredArrow fromCostructuredArrow	—	—
equivCostructuredArrow_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Limits.Cone CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const category CategoryTheory.instCategoryCostructuredArrow equivCostructuredArrow CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp toCostructuredArrow fromCostructuredArrow CategoryTheory.Limits.Cones.eta	—	—
fromCostructuredArrow_map_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Limits.Cone category fromCostructuredArrow CategoryTheory.CommaMorphism.left	—	—
fromCostructuredArrow_obj_pt 📖	mathematical	—	pt CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Limits.Cone category fromCostructuredArrow CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
fromCostructuredArrow_obj_π 📖	mathematical	—	π CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Limits.Cone category fromCostructuredArrow CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
fromStructuredArrow_pt 📖	mathematical	—	pt CategoryTheory.Functor.comp CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.StructuredArrow.proj fromStructuredArrow	—	—
fromStructuredArrow_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Functor.comp CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.StructuredArrow.proj π fromStructuredArrow CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	—
mapConeToUnder_hom_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Functor.comp CategoryTheory.Under pt CategoryTheory.instCategoryUnder CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.toUnder CategoryTheory.Under.forget CategoryTheory.Functor.mapCone toUnder CategoryTheory.Iso.hom CategoryTheory.Limits.Cone category mapConeToUnder CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
mapConeToUnder_inv_hom 📖	mathematical	—	CategoryTheory.Limits.ConeMorphism.hom CategoryTheory.Functor.comp CategoryTheory.Under pt CategoryTheory.instCategoryUnder CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.toUnder CategoryTheory.Under.forget CategoryTheory.Functor.mapCone toUnder CategoryTheory.Iso.inv CategoryTheory.Limits.Cone category mapConeToUnder CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
toCostructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Limits.Cone category CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.homMk pt π CategoryTheory.Limits.ConeMorphism.hom	—	—
toCostructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.Cone category CategoryTheory.CostructuredArrow CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow pt π	—	—
toStructuredArrowCompProj_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.StructuredArrow pt CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.proj CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id toStructuredArrowCompProj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
toStructuredArrowCompProj_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.StructuredArrow pt CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.proj CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id toStructuredArrowCompProj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
toStructuredArrowCompToUnderCompForget_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.StructuredArrow pt CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.StructuredArrow.toUnder CategoryTheory.Under.forget CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category toStructuredArrowCompToUnderCompForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
toStructuredArrowCompToUnderCompForget_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.StructuredArrow pt CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.StructuredArrow.toUnder CategoryTheory.Under.forget CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category toStructuredArrowCompToUnderCompForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—
toStructuredArrowCone_pt 📖	mathematical	—	pt CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.comp CategoryTheory.Functor.mapCone toStructuredArrow CategoryTheory.StructuredArrow.map CategoryTheory.StructuredArrow.pre toStructuredArrowCone	—	—
toStructuredArrowCone_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const pt CategoryTheory.Functor.comp CategoryTheory.Functor.mapCone toStructuredArrow CategoryTheory.StructuredArrow.map CategoryTheory.StructuredArrow.pre π toStructuredArrowCone CategoryTheory.StructuredArrow.homMk	—	—
toStructuredArrow_comp_proj 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.StructuredArrow pt CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.proj CategoryTheory.Functor.id	—	—
toStructuredArrow_comp_toUnder_comp_forget 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.StructuredArrow pt CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.StructuredArrow.toUnder CategoryTheory.Under.forget	—	—
toStructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.StructuredArrow pt CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.homMk CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const π	—	—
toStructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow pt CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const π	—	—
toUnder_pt 📖	mathematical	—	pt CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.comp CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.toUnder toUnder CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
toUnder_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Under pt CategoryTheory.instCategoryUnder CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.toUnder π toUnder CategoryTheory.Under.homMk	—	—

CategoryTheory.Limits.IsColimit

Definitions

Name	Category	Theorems
ofPreservesCoconeInitial 📖	CompOp	—
ofReflectsCoconeInitial 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
descCoconeMorphism_eq_isInitial_to 📖	mathematical	—	descCoconeMorphism CategoryTheory.Limits.IsInitial.to CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category DFunLike.coe Equiv CategoryTheory.Limits.IsColimit CategoryTheory.Limits.IsInitial EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Limits.Cocone.isColimitEquivIsInitial	—	—

CategoryTheory.Limits.IsInitial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_eq_descCoconeMorphism 📖	mathematical	—	to CategoryTheory.Limits.Cocone CategoryTheory.Limits.Cocone.category CategoryTheory.Limits.IsColimit.descCoconeMorphism DFunLike.coe Equiv CategoryTheory.Limits.IsInitial CategoryTheory.Limits.IsColimit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Limits.Cocone.isColimitEquivIsInitial	—	CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to

CategoryTheory.Limits.IsLimit

Definitions

Name	Category	Theorems
ofPreservesConeTerminal 📖	CompOp	—
ofReflectsConeTerminal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftConeMorphism_eq_isTerminal_from 📖	mathematical	—	liftConeMorphism CategoryTheory.Limits.IsTerminal.from CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category DFunLike.coe Equiv CategoryTheory.Limits.IsLimit CategoryTheory.Limits.IsTerminal EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Limits.Cone.isLimitEquivIsTerminal	—	—

CategoryTheory.Limits.IsTerminal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
from_eq_liftConeMorphism 📖	mathematical	—	from CategoryTheory.Limits.Cone CategoryTheory.Limits.Cone.category CategoryTheory.Limits.IsLimit.liftConeMorphism DFunLike.coe Equiv CategoryTheory.Limits.IsTerminal CategoryTheory.Limits.IsLimit EquivLike.toFunLike Equiv.instEquivLike Equiv.symm CategoryTheory.Limits.Cone.isLimitEquivIsTerminal	—	CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from

CategoryTheory.Limits.colimit

Definitions

Name	Category	Theorems
toCostructuredArrow 📖	CompOp	4 math math: toOver_ι_app, toCostructuredArrow_map, toCostructuredArrow_obj, toOver_pt
toOver 📖	CompOp	2 math math: toOver_ι_app, toOver_pt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCostructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.Limits.colimit CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.homMk ι	—	—
toCostructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.Limits.colimit CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow ι	—	—
toOver_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Over CategoryTheory.Limits.colimit CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.toOver toOver CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
toOver_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.Limits.colimit CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.toOver CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cocone.ι toOver CategoryTheory.Over.homMk ι	—	—

CategoryTheory.Limits.limit

Definitions

Name	Category	Theorems
toStructuredArrow 📖	CompOp	2 math math: toStructuredArrow_obj, toStructuredArrow_map
toUnder 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toStructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.StructuredArrow CategoryTheory.Limits.limit CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.homMk π	—	—
toStructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.Limits.limit CategoryTheory.instCategoryStructuredArrow toStructuredArrow π	—	—

---

← Back to Index