Documentation Verification Report

LimitsOfShape

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

Statistics

Metric	Count
Definitions `ClosedUnderLimitsOfShape`, `IsClosedUnderLimitsOfShape`, `LimitOfShape`, `limit`, `ofIso`, `ofLE`, `reindex`, `toLimitPresentation`, `toStructuredArrow`, `limitsOfShape`, `strictLimitsOfShape`	11
Theorems `limit`, `closedUnderLimitsOfShape_of_limit`, `inverseImage`, `limitsOfShape_le`, `mk'`, `of_equivalence`, `limitsOfShape`, `ofIso_toLimitPresentation`, `ofLE_toLimitPresentation`, `prop`, `prop_diag_obj`, `reindex_toLimitPresentation`, `toStructuredArrow_map`, `toStructuredArrow_obj`, `instEssentiallySmallLimitsOfShapeOfSmallOfSmallOfLocallySmall`, `instIsClosedUnderIsomorphismsLimitsOfShape`, `instSmallStrictLimitsOfShapeOfSmallOfLocallySmall`, `isClosedUnderLimitsOfShape_iff`, `isClosedUnderLimitsOfShape_iff_of_equivalence`, `isClosedUnderLimitsOfShape_inverseImage_iff`, `isoClosure_strictLimitsOfShape`, `limitsOfShape_congr`, `limitsOfShape_isoClosure`, `limitsOfShape_le_of_initial`, `limitsOfShape_monotone`, `prop_limit`, `prop_of_isLimit`, `prop_pi`, `strictLimitsOfShape_le_limitsOfShape`, `strictLimitsOfShape_monotone`	30
Total	41

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`ClosedUnderLimitsOfShape` 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedUnderLimitsOfShape_of_limit` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `CategoryTheory.ObjectProperty.strictLimitsOfShape`	`CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape`	—	`CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk'`

CategoryTheory.Limits.ClosedUnderLimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`limit` 📖	mathematical	`CategoryTheory.Functor.obj`	`CategoryTheory.Limits.limit`	—	`CategoryTheory.ObjectProperty.prop_limit`

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`IsClosedUnderLimitsOfShape` 📖	CompData	34 math math: `instIsClosedUnderLimitsOfShapeUnopOppositeOfIsClosedUnderColimitsOfShape`, `isClosedUnderColimitsOfShape_iff_op`, `CategoryTheory.Limits.isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair`, `CategoryTheory.instIsClosedUnderLimitsOfShapeFunctorOppositeTypeIsIndObjectDiscreteOfHasLimitsOfShape`, `CategoryTheory.Limits.closedUnderLimitsOfShape_walkingParallelPair_isIndObject`, `CategoryTheory.NatTrans.instIsClosedUnderLimitsOfShapeOverFunctorEquifiberedHomDiscretePUnitOfHasCoproductsOfShapeHom`, `isClosedUnderLimitsOfShape_op_iff_unop`, `CategoryTheory.Limits.instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful`, `IsClosedUnderLimitsOfShape.mk'`, `CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_discrete_empty`, `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`, `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.Limits.closedUnderLimitsOfShape_of_limit`, `CategoryTheory.MonoOver.instIsClosedUnderLimitsOfShapeOverIsMono`, `isClosedUnderLimitsOfShape_iff_op`
`LimitOfShape` 📖	CompData	—
`limitsOfShape` 📖	CompOp	15 math math: `colimitsOfShape_op`, `limitsOfShape_isoClosure`, `limitsOfShape_op`, `LimitOfShape.limitsOfShape`, `instEssentiallySmallLimitsOfShapeOfSmallOfSmallOfLocallySmall`, `instIsClosedUnderIsomorphismsLimitsOfShape`, `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	4 math math: `strictLimitsOfShape_le_limitsOfShape`, `strictLimitsOfShape_monotone`, `isoClosure_strictLimitsOfShape`, `instSmallStrictLimitsOfShapeOfSmallOfLocallySmall`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEssentiallySmallLimitsOfShapeOfSmallOfSmallOfLocallySmall` 📖	mathematical	—	`EssentiallySmall` `limitsOfShape`	—	`isoClosure_strictLimitsOfShape` `instEssentiallySmallIsoClosure` `instEssentiallySmallOfSmall` `instSmallStrictLimitsOfShapeOfSmallOfLocallySmall`
`instIsClosedUnderIsomorphismsLimitsOfShape` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `limitsOfShape`	—	—
`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_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`	`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_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`	`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