RetractArgument

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

Statistics

Metric	Count
Definitions ofLeftLiftingProperty, ofRightLiftingProperty	2
Theorems llp_eq_of_le_llp_of_hasFactorization_of_isStableUnderRetracts, rlp_eq_of_le_rlp_of_hasFactorization_of_isStableUnderRetracts	2
Total	4

CategoryTheory.MorphismProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
llp_eq_of_le_llp_of_hasFactorization_of_isStableUnderRetracts 📖	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra llp	—	—	le_antisymm MapFactorizationData.hp of_retract MapFactorizationData.fac MapFactorizationData.hi
rlp_eq_of_le_rlp_of_hasFactorization_of_isStableUnderRetracts 📖	—	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice instCompleteBooleanAlgebra rlp	—	—	le_antisymm MapFactorizationData.hi of_retract MapFactorizationData.fac MapFactorizationData.hp

CategoryTheory.RetractArrow

Definitions

Name	Category	Theorems
ofLeftLiftingProperty 📖	CompOp	—
ofRightLiftingProperty 📖	CompOp	—

---

← Back to Index