Documentation Verification Report

FullSubcategory

📁 Source: Mathlib/CategoryTheory/Limits/FullSubcategory.lean

Statistics

Metric	Count
Definitions `createsColimitFullSubcategoryInclusion`, `createsColimitFullSubcategoryInclusion'`, `createsColimitFullSubcategoryInclusionOfClosed`, `createsColimitsOfShapeFullSubcategoryInclusion`, `createsLimitFullSubcategoryInclusion`, `createsLimitFullSubcategoryInclusion'`, `createsLimitFullSubcategoryInclusionOfClosed`, `createsLimitsOfShapeFullSubcategoryInclusion`	8
Theorems `hasColimit_of_closedUnderColimits`, `hasColimitsOfShape_of_closedUnderColimits`, `hasLimit_of_closedUnderLimits`, `hasLimitsOfShape_of_closedUnderLimits`, `instIsClosedUnderColimitsOfShapeEssImageOfHasColimitsOfShapeOfPreservesColimitsOfShapeOfFullOfFaithful`, `instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful`, `isClosedUnderColimitsOfShape_of_preservesColimitsOfShape_ι`, `isClosedUnderLimitsOfShape_of_preservesLimitsOfShape_ι`	8
Total	16

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`createsColimitFullSubcategoryInclusion` 📖	CompOp	—
`createsColimitFullSubcategoryInclusion'` 📖	CompOp	—
`createsColimitFullSubcategoryInclusionOfClosed` 📖	CompOp	—
`createsColimitsOfShapeFullSubcategoryInclusion` 📖	CompOp	—
`createsLimitFullSubcategoryInclusion` 📖	CompOp	—
`createsLimitFullSubcategoryInclusion'` 📖	CompOp	—
`createsLimitFullSubcategoryInclusionOfClosed` 📖	CompOp	—
`createsLimitsOfShapeFullSubcategoryInclusion` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasColimit_of_closedUnderColimits` 📖	mathematical	—	`HasColimit` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category`	—	`CategoryTheory.hasColimit_of_created`
`hasColimitsOfShape_of_closedUnderColimits` 📖	mathematical	—	`HasColimitsOfShape` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category`	—	`hasColimit_of_closedUnderColimits` `hasColimitOfHasColimitsOfShape`
`hasLimit_of_closedUnderLimits` 📖	mathematical	—	`HasLimit` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category`	—	`CategoryTheory.hasLimit_of_created`
`hasLimitsOfShape_of_closedUnderLimits` 📖	mathematical	—	`HasLimitsOfShape` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category`	—	`hasLimit_of_closedUnderLimits` `hasLimitOfHasLimitsOfShape`
`instIsClosedUnderColimitsOfShapeEssImageOfHasColimitsOfShapeOfPreservesColimitsOfShapeOfFullOfFaithful` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape` `CategoryTheory.Functor.essImage`	—	`CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.mk'` `CategoryTheory.Functor.instIsClosedUnderIsomorphismsEssImage` `hasColimitOfHasColimitsOfShape` `PreservesColimitsOfShape.preservesColimit`
`instIsClosedUnderLimitsOfShapeEssImageOfHasLimitsOfShapeOfPreservesLimitsOfShapeOfFullOfFaithful` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape` `CategoryTheory.Functor.essImage`	—	`CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk'` `CategoryTheory.Functor.instIsClosedUnderIsomorphismsEssImage` `hasLimitOfHasLimitsOfShape` `PreservesLimitsOfShape.preservesLimit`

CategoryTheory.ObjectProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosedUnderColimitsOfShape_of_preservesColimitsOfShape_ι` 📖	mathematical	—	`IsClosedUnderColimitsOfShape`	—	`prop_of_iso` `ColimitOfShape.prop_diag_obj` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit` `FullSubcategory.property`
`isClosedUnderLimitsOfShape_of_preservesLimitsOfShape_ι` 📖	mathematical	—	`IsClosedUnderLimitsOfShape`	—	`prop_of_iso` `LimitOfShape.prop_diag_obj` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit` `FullSubcategory.property`

---

← Back to Index