Documentation Verification Report

Retract

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

Statistics

Metric	Count
Definitions `IsStableUnderRetracts`, `retractClosure`	2
Theorems `containsZero`, `instIsClosedUnderIsomorphisms`, `of_bicone`, `of_binaryBicone_left`, `of_binaryBicone_right`, `of_biprod_left`, `of_biprod_right`, `of_biproduct`, `of_retract`, `instEssentiallySmallRetractClosureOfLocallySmall`, `instIsStableUnderRetractsBot`, `instIsStableUnderRetractsRetractClosure`, `instIsStableUnderRetractsTop`, `le_retractClosure`, `monotone_retractClosure`, `prop_of_retract`, `prop_retractClosure`, `prop_retractClosure_iff`, `retractClosure_bot`, `retractClosure_eq_self`, `retractClosure_isoClosure`, `retractClosure_le_iff`, `retractClosure_top`	23
Total	25

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`IsStableUnderRetracts` 📖	CompData	7 math math: `CategoryTheory.instIsStableUnderRetractsIsCardinalPresentable`, `instIsStableUnderRetractsTop`, `isStableUnderRetracts_colimitsCardinalClosure`, `instIsStableUnderRetractsBot`, `instIsStableUnderRetractsOfIsClosedUnderColimitsOfShapeWalkingParallelPair`, `CategoryTheory.instIsStableUnderRetractsIsInternallyProjective`, `instIsStableUnderRetractsRetractClosure`
`retractClosure` 📖	CompOp	16 math math: `monotone_retractClosure`, `IsCardinalFilteredGenerator.isPresentable_eq_retractClosure`, `retractClosure_bot`, `prop_retractClosure_iff`, `retractClosure_eq_self`, `retractClosure_le_iff`, `retractClosure_extensionProduct_retractClosure_retractClosure`, `retractClosure_isoClosure`, `extensionProductIter_retractClosure_le`, `instIsStableUnderRetractsRetractClosure`, `extensionProduct_retractClosure_retractClosure_le`, `prop_retractClosure`, `le_retractClosure`, `instEssentiallySmallRetractClosureOfLocallySmall`, `retractClosure_extensionProductIter_retractClosure`, `retractClosure_top`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEssentiallySmallRetractClosureOfLocallySmall` 📖	mathematical	—	`EssentiallySmall` `retractClosure`	—	`EssentiallySmall.exists_small_le` `CategoryTheory.Category.assoc` `CategoryTheory.Retract.retract_assoc` `instSmallOfObjOfSmall` `small_subtype` `small_sigma` `CategoryTheory.instSmallHomOfLocallySmall` `LE.le.trans` `monotone_retractClosure` `retractClosure_isoClosure` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Retract.retract` `CategoryTheory.Category.comp_id`
`instIsStableUnderRetractsBot` 📖	mathematical	—	`IsStableUnderRetracts` `Bot.bot` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instBotForall` `BooleanAlgebra.toBot` `Prop.instBooleanAlgebra`	—	—
`instIsStableUnderRetractsRetractClosure` 📖	mathematical	—	`IsStableUnderRetracts` `retractClosure`	—	—
`instIsStableUnderRetractsTop` 📖	mathematical	—	`IsStableUnderRetracts` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	—
`le_retractClosure` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `retractClosure`	—	—
`monotone_retractClosure` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `retractClosure`	—	—
`prop_of_retract` 📖	—	—	—	—	`IsStableUnderRetracts.of_retract`
`prop_retractClosure` 📖	mathematical	—	`retractClosure`	—	—
`prop_retractClosure_iff` 📖	mathematical	—	`retractClosure` `CategoryTheory.Retract`	—	—
`retractClosure_bot` 📖	mathematical	—	`retractClosure` `Bot.bot` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instBotForall` `BooleanAlgebra.toBot` `Prop.instBooleanAlgebra`	—	`retractClosure_eq_self` `instIsStableUnderRetractsBot`
`retractClosure_eq_self` 📖	mathematical	—	`retractClosure`	—	`le_antisymm` `prop_of_retract` `le_retractClosure`
`retractClosure_isoClosure` 📖	mathematical	—	`retractClosure` `isoClosure`	—	`le_antisymm` `monotone_retractClosure` `le_isoClosure`
`retractClosure_le_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `retractClosure`	—	`LE.le.trans` `le_retractClosure` `monotone_retractClosure` `retractClosure_eq_self` `le_refl`
`retractClosure_top` 📖	mathematical	—	`retractClosure` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	`retractClosure_eq_self` `instIsStableUnderRetractsTop`

CategoryTheory.ObjectProperty.IsStableUnderRetracts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`containsZero` 📖	mathematical	—	`CategoryTheory.ObjectProperty.ContainsZero`	—	`CategoryTheory.Limits.isZero_zero` `of_retract`
`instIsClosedUnderIsomorphisms` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms`	—	`of_retract`
`of_bicone` 📖	—	`CategoryTheory.Limits.Bicone.pt`	—	—	`of_retract`
`of_binaryBicone_left` 📖	—	`CategoryTheory.Limits.BinaryBicone.pt`	—	—	`of_retract`
`of_binaryBicone_right` 📖	—	`CategoryTheory.Limits.BinaryBicone.pt`	—	—	`of_retract`
`of_biprod_left` 📖	—	`CategoryTheory.Limits.biprod`	—	—	`of_binaryBicone_left`
`of_biprod_right` 📖	—	`CategoryTheory.Limits.biprod`	—	—	`of_binaryBicone_right`
`of_biproduct` 📖	—	`CategoryTheory.Limits.biproduct`	—	—	`of_bicone`
`of_retract` 📖	—	—	—	—	—

---

← Back to Index