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} [Category.{v, u} C] (T : MorphismProperty C) : 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} [Category.{v, u} C] (T : MorphismProperty C) : 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_of_isIso {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) {A B : C} (i : A ⟶ B) [IsIso i] : T.llp i

theorem CategoryTheory.MorphismProperty.rlp_of_isIso {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) {X Y : C} (f : X ⟶ Y) [IsIso f] : T.rlp f

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

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

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

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

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

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

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

instance CategoryTheory.MorphismProperty.instIsStableUnderCoproductsLlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : IsStableUnderCoproducts.{w, v, u} T.llp

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

theorem CategoryTheory.MorphismProperty.le_llp_iff_le_rlp {C : Type u} [Category.{v, u} C] (T T' : MorphismProperty C) : T ≤ T'.llp ↔ T' ≤ T.rlp

theorem CategoryTheory.MorphismProperty.gc_llp_rlp {C : Type u} [Category.{v, u} C] : GaloisConnection (⇑OrderDual.toDual ∘ llp) (rlp ∘ ⇑OrderDual.ofDual)

theorem CategoryTheory.MorphismProperty.le_llp_rlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : T ≤ T.rlp.llp

@[simp]

theorem CategoryTheory.MorphismProperty.rlp_llp_rlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : T.rlp.llp.rlp = T.rlp

@[simp]

theorem CategoryTheory.MorphismProperty.llp_rlp_llp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : T.llp.rlp.llp = T.llp

theorem CategoryTheory.MorphismProperty.antitone_rlp {C : Type u} [Category.{v, u} C] : Antitone rlp

theorem CategoryTheory.MorphismProperty.antitone_llp {C : Type u} [Category.{v, u} C] : Antitone llp

theorem CategoryTheory.MorphismProperty.pushouts_le_llp_rlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : T.pushouts ≤ T.rlp.llp

@[simp]

theorem CategoryTheory.MorphismProperty.rlp_pushouts {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : T.pushouts.rlp = T.rlp

theorem CategoryTheory.MorphismProperty.colimitsOfShape_discrete_le_llp_rlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) (J : Type w) : T.colimitsOfShape (Discrete J) ≤ T.rlp.llp

theorem CategoryTheory.MorphismProperty.coproducts_le_llp_rlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : coproducts.{w, v, u} T ≤ T.rlp.llp

@[simp]

theorem CategoryTheory.MorphismProperty.rlp_coproducts {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : (coproducts.{w, v, u} T).rlp = T.rlp

theorem CategoryTheory.MorphismProperty.retracts_le_llp_rlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : T.retracts ≤ T.rlp.llp

@[simp]

theorem CategoryTheory.MorphismProperty.rlp_retracts {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) : T.retracts.rlp = T.rlp

theorem CategoryTheory.MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty {C : Type u} [Category.{v, u} C] (ι : Type u_1) [Nonempty ι] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) : (ofHoms fun (x : ι) => i).rlp p ↔ HasLiftingProperty i p

theorem CategoryTheory.MorphismProperty.llp_ofHoms_iff_hasLiftingProperty {C : Type u} [Category.{v, u} C] (ι : Type u_1) [Nonempty ι] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) : (ofHoms fun (x : ι) => p).llp i ↔ HasLiftingProperty i p

theorem CategoryTheory.Functor.hasLiftingProperty_iff_of_isEquivalence {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (G : Functor C D) [G.IsEquivalence] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) : HasLiftingProperty (G.map i) (G.map p) ↔ HasLiftingProperty i p