Documentation Verification Report

Retract

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

Statistics

Metric	Count
Definitions `IsStableUnderRetracts`, `retracts`	2
Theorems `epimorphisms`, `isomorphisms`, `monomorphisms`, `of_retract`, `instIsStableUnderRetractsInverseImage`, `instIsStableUnderRetractsMin`, `instIsStableUnderRetractsOppositeOp`, `instIsStableUnderRetractsUnopOfOpposite`, `instRespectsIsoOfIsStableUnderRetracts`, `isStableUnderRetracts_iff`, `isStableUnderRetracts_iff_retracts_le`, `le_retracts`, `of_retract`, `retracts_le`, `retracts_le_iff`, `retracts_monotone`	16
Total	18

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`IsStableUnderRetracts` 📖	CompData	27 math math: `CategoryTheory.ObjectProperty.instIsStableUnderRetractsIsoModSerre`, `isStableUnderRetracts_iff`, `HomologicalComplex.instIsStableUnderRetractsQuasiIso`, `llp_isStableUnderRetracts`, `HomotopicalAlgebra.instIsStableUnderRetractsOverFibrations`, `isStableUnderRetracts_iff_retracts_le`, `HomotopicalAlgebra.ModelCategory.cm3b`, `HomotopicalAlgebra.ModelCategory.cm3c`, `instIsStableUnderRetractsUnopOfOpposite`, `HomotopicalAlgebra.instIsStableUnderRetractsOverCofibrations`, `instIsStableUnderRetractsMin`, `instIsStableUnderRetractsInverseImage`, `CategoryTheory.ObjectProperty.instIsStableUnderRetractsEpiModSerre`, `IsStableUnderRetracts.epimorphisms`, `CategoryTheory.ObjectProperty.instIsStableUnderRetractsMonoModSerre`, `HomotopicalAlgebra.instIsStableUnderRetractsOppositeWeakEquivalences`, `HomotopicalAlgebra.ModelCategory.cm3a`, `IsStableUnderRetracts.isomorphisms`, `HomotopicalAlgebra.instIsStableUnderRetractsTrivialCofibrationsOfCofibrationsOfWeakEquivalences`, `HomotopicalAlgebra.instIsStableUnderRetractsOppositeFibrationsOfCofibrations`, `instIsStableUnderRetractsFunctorFunctorCategory`, `rlp_isStableUnderRetracts`, `HomotopicalAlgebra.instIsStableUnderRetractsOppositeCofibrationsOfFibrations`, `instIsStableUnderRetractsOppositeOp`, `HomotopicalAlgebra.instIsStableUnderRetractsTrivialFibrationsOfFibrationsOfWeakEquivalences`, `IsStableUnderRetracts.monomorphisms`, `HomotopicalAlgebra.instIsStableUnderRetractsOverWeakEquivalences`
`retracts` 📖	CompOp	13 math math: `rlp_retracts`, `isStableUnderRetracts_iff_retracts_le`, `retracts_le`, `llp_rlp_of_hasSmallObjectArgument`, `retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp`, `CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument`, `le_retracts`, `retracts_le_iff`, `llp_rlp_of_hasSmallObjectArgument'`, `retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp`, `retracts_le_llp_rlp`, `CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'`, `retracts_monotone`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsStableUnderRetractsInverseImage` 📖	mathematical	—	`IsStableUnderRetracts` `inverseImage`	—	`of_retract`
`instIsStableUnderRetractsMin` 📖	mathematical	—	`IsStableUnderRetracts` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra`	—	`of_retract`
`instIsStableUnderRetractsOppositeOp` 📖	mathematical	—	`IsStableUnderRetracts` `Opposite` `CategoryTheory.Category.opposite` `op` `CategoryTheory.Category.toCategoryStruct`	—	`of_retract`
`instIsStableUnderRetractsUnopOfOpposite` 📖	mathematical	—	`IsStableUnderRetracts` `unop` `CategoryTheory.Category.toCategoryStruct`	—	`of_retract`
`instRespectsIsoOfIsStableUnderRetracts` 📖	mathematical	—	`RespectsIso`	—	`RespectsIso.of_respects_arrow_iso` `of_retract`
`isStableUnderRetracts_iff` 📖	mathematical	—	`IsStableUnderRetracts`	—	—
`isStableUnderRetracts_iff_retracts_le` 📖	mathematical	—	`IsStableUnderRetracts` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `retracts`	—	`isStableUnderRetracts_iff`
`le_retracts` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `retracts`	—	`CategoryTheory.Category.comp_id`
`of_retract` 📖	—	—	—	—	`IsStableUnderRetracts.of_retract`
`retracts_le` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `retracts`	—	`isStableUnderRetracts_iff_retracts_le`
`retracts_le_iff` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `retracts`	—	`le_trans` `le_retracts` `retracts_monotone` `retracts_le`
`retracts_monotone` 📖	mathematical	—	`Monotone` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `retracts`	—	—

CategoryTheory.MorphismProperty.IsStableUnderRetracts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epimorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderRetracts` `CategoryTheory.MorphismProperty.epimorphisms`	—	`CategoryTheory.cancel_epi` `CategoryTheory.Arrow.epi_right` `CategoryTheory.IsSplitEpi.epi` `CategoryTheory.Retract.instIsSplitEpiR` `CategoryTheory.Category.assoc` `CategoryTheory.RetractArrow.r_w`
`isomorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderRetracts` `CategoryTheory.MorphismProperty.isomorphisms`	—	`CategoryTheory.RetractArrow.i_w_assoc` `CategoryTheory.IsIso.hom_inv_id_assoc` `CategoryTheory.RetractArrow.retract_left` `CategoryTheory.Category.assoc` `CategoryTheory.RetractArrow.r_w` `CategoryTheory.IsIso.inv_hom_id_assoc` `CategoryTheory.RetractArrow.retract_right`
`monomorphisms` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderRetracts` `CategoryTheory.MorphismProperty.monomorphisms`	—	`CategoryTheory.cancel_mono` `CategoryTheory.Arrow.mono_left` `CategoryTheory.IsSplitMono.mono` `CategoryTheory.Retract.instIsSplitMonoI` `CategoryTheory.Category.assoc` `CategoryTheory.RetractArrow.i_w` `Mathlib.Tactic.Reassoc.eq_whisker'`
`of_retract` 📖	—	—	—	—	—

---

← Back to Index