The retract argument

Let W₁ and W₂ be classes of morphisms in a category C such that any morphism can be factored as a morphism in W₁ followed by a morphism in W₂ (this is HasFactorization W₁ W₂). If W₁ has the left lifting property with respect to W₂ (i.e. W₁ ≤ W₂.llp, or equivalently W₂ ≤ W₁.rlp), then W₂.llp = W₁ if W₁ is stable under retracts, and W₁.rlp = W₂ if W₂ is.

Reference

• https://ncatlab.org/nlab/show/weak+factorization+system#retract_argument

noncomputable def CategoryTheory.RetractArrow.ofLeftLiftingProperty {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z : C} {f : X ⟶ Z} {i : X ⟶ Y} {p : Y ⟶ Z} (h : CategoryStruct.comp i p = f) [HasLiftingProperty f p] : RetractArrow f i

If i ≫ p = f, and f has the left lifting property with respect to p, then f is a retract of i.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.RetractArrow.ofRightLiftingProperty {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z : C} {f : X ⟶ Z} {i : X ⟶ Y} {p : Y ⟶ Z} (h : CategoryStruct.comp i p = f) [HasLiftingProperty i f] : RetractArrow f p

If i ≫ p = f, and f has the right lifting property with respect to i, then f is a retract of p.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.MorphismProperty.llp_eq_of_le_llp_of_hasFactorization_of_isStableUnderRetracts {C : Type u_1} [Category.{u_2, u_1} C] {W₁ W₂ : MorphismProperty C} [W₁.HasFactorization W₂] [W₁.IsStableUnderRetracts] (h₁ : W₁ ≤ W₂.llp) : W₂.llp = W₁

theorem CategoryTheory.MorphismProperty.rlp_eq_of_le_rlp_of_hasFactorization_of_isStableUnderRetracts {C : Type u_1} [Category.{u_2, u_1} C] {W₁ W₂ : MorphismProperty C} [W₁.HasFactorization W₂] [W₂.IsStableUnderRetracts] (h₂ : W₂ ≤ W₁.rlp) : W₁.rlp = W₂