LimitsOfShape

📁 Source: Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean

Statistics

Metric	Count
Definitions IsClosedUnderLimitsOfShape, LimitOfShape, limit, ofIso, ofLE, reindex, toLimitPresentation, toStructuredArrow, limitsOfShape, strictLimitsOfShape	10
Theorems inverseImage, limitsOfShape_le, mk', of_equivalence, limitsOfShape, ofIso_toLimitPresentation, ofLE_toLimitPresentation, prop, prop_diag_obj, reindex_toLimitPresentation, toStructuredArrow_map, toStructuredArrow_obj, instEssentiallySmallLimitsOfShapeOfSmallOfSmallOfLocallySmall, instIsClosedUnderIsomorphismsLimitsOfShape, instIsClosedUnderLimitsOfShapeBotOfNonempty, instIsClosedUnderLimitsOfShapeTop, instSmallStrictLimitsOfShapeOfSmallOfLocallySmall, isClosedUnderLimitsOfShape_iff, isClosedUnderLimitsOfShape_iff_of_equivalence, isClosedUnderLimitsOfShape_inverseImage_iff, isoClosure_strictLimitsOfShape, limitsOfShape_bot, limitsOfShape_congr, limitsOfShape_isoClosure, limitsOfShape_le_of_initial, limitsOfShape_monotone, prop_limit, prop_of_isLimit, prop_pi, strictLimitsOfShape_bot, strictLimitsOfShape_le_limitsOfShape, strictLimitsOfShape_monotone	32
Total	42

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
IsClosedUnderLimitsOfShape 📖	CompData	37 math math: instIsClosedUnderLimitsOfShapeUnopOppositeOfIsClosedUnderColimitsOfShape, isClosedUnderColimitsOfShape_iff_op, instIsClosedUnderLimitsOfShapeTop, CategoryTheory.Limits.isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair, CategoryTheory.instIsClosedUnderLimitsOfShapeFunctorOppositeTypeIsIndObjectDiscreteOfHasLimitsOfShape, CategoryTheory.NatTrans.instIsClosedUnderLimitsOfShapeOverFunctorEquifiberedHomDiscretePUnitOfHasCoproductsOfShapeHom, isClosedUnderLimitsOfShape_op_iff_unop, CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful, instIsClosedUnderLimitsOfShapeBotOfNonempty, IsClosedUnderLimitsOfShape.mk', CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_discrete_empty, instIsClosedUnderLimitsOfShapeLimitClosure, CochainComplex.Plus.instIsClosedUnderLimitsOfShapeIntPlusOfFinCategoryOfHasLimitsOfShape, instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape_1, IsClosedUnderFiniteProducts.isClosedUnderLimitsOfShape, isClosedUnderLimitsOfShape_inverseImage_iff, isClosedUnderLimitsOfShape_of_preservesLimitsOfShape_ι, CategoryTheory.Over.closedUnderLimitsOfShape_pullback, isClosedUnderColimitsOfShape_op_iff_unop, CategoryTheory.Over.closedUnderLimitsOfShape_discrete_empty, instIsClosedUnderLimitsOfShapeDiscreteOfIsClosedUnderFiniteProductsOfFinite, instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape, instIsClosedUnderLimitsOfShapeUnopOfIsClosedUnderColimitsOfShapeOpposite, instIsClosedUnderLimitsOfShapeLimitsClosure, IsClosedUnderLimitsOfShape.inverseImage, CategoryTheory.Sheaf.instIsClosedUnderLimitsOfShapeFunctorOppositeIsSheaf, isClosedUnderColimitsOfShape_op_iff_op, isClosedUnderLimitsOfShape_op_iff_op, instIsClosedUnderLimitsOfShapeDiscretePEmptyOfContainsZeroOfIsClosedUnderIsomorphisms, CategoryTheory.MorphismProperty.instIsClosedUnderLimitsOfShapeIsLocal, isClosedUnderColimitsOfShape_iff_unop, isClosedUnderLimitsOfShape_iff_of_equivalence, isClosedUnderLimitsOfShape_iff, IsClosedUnderLimitsOfShape.of_equivalence, isClosedUnderLimitsOfShape_iff_unop, CategoryTheory.MonoOver.instIsClosedUnderLimitsOfShapeOverIsMono, isClosedUnderLimitsOfShape_iff_op
LimitOfShape 📖	CompData	—
limitsOfShape 📖	CompOp	16 math math: colimitsOfShape_op, limitsOfShape_isoClosure, limitsOfShape_op, LimitOfShape.limitsOfShape, instEssentiallySmallLimitsOfShapeOfSmallOfSmallOfLocallySmall, instIsClosedUnderIsomorphismsLimitsOfShape, limitsOfShape_bot, strictLimitsOfShape_le_limitsOfShape, limitsOfShape_eq_unop_colimitsOfShape, isoClosure_strictLimitsOfShape, limitsOfShape_monotone, limitsOfShape_congr, colimitsOfShape_eq_unop_limitsOfShape, IsClosedUnderLimitsOfShape.limitsOfShape_le, limitsOfShape_le_of_initial, isClosedUnderLimitsOfShape_iff
strictLimitsOfShape 📖	CompData	5 math math: strictLimitsOfShape_le_limitsOfShape, strictLimitsOfShape_monotone, strictLimitsOfShape_bot, isoClosure_strictLimitsOfShape, instSmallStrictLimitsOfShapeOfSmallOfLocallySmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEssentiallySmallLimitsOfShapeOfSmallOfSmallOfLocallySmall 📖	mathematical	—	EssentiallySmall limitsOfShape	—	isoClosure_strictLimitsOfShape instEssentiallySmallIsoClosure instEssentiallySmallOfSmall instSmallStrictLimitsOfShapeOfSmallOfLocallySmall
instIsClosedUnderIsomorphismsLimitsOfShape 📖	mathematical	—	IsClosedUnderIsomorphisms limitsOfShape	—	—
instIsClosedUnderLimitsOfShapeBotOfNonempty 📖	mathematical	—	IsClosedUnderLimitsOfShape Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	limitsOfShape_bot le_refl
instIsClosedUnderLimitsOfShapeTop 📖	mathematical	—	IsClosedUnderLimitsOfShape Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	—
instSmallStrictLimitsOfShapeOfSmallOfLocallySmall 📖	mathematical	—	Small strictLimitsOfShape	—	small_of_surjective small_subtype CategoryTheory.instSmallFunctorOfLocallySmall instSmallFullSubcategoryOfSmall CategoryTheory.locallySmall_fullSubcategory FullSubcategory.property
isClosedUnderLimitsOfShape_iff 📖	mathematical	—	IsClosedUnderLimitsOfShape CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le limitsOfShape	—	—
isClosedUnderLimitsOfShape_iff_of_equivalence 📖	mathematical	—	IsClosedUnderLimitsOfShape	—	limitsOfShape_congr
isClosedUnderLimitsOfShape_inverseImage_iff 📖	mathematical	—	IsClosedUnderLimitsOfShape inverseImage CategoryTheory.Equivalence.functor	—	prop_iff_of_iso IsClosedUnderLimitsOfShape.inverseImage CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Equivalence.isEquivalence_functor
isoClosure_strictLimitsOfShape 📖	mathematical	—	isoClosure strictLimitsOfShape limitsOfShape	—	le_antisymm isoClosure_le_iff instIsClosedUnderIsomorphismsLimitsOfShape strictLimitsOfShape_le_limitsOfShape CategoryTheory.Limits.LimitPresentation.hasLimit LimitOfShape.prop_diag_obj
limitsOfShape_bot 📖	mathematical	—	limitsOfShape Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	eq_bot_iff
limitsOfShape_congr 📖	mathematical	—	limitsOfShape	—	le_antisymm limitsOfShape_le_of_initial CategoryTheory.Functor.initial_of_isLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Equivalence.isEquivalence_functor
limitsOfShape_isoClosure 📖	mathematical	—	limitsOfShape isoClosure	—	le_antisymm LimitOfShape.prop_diag_obj limitsOfShape_monotone le_isoClosure
limitsOfShape_le_of_initial 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le limitsOfShape	—	—
limitsOfShape_monotone 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le limitsOfShape	—	—
prop_limit 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Limits.limit	—	prop_of_isLimit
prop_of_isLimit 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Limits.Cone.pt	—	IsClosedUnderLimitsOfShape.limitsOfShape_le
prop_pi 📖	mathematical	—	CategoryTheory.Limits.piObj	—	prop_of_isLimit
strictLimitsOfShape_bot 📖	mathematical	—	strictLimitsOfShape Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	eq_bot_iff
strictLimitsOfShape_le_limitsOfShape 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le strictLimitsOfShape limitsOfShape	—	—
strictLimitsOfShape_monotone 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le strictLimitsOfShape	—	—

CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inverseImage 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape CategoryTheory.ObjectProperty.inverseImage	—	CategoryTheory.ObjectProperty.LimitOfShape.prop
limitsOfShape_le 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.ObjectProperty.limitsOfShape	—	—
mk' 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.ObjectProperty.strictLimitsOfShape	CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape	—	CategoryTheory.ObjectProperty.isoClosure_eq_self CategoryTheory.ObjectProperty.isoClosure_strictLimitsOfShape CategoryTheory.ObjectProperty.monotone_isoClosure
of_equivalence 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape	—	CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_of_equivalence

CategoryTheory.ObjectProperty.LimitOfShape

Definitions

Name	Category	Theorems
limit 📖	CompOp	—
ofIso 📖	CompOp	1 math math: ofIso_toLimitPresentation
ofLE 📖	CompOp	1 math math: ofLE_toLimitPresentation
reindex 📖	CompOp	1 math math: reindex_toLimitPresentation
toLimitPresentation 📖	CompOp	6 math math: prop_diag_obj, reindex_toLimitPresentation, ofIso_toLimitPresentation, ofLE_toLimitPresentation, toStructuredArrow_obj, toStructuredArrow_map
toStructuredArrow 📖	CompOp	2 math math: toStructuredArrow_obj, toStructuredArrow_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
limitsOfShape 📖	mathematical	—	CategoryTheory.ObjectProperty.limitsOfShape	—	—
ofIso_toLimitPresentation 📖	mathematical	—	toLimitPresentation ofIso CategoryTheory.Limits.LimitPresentation.ofIso	—	—
ofLE_toLimitPresentation 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	toLimitPresentation ofLE	—	—
prop 📖	—	—	—	—	CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.limitsOfShape_le
prop_diag_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.LimitPresentation.diag toLimitPresentation	—	—
reindex_toLimitPresentation 📖	mathematical	—	toLimitPresentation reindex CategoryTheory.Limits.LimitPresentation.reindex	—	—
toStructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.StructuredArrow CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.StructuredArrow.homMk CategoryTheory.Functor.obj CategoryTheory.Limits.LimitPresentation.diag toLimitPresentation prop_diag_obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.LimitPresentation.π CategoryTheory.ObjectProperty.homMk CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	prop_diag_obj
toStructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.StructuredArrow CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι CategoryTheory.instCategoryStructuredArrow toStructuredArrow CategoryTheory.Limits.LimitPresentation.diag toLimitPresentation prop_diag_obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.LimitPresentation.π	—	—

---

← Back to Index