Structures · Category theory
CategoryTheory.Limits.HasColimitsOfShape
C has colimits of shape J if there exists a colimit for every functor F : J ⥤ C.
- Defined in
- Mathlib.CategoryTheory.Limits.HasLimits
- Shape
- 2 explicit arguments · adds has_colimit
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances7
- CategoryTheory.Discrete
- CategoryTheory.CostructuredArrow
- CategoryTheory.SingleObj
- CategoryTheory.Grothendieck
- CategoryTheory.Limits.WalkingParallelPair
- CategoryTheory.Limits.WidePushoutShape
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by466
- CategoryTheory.Limits.colim
- CategoryTheory.GrothendieckTopology.plusObj
- CategoryTheory.GrothendieckTopology.sheafify
- CategoryTheory.SmallObject.functorObj
- CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation
- CategoryTheory.SmallObject.functorObjTop
- CategoryTheory.SmallObject.functorObjLeft
- CategoryTheory.GrothendieckTopology.toPlus
- CategoryTheory.GrothendieckTopology.plusMap
- CategoryTheory.SmallObject.ιFunctorObj
- CategoryTheory.Limits.hasColimitsOfShape_of_equivalence
- CategoryTheory.GrothendieckTopology.plusCompIso
- CategoryTheory.GrothendieckTopology.toSheafify
- CategoryTheory.SmallObject.πFunctorObj
- CategoryTheory.GrothendieckTopology.sheafifyCompIso
- CategoryTheory.GrothendieckTopology.plusLift
- CategoryTheory.SmallObject.attachCellsιFunctorObj
- CategoryTheory.SmallObject.ρFunctorObj
- CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_inv
- CategoryTheory.Limits.fiberwiseColim
- CategoryTheory.GrothendieckTopology.sheafifyLift
- CategoryTheory.SmallObject.functorMapSrc
- CategoryTheory.GrothendieckTopology.sheafifyMap
- CategoryTheory.GrothendieckTopology.plusFunctor
- AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit
- CategoryTheory.Limits.colimitLimitIso
- CategoryTheory.GrothendieckTopology.sheafification
- CategoryTheory.Limits.colimitUncurryIsoColimitCompColim
- CategoryTheory.Limits.colimitLimitToLimitColimit
- CategoryTheory.SmallObject.functorMapTgt
- CategoryTheory.preservesColimitNatIso
- CategoryTheory.Limits.colimit.ι_map
- CategoryTheory.SmallObject.functor
- CategoryTheory.GrothendieckTopology.toPlus_naturality
- CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone
- CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op
- CategoryTheory.Limits.colimitIsoColimitCurryCompColim
- AlgebraicGeometry.PresheafedSpace.colimit
- AlgebraicGeometry.PresheafedSpace.colimitCocone
- CategoryTheory.SmallObject.functorMap
- CategoryTheory.SmallObject.ε
- CategoryTheory.GrothendieckTopology.plusMap_toPlus
- CategoryTheory.GrothendieckTopology.plusLift_unique
- CategoryTheory.GrothendieckTopology.isoToPlus
- CategoryTheory.Limits.colimitCompWhiskeringLeftIsoCompColimit
- CategoryTheory.plusPlusSheaf
- CategoryTheory.Limits.fiberwiseColimCompEvaluationIso
- CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence
- CategoryTheory.Limits.colimitFlipIsoCompColim
- CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv
Ancestors0
No ancestors.