Structures · Category theory
CategoryTheory.HasExactColimitsOfShape
A category C is said to have exact colimits of shape J provided that colimits of shape J
exist and are exact (in the sense that they preserve finite limits).
- Shape
- 2 explicit arguments · adds preservesFiniteLimits
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- CategoryTheory.Discrete
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by20
- CategoryTheory.HasExactColimitsOfShape.of_domain_equivalence
- CategoryTheory.hasExactColimitsOfShape_discrete_of_hasExactColimitsOfShape_finset_discrete
- CategoryTheory.hasExactColimitsOfShape_of_final
- CategoryTheory.Limits.IsColimit.pullbackOfHasExactColimitsOfShape
- CategoryTheory.Limits.IsColimit.pullback_hom_ext
- CategoryTheory.Limits.colim.exact_mapShortComplex
- CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat_and_finite
- CategoryTheory.Limits.IsColimit.pullback_zero_ext
- CategoryTheory.HasExactColimitsOfShape.domain_of_functor
- CategoryTheory.HasExactColimitsOfShape.of_codomain_equivalence
- HomologicalComplex.hasExactColimitsOfShape
- CategoryTheory.instHasExactColimitsOfShapeFunctorOfHasFiniteLimits
- CategoryTheory.CountableAB4.of_countableAB5
- Condensed.hasExactColimitsOfShape
- CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeFunctorPreservesFiniteLimitsOfHasExactColimitsOfShape
- CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits
- CategoryTheory.Adjunction.hasExactColimitsOfShape
- CategoryTheory.Sheaf.instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf
- CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat
- CategoryTheory.Sheaf.hasExactColimitsOfShape
Ancestors0
No ancestors.