Documentation

Mathlib.CategoryTheory.LiftingProperties.Basic

Lifting properties #

This file defines the lifting property of two morphisms in a category and shows basic properties of this notion.

Main results #

Tags #

lifting property

@TODO :

  1. define llp/rlp with respect to a morphism_property
  2. retracts, direct/inverse images, (co)products, adjunctions
class CategoryTheory.HasLiftingProperty {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} (i : A B) (p : X Y) :

HasLiftingProperty i p means that i has the left lifting property with respect to p, or equivalently that p has the right lifting property with respect to i.

  • sq_hasLift : ∀ {f : A X} {g : B Y} (sq : CategoryTheory.CommSq f i p g), sq.HasLift

    Unique field expressing that any commutative square built from f and g has a lift

Instances
    theorem CategoryTheory.HasLiftingProperty.sq_hasLift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} {i : A B} {p : X Y} [self : CategoryTheory.HasLiftingProperty i p] {f : A X} {g : B Y} (sq : CategoryTheory.CommSq f i p g) :
    sq.HasLift

    Unique field expressing that any commutative square built from f and g has a lift

    @[instance 100]
    instance CategoryTheory.sq_hasLift_of_hasLiftingProperty {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A : C} {B : C} {X : C} {Y : C} (i : A B) (p : X Y) {f : A X} {g : B Y} (sq : CategoryTheory.CommSq f i p g) [hip : CategoryTheory.HasLiftingProperty i p] :
    sq.HasLift
    Equations
    • =
    @[instance 100]
    Equations
    • =
    @[instance 100]
    Equations
    • =