mathlib3 documentation


Lifting properties #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

Tags #

lifting property


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

has_lifting_property 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 of this typeclass
@[protected, instance]
def category_theory.sq_has_lift_of_has_lifting_property {C : Type u_1} [category_theory.category C] {A B X Y : C} (i : A B) (p : X Y) {f : A X} {g : B Y} (sq : category_theory.comm_sq f i p g) [hip : category_theory.has_lifting_property i p] :