Documentation

Mathlib.CategoryTheory.MorphismProperty.RetractArgument

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 #

source
noncomputable def CategoryTheory.RetractArrow.ofLeftLiftingProperty {C : Type u_1} [Category.{v_1, 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.
Instances For
    source
    noncomputable def CategoryTheory.RetractArrow.ofRightLiftingProperty {C : Type u_1} [Category.{v_1, 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.
    Instances For
      source
      theorem CategoryTheory.MorphismProperty.llp_eq_of_le_llp_of_hasFactorization_of_isStableUnderRetracts {C : Type u_1} [Category.{v_1, u_1} C] {W₁ W₂ : MorphismProperty C} [W₁.HasFactorization W₂] [W₁.IsStableUnderRetracts] (h₁ : W₁ ≤ W₂.llp) :
      W₂.llp = W₁
      source
      theorem CategoryTheory.MorphismProperty.rlp_eq_of_le_rlp_of_hasFactorization_of_isStableUnderRetracts {C : Type u_1} [Category.{v_1, u_1} C] {W₁ W₂ : MorphismProperty C} [W₁.HasFactorization W₂] [W₂.IsStableUnderRetracts] (h₂ : W₂ ≤ W₁.rlp) :
      W₁.rlp = W₂