HasColimits

📁 Source: Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean

Statistics

Metric	Count
Definitions desc, descCApp, colimit, colimitCocone, colimitCoconeIsColimit, colimitPresheafObjIsoComponentwiseLimit, componentwiseDiagram, pushforwardDiagramToColimit, HasColimits	9
Theorems desc_c_naturality, desc_fac, colimitCocone_pt, colimitCocone_ι_app_base, colimitCocone_ι_app_c, colimitPresheafObjIsoComponentwiseLimit_hom_π, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app, colimit_carrier, colimit_presheaf, componentwiseDiagram_map, componentwiseDiagram_obj, forget_preservesColimits, instHasColimits, instHasColimitsOfShape, instPreservesColimitsOfShapeTopCatForget, map_comp_c_app, map_id_c_app, pushforwardDiagramToColimit_map, pushforwardDiagramToColimit_obj	19
Total	28

AlgebraicGeometry.PresheafedSpace

Definitions

Name	Category	Theorems
colimit 📖	CompOp	5 math math: colimitCocone_ι_app_base, colimit_presheaf, colimit_carrier, colimitCocone_ι_app_c, colimitCocone_pt
colimitCocone 📖	CompOp	5 math math: colimitCocone_ι_app_base, ColimitCoconeIsColimit.desc_c_naturality, ColimitCoconeIsColimit.desc_fac, colimitCocone_ι_app_c, colimitCocone_pt
colimitCoconeIsColimit 📖	CompOp	—
colimitPresheafObjIsoComponentwiseLimit 📖	CompOp	2 math math: colimitPresheafObjIsoComponentwiseLimit_hom_π, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app
componentwiseDiagram 📖	CompOp	4 math math: colimitPresheafObjIsoComponentwiseLimit_hom_π, componentwiseDiagram_map, componentwiseDiagram_obj, colimitPresheafObjIsoComponentwiseLimit_inv_ι_app
pushforwardDiagramToColimit 📖	CompOp	5 math math: ColimitCoconeIsColimit.desc_c_naturality, colimit_presheaf, pushforwardDiagramToColimit_map, pushforwardDiagramToColimit_obj, colimitCocone_ι_app_c

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitCocone_pt 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf	CategoryTheory.Limits.Cocone.pt AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces colimitCocone colimit	—	—
colimitCocone_ι_app_base 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf	Hom.base CategoryTheory.Functor.obj AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const colimit CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι colimitCocone CategoryTheory.Limits.colimit.ι TopCat TopCat.instCategory CategoryTheory.Functor.comp forget	—	—
colimitCocone_ι_app_c 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf	Hom.c CategoryTheory.Functor.obj AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const colimit CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι colimitCocone CategoryTheory.Limits.limit.π carrier CategoryTheory.Limits.colimit TopCat TopCat.instCategory CategoryTheory.Functor.comp forget CategoryTheory.Functor.leftOp pushforwardDiagramToColimit Opposite.op	—	—
colimitPresheafObjIsoComponentwiseLimit_hom_π 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier carrier CategoryTheory.Limits.colimit AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShape TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op CategoryTheory.Limits.limit componentwiseDiagram CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Iso.hom colimitPresheafObjIsoComponentwiseLimit CategoryTheory.Limits.limit.π CategoryTheory.NatTrans.app TopCat.Presheaf.pushforward Hom.base CategoryTheory.Limits.colimit.ι Hom.c	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Iso.eq_inv_comp colimitPresheafObjIsoComponentwiseLimit_inv_ι_app
colimitPresheafObjIsoComponentwiseLimit_inv_ι_app 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit componentwiseDiagram CategoryTheory.Limits.hasColimitOfHasColimitsOfShape AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces instHasColimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier carrier CategoryTheory.Limits.colimit TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op TopCat.Presheaf.pushforward Hom.base CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.inv colimitPresheafObjIsoComponentwiseLimit CategoryTheory.NatTrans.app Hom.c CategoryTheory.Limits.limit.π	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Iso.trans_inv CategoryTheory.Iso.app_inv sheafIsoOfIso_inv TopCat.Presheaf.pushforwardToOfIso_app CategoryTheory.Iso.symm_inv congr_app CategoryTheory.Limits.hasLimit_leftOp_of_hasColimit CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality comp_c_app_assoc CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom CategoryTheory.Limits.hasLimitCompEvaluation CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_π_app_assoc CategoryTheory.Limits.limMap_π_assoc CategoryTheory.eqToHom_map CategoryTheory.eqToHom_unop CategoryTheory.eqToHom_op CategoryTheory.eqToHom_trans
colimit_carrier 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf	carrier colimit CategoryTheory.Limits.colimit TopCat TopCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces forget CategoryTheory.Limits.hasColimitOfHasColimitsOfShape	—	—
colimit_presheaf 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf	presheaf colimit CategoryTheory.Limits.limit CategoryTheory.Limits.colimit TopCat TopCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces forget CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Functor.leftOp pushforwardDiagramToColimit CategoryTheory.Limits.hasLimit_leftOp_of_hasColimit CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape	—	—
componentwiseDiagram_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite componentwiseDiagram CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier carrier AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces Opposite.unop TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op CategoryTheory.Limits.colimit TopologicalSpace.Opens.map Hom.base CategoryTheory.Limits.colimit.ι TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.NatTrans.app Hom.c CategoryTheory.Functor.op CategoryTheory.eqToHom CategoryTheory.CategoryStruct.opposite	—	—
componentwiseDiagram_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite componentwiseDiagram TopologicalSpace.Opens TopCat.carrier carrier AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces Opposite.unop TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf Opposite.op CategoryTheory.Limits.colimit TopologicalSpace.Opens.map Hom.base CategoryTheory.Limits.colimit.ι	—	—
forget_preservesColimits 📖	mathematical	—	CategoryTheory.Limits.PreservesColimits AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces TopCat TopCat.instCategory forget	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone TopCat.topCat_hasColimitsOfShape UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeTopCatForget
instHasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces	—	TopCat.topCat_hasColimitsOfShape UnivLE.small UnivLE.self TopCat.instHasLimitsOfShapePresheaf CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
instHasColimitsOfShape 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf	CategoryTheory.Limits.HasColimitsOfShape AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces	—	—
instPreservesColimitsOfShapeTopCatForget 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf	CategoryTheory.Limits.PreservesColimitsOfShape AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces TopCat TopCat.instCategory forget	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.comp_id
map_comp_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier carrier CategoryTheory.Functor.obj AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward Hom.base CategoryTheory.Functor.map CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Hom.c CategoryTheory.Iso.hom TopCat.Presheaf.pushforwardEq Hom Quiver.Hom TopCat CategoryTheory.CategoryStruct.toQuiver TopCat.instCategory CategoryTheory.Functor.map_comp	—	CategoryTheory.Functor.map_comp congr_app CategoryTheory.eqToHom_map CategoryTheory.Category.assoc TopCat.Presheaf.pushforwardEq_hom_app
map_id_c_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite TopologicalSpace.Opens TopCat.carrier carrier CategoryTheory.Functor.obj AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder presheaf TopCat.Presheaf TopCat.instCategoryPresheaf TopCat.Presheaf.pushforward Hom.base CategoryTheory.Functor.map CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Hom.c CategoryTheory.CategoryStruct.comp TopCat TopCat.instCategory CategoryTheory.Iso.inv TopCat.Presheaf.Pushforward.id CategoryTheory.Iso.hom TopCat.Presheaf.pushforwardEq	—	CategoryTheory.Functor.map_id TopologicalSpace.Opens.map_id_obj congr_app id_c_app CategoryTheory.eqToHom_map CategoryTheory.eqToHom_naturality CategoryTheory.Category.comp_id TopCat.Presheaf.pushforwardEq_hom_app
pushforwardDiagramToColimit_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite TopCat.Presheaf CategoryTheory.Limits.colimit TopCat TopCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces forget CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.opposite TopCat.instCategoryPresheaf pushforwardDiagramToColimit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj TopCat.Presheaf.pushforward CategoryTheory.Limits.colimit.ι presheaf CategoryTheory.CategoryStruct.comp carrier Hom.base Hom.c CategoryTheory.Iso.inv TopCat.Presheaf.Pushforward.comp CategoryTheory.Iso.hom TopCat.Presheaf.pushforwardEq	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
pushforwardDiagramToColimit_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite TopCat.Presheaf CategoryTheory.Limits.colimit TopCat TopCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.PresheafedSpace categoryOfPresheafedSpaces forget CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.opposite TopCat.instCategoryPresheaf pushforwardDiagramToColimit Opposite.op TopCat.Presheaf.pushforward CategoryTheory.Limits.colimit.ι presheaf	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape

AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit

Definitions

Name	Category	Theorems
desc 📖	CompOp	1 math math: desc_fac
descCApp 📖	CompOp	1 math math: desc_c_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
desc_c_naturality 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CategoryTheory.Limits.Cocone.pt AlgebraicGeometry.PresheafedSpace AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf TopCat TopCat.instCategory CategoryTheory.Functor.comp AlgebraicGeometry.PresheafedSpace.forget CategoryTheory.Functor.mapCocone CategoryTheory.Limits.colimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape TopCat.Presheaf.pushforward CategoryTheory.Limits.colimit.desc CategoryTheory.Limits.limit CategoryTheory.Functor.leftOp AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit CategoryTheory.Limits.hasLimit_leftOp_of_hasColimit CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape CategoryTheory.Functor.map descCApp AlgebraicGeometry.PresheafedSpace.colimitCocone	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasLimit_leftOp_of_hasColimit CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape CategoryTheory.Limits.limit_obj_ext CategoryTheory.Functor.congr_obj CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Functor.congr_hom CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc CategoryTheory.Limits.hasLimitCompEvaluation CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_π_app CategoryTheory.Limits.limit.lift_π CategoryTheory.eqToHom_map CategoryTheory.NatTrans.naturality_assoc CategoryTheory.NatTrans.naturality CategoryTheory.eqToHom_op CategoryTheory.Functor.map_comp CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_π_app_assoc CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.eqToHom_trans_assoc CategoryTheory.Category.id_comp
desc_fac 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape Opposite CategoryTheory.Category.opposite TopCat.Presheaf TopCat.instCategoryPresheaf	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.PresheafedSpace CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt AlgebraicGeometry.PresheafedSpace.colimitCocone CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι desc	—	AlgebraicGeometry.PresheafedSpace.ext TopCat.ext CategoryTheory.Limits.colimit.ι_desc TopCat.Presheaf.ext desc_c_naturality CategoryTheory.Category.assoc CategoryTheory.Limits.hasLimitCompEvaluation CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_π_app_assoc CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Functor.congr_obj CategoryTheory.eqToHom_app CategoryTheory.eqToHom_map CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.eqToHom_trans CategoryTheory.Category.comp_id

