Documentation

Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

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.

source
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
Instances For
    source
    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
    Instances For
      source
      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
      source
      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
      source
      instance CategoryTheory.MorphismProperty.llp_isStableUnderRetracts {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.llp.IsStableUnderRetracts
      source
      instance CategoryTheory.MorphismProperty.rlp_isStableUnderRetracts {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.rlp.IsStableUnderRetracts
      source
      instance CategoryTheory.MorphismProperty.llp_isStableUnderCobaseChange {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.llp.IsStableUnderCobaseChange
      source
      instance CategoryTheory.MorphismProperty.rlp_isStableUnderBaseChange {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.rlp.IsStableUnderBaseChange
      source
      instance CategoryTheory.MorphismProperty.llp_isMultiplicative {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.llp.IsMultiplicative
      source
      instance CategoryTheory.MorphismProperty.rlp_isMultiplicative {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.rlp.IsMultiplicative
      source
      instance CategoryTheory.MorphismProperty.llp_isStableUnderCoproductsOfShape {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) (J : Type u_1) :
      T.llp.IsStableUnderCoproductsOfShape J
      source
      instance CategoryTheory.MorphismProperty.rlp_isStableUnderProductsOfShape {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) (J : Type u_1) :
      T.rlp.IsStableUnderProductsOfShape J
      source
      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
      source
      theorem CategoryTheory.MorphismProperty.gc_llp_rlp {C : Type u} [Category.{v, u} C] :
      GaloisConnection (⇑OrderDual.toDual ∘ llp) (rlp ∘ ⇑OrderDual.ofDual)
      source
      theorem CategoryTheory.MorphismProperty.le_llp_rlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T ≤ T.rlp.llp
      source
      @[simp]
      theorem CategoryTheory.MorphismProperty.rlp_llp_rlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.rlp.llp.rlp = T.rlp
      source
      @[simp]
      theorem CategoryTheory.MorphismProperty.llp_rlp_llp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.llp.rlp.llp = T.llp
      source
      theorem CategoryTheory.MorphismProperty.antitone_rlp {C : Type u} [Category.{v, u} C] :
      Antitone rlp
      source
      theorem CategoryTheory.MorphismProperty.antitone_llp {C : Type u} [Category.{v, u} C] :
      Antitone llp
      source
      theorem CategoryTheory.MorphismProperty.pushouts_le_llp_rlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.pushouts ≤ T.rlp.llp
      source
      @[simp]
      theorem CategoryTheory.MorphismProperty.rlp_pushouts {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.pushouts.rlp = T.rlp
      source
      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
      source
      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
      source
      @[simp]
      theorem CategoryTheory.MorphismProperty.rlp_coproducts {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      (coproducts.{w, v, u} T).rlp = T.rlp
      source
      theorem CategoryTheory.MorphismProperty.retracts_le_llp_rlp {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.retracts ≤ T.rlp.llp
      source
      @[simp]
      theorem CategoryTheory.MorphismProperty.rlp_retracts {C : Type u} [Category.{v, u} C] (T : MorphismProperty C) :
      T.retracts.rlp = T.rlp