Structures · Category theory
CategoryTheory.HasExactLimitsOfShape
A category C is said to have exact limits of shape J provided that limits of shape J
exist and are exact (in the sense that they preserve finite colimits).
- Shape
- 2 explicit arguments · adds preservesFiniteColimits
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- CategoryTheory.Discrete
How is a type an instance?
Loading the hierarchy index…
Assumed by16
- CategoryTheory.HasExactLimitsOfShape.of_domain_equivalence
- CategoryTheory.hasExactLimitsOfShape_discrete_of_hasExactLimitsOfShape_finset_discrete_op
- CategoryTheory.hasExactLimitsOfShape_of_initial
- CategoryTheory.Limits.IsLimit.pushoutOfHasExactLimitsOfShape
- CategoryTheory.HasExactLimitsOfShape.domain_of_functor
- CategoryTheory.Limits.IsLimit.pushout_hom_ext
- CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite
- Condensed.hasExactLimitsOfShape
- CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat
- CategoryTheory.Sheaf.instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf
- CategoryTheory.HasExactLimitsOfShape.preservesFiniteColimits
- CategoryTheory.instHasExactLimitsOfShapeFunctorOfHasFiniteColimits
- CategoryTheory.CountableAB4Star.of_countableAB5Star
- CategoryTheory.Limits.IsLimit.pushout_zero_ext
- CategoryTheory.Adjunction.hasExactLimitsOfShape
- CategoryTheory.HasExactLimitsOfShape.of_codomain_equivalence
Ancestors0
No ancestors.