Structures · Category theory
CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape
A property of objects satisfies P.IsClosedUnderLimitsOfShape J if it
is stable by limits of shape J.
- Shape
- 2 explicit arguments · adds limitsOfShape_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- CategoryTheory.Functor
- CategoryTheory.Over
- CategoryTheory.CostructuredArrow
- CochainComplex
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by44
- CategoryTheory.ObjectProperty.prop_of_isLimit
- CategoryTheory.ObjectProperty.limitsClosure_le
- CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.limitsOfShape_le
- CategoryTheory.ObjectProperty.limitsClosure_eq_self
- CategoryTheory.ObjectProperty.IsClosedUnderBinaryProducts.closedUnderIsomorphisms
- CategoryTheory.ObjectProperty.binaryProductsClosure_le_iff
- CategoryTheory.ObjectProperty.prop_of_isTerminal
- CategoryTheory.Limits.createsLimitFullSubcategoryInclusionOfClosed
- CategoryTheory.ObjectProperty.prop_terminal
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_inv_hom
- CategoryTheory.MorphismProperty.Comma.hasLimit_of_closedUnderLimitsOfShape
- CategoryTheory.Limits.createsLimitsOfShapeFullSubcategoryInclusion
- CategoryTheory.ObjectProperty.prop_limit
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerRight_hom
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift_hom
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorObj_obj
- CategoryTheory.ObjectProperty.LimitOfShape.prop
- CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_ind_discrete
- CategoryTheory.ObjectProperty.instNonemptyOfIsClosedUnderLimitsOfShapeDiscretePEmptyOfHasTerminal
- CategoryTheory.ObjectProperty.IsClosedUnderFiniteProducts.mk'
- CategoryTheory.MorphismProperty.Comma.forgetCreatesLimitsOfShapeOfClosed
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_inv_hom
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift_hom
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerLeft_hom
- CategoryTheory.MorphismProperty.Comma.forgetCreatesLimitOfClosed
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorUnit_obj
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_fst_hom
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_hom_hom
- CategoryTheory.Limits.hasLimitsOfShape_of_closedUnderLimits
- CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape_1
- CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeUnopOppositeOfIsClosedUnderLimitsOfShape
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorHom_hom
- CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeUnopOfIsClosedUnderLimitsOfShapeOpposite
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_inv_hom
- CategoryTheory.Limits.hasLimit_of_closedUnderLimits
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_hom_hom
- CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.inverseImage
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_hom_hom
- CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.of_equivalence
- CategoryTheory.ObjectProperty.prop_pi
- CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape
- CategoryTheory.MorphismProperty.Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape
- CategoryTheory.CartesianMonoidalCategory.fullSubcategory_snd_hom
Ancestors0
No ancestors.