Structures · Category theory
CategoryTheory.Limits.HasFilteredColimitsOfSize
Class for having all filtered colimits of a given size.
- Defined in
- Mathlib.CategoryTheory.Limits.Filtered
- Shape
- One type argument · adds HasColimitsOfShape
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances5
- CategoryTheory.Functor
- HomologicalComplex
- CategoryTheory.Sheaf
- PartOrdEmb
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by20
- CategoryTheory.Limits.hasCoproducts_of_finite_and_filtered
- CategoryTheory.Limits.hasFilteredColimitsOfSize_of_univLE
- CategoryTheory.AB5OfSize_of_univLE
- CategoryTheory.Limits.hasFilteredColimitsOfSize_shrink
- CategoryTheory.Sheaf.hasFilteredColimitsOfSize
- CategoryTheory.Limits.instIsIPCFunctor
- CategoryTheory.Sheaf.ab5ofSize
- HomologicalComplex.ab5OfSize
- CategoryTheory.Limits.has_colimits_of_finite_and_filtered
- CategoryTheory.Limits.HasFilteredColimitsOfSize.HasColimitsOfShape
- CategoryTheory.AB5OfSize_shrink
- CategoryTheory.MorphismProperty.instIsStableUnderFilteredColimitsMonomorphismsOfAB5OfSize
- CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits
- CategoryTheory.Limits.instIsIPCOfShapeFunctorOfHasFilteredColimitsOfSize
- CategoryTheory.Limits.instIsIPCOfShapeOfIsIPCOfSmall
- HomologicalComplex.instHasFilteredColimitsOfSize
- CategoryTheory.Limits.has_cofiltered_limits_of_has_filtered_colimits_op
- CategoryTheory.Limits.instHasFilteredColimitsOfSizeFunctor
- CategoryTheory.Limits.has_cofiltered_limits_op_of_has_filtered_colimits
- CategoryTheory.AB4.of_AB5
Ancestors0
No ancestors.