Structures · Category theory
CategoryTheory.Limits.HasColimit
HasColimit F represents the mere existence of a colimit for F.
- Defined in
- Mathlib.CategoryTheory.Limits.HasLimits
- Shape
- One type argument · adds exists_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.Bundled.α
- CategoryTheory.Grothendieck
- CategoryTheory.Limits.WalkingParallelPair
- CategoryTheory.Limits.WalkingReflexivePair
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by383
- CategoryTheory.Limits.colimit
- CategoryTheory.Limits.colimit.ι
- CategoryTheory.Limits.colimit.isColimit
- CategoryTheory.Limits.colimit.ι_desc
- CategoryTheory.Limits.colimit.cocone
- CategoryTheory.Limits.colimMap
- CategoryTheory.Limits.colimit.desc
- CategoryTheory.Limits.HasColimit.isoOfNatIso
- CategoryTheory.Limits.colimit.hom_ext
- CategoryTheory.Limits.colimit.ι_desc_assoc
- CategoryTheory.Limits.ι_colimMap
- CategoryTheory.Limits.colimit.pre
- CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom
- CategoryTheory.Limits.colimit.w
- CategoryTheory.Limits.fiberwiseColimit
- CategoryTheory.Limits.colimit.ι_pre
- CategoryTheory.Limits.ι_colimMap_assoc
- CategoryTheory.Limits.colimit.isoColimitCocone
- CategoryTheory.preservesColimitIso
- CategoryTheory.Limits.hasColimit_of_iso
- CategoryTheory.Limits.hasColimit_ι_comp
- CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom
- CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv
- CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom
- CategoryTheory.Limits.HasColimit.isoOfEquivalence
- CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc
- CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv
- CategoryTheory.Functor.Final.colimitIso
- CategoryTheory.Limits.colimit.post
- CategoryTheory.Functor.colimitIsoOfIsLeftKanExtension
- CategoryTheory.ι_preservesColimitIso_inv
- CategoryTheory.Limits.Sigma.isoColimit
- CategoryTheory.Limits.colimitFiberwiseColimitIso
- CategoryTheory.hasColimit_of_created
- CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom_assoc
- CategoryTheory.Limits.colimitHomIsoLimitYoneda
- CategoryTheory.Limits.Types.jointly_surjective'
- CategoryTheory.Limits.colimitHomIsoLimitYoneda'
- CategoryTheory.Limits.Types.colimitEquivColimitType
- AlgebraicGeometry.PresheafedSpace.componentwiseDiagram
- CategoryTheory.Limits.colimitUncurryIsoColimitCompColim
- CategoryTheory.Limits.colimit.ι_post
- CategoryTheory.Limits.colimitPointwiseProductToProductColimit
- CategoryTheory.Limits.colimitIsoColimitCurryCompColim
- CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂
- CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda
- CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'
- CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_inv_assoc
- CategoryTheory.Limits.limitOpIsoOpColimit
- CategoryTheory.Limits.limitRightOpIsoOpColimit
Ancestors0
No ancestors.