Left and right lifting properties

Given a morphism property T, we define the left and right lifting property with respect to T.

We show that the left lifting property is stable under retracts, cobase change, coproducts, and composition, with dual statements for the right lifting property.

def CategoryTheory.MorphismProperty.llp {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty C

Given T : MorphismProperty C, this is the class of morphisms that have the left lifting property (llp) with respect to T.

Equations

• T.llp f = ∀ ⦃X Y : C⦄ (g : X ⟶ Y), T g → CategoryTheory.HasLiftingProperty f g

def CategoryTheory.MorphismProperty.rlp {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) : CategoryTheory.MorphismProperty C

Given T : MorphismProperty C, this is the class of morphisms that have the right lifting property (rlp) with respect to T.

Equations

• T.rlp f = ∀ ⦃X Y : C⦄ (g : X ⟶ Y), T g → CategoryTheory.HasLiftingProperty g f

theorem CategoryTheory.MorphismProperty.llp_isStableUnderRetracts {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) : T.llp.IsStableUnderRetracts

theorem CategoryTheory.MorphismProperty.rlp_isStableUnderRetracts {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) : T.rlp.IsStableUnderRetracts

instance CategoryTheory.MorphismProperty.llp_isStableUnderCobaseChange {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) : T.llp.IsStableUnderCobaseChange

instance CategoryTheory.MorphismProperty.rlp_isStableUnderBaseChange {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) : T.rlp.IsStableUnderBaseChange

instance CategoryTheory.MorphismProperty.llp_isMultiplicative {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) : T.llp.IsMultiplicative

instance CategoryTheory.MorphismProperty.rlp_isMultiplicative {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) : T.rlp.IsMultiplicative

theorem CategoryTheory.MorphismProperty.llp_IsStableUnderCoproductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) (J : Type u_1) : T.llp.IsStableUnderCoproductsOfShape J

theorem CategoryTheory.MorphismProperty.rlp_IsStableUnderProductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C) (J : Type u_1) : T.rlp.IsStableUnderProductsOfShape J