CategoryTheory.Limits

Definitions

Name	Category	Theorems
HasColimits 📖	MathDef	28 math math: SSet.hasColimits, CategoryTheory.SimplicialObject.Truncated.instHasColimits, DeltaGenerated.hasColimits, CompHaus.hasColimits, CategoryTheory.CosimplicialObject.instHasColimits, AlgebraicGeometry.AffineScheme.hasColimits, Profinite.hasColimits, TopCat.topCat_hasColimits, TopModuleCat.instHasColimits, SSet.Truncated.hasColimits, CategoryTheory.CosimplicialObject.Truncated.instHasColimits, AlgebraicGeometry.SheafedSpace.instHasColimitsOfHasLimits, RingCat.Colimits.hasColimits_ringCat, AlgebraicGeometry.PresheafedSpace.instHasColimits, hasColimits_of_hasLimits_of_hasCoseparator, AlgebraicGeometry.Scheme.Modules.instHasColimits, instHasColimitsCommAlgCat, CategoryTheory.Arrow.hasColimits, CommRingCat.Colimits.hasColimits_commRingCat, instHasColimitsCondensedMod, AlgebraicGeometry.LocallyRingedSpace.instHasColimits, MonCat.Colimits.hasColimits_monCat, CategoryTheory.instHasColimitsIndOfHasFiniteColimits, Action.instHasColimits, CategoryTheory.Cat.instHasColimits, hasColimits_of_hasLimits_of_isCoseparating, CategoryTheory.SimplicialObject.instHasColimits, CategoryTheory.Over.instHasColimits

---

← Back to Index