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.

Instances
    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] :
    Equations