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 #
has_lifting_property: the definition of the lifting property
Tags #
lifting property
@TODO :
- define llp/rlp with respect to a
morphism_property - retracts, direct/inverse images, (co)products, adjunctions
@[class]
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) :
Prop
- sq_has_lift : ∀ {f : A ⟶ X} {g : B ⟶ Y} (sq : category_theory.comm_sq f i p g), sq.has_lift
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.
@[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] :
sq.has_lift
theorem
category_theory.has_lifting_property.op
{C : Type u_1}
[category_theory.category C]
{A B X Y : C}
{i : A ⟶ B}
{p : X ⟶ Y}
(h : category_theory.has_lifting_property i p) :
theorem
category_theory.has_lifting_property.unop
{C : Type u_1}
[category_theory.category C]
{A B X Y : Cᵒᵖ}
{i : A ⟶ B}
{p : X ⟶ Y}
(h : category_theory.has_lifting_property i p) :
theorem
category_theory.has_lifting_property.iff_op
{C : Type u_1}
[category_theory.category C]
{A B X Y : C}
{i : A ⟶ B}
{p : X ⟶ Y} :
theorem
category_theory.has_lifting_property.iff_unop
{C : Type u_1}
[category_theory.category C]
{A B X Y : Cᵒᵖ}
(i : A ⟶ B)
(p : X ⟶ Y) :
@[protected, instance]
def
category_theory.has_lifting_property.of_left_iso
{C : Type u_1}
[category_theory.category C]
{A B X Y : C}
(i : A ⟶ B)
(p : X ⟶ Y)
[category_theory.is_iso i] :
@[protected, instance]
def
category_theory.has_lifting_property.of_right_iso
{C : Type u_1}
[category_theory.category C]
{A B X Y : C}
(i : A ⟶ B)
(p : X ⟶ Y)
[category_theory.is_iso p] :
@[protected, instance]
def
category_theory.has_lifting_property.of_comp_left
{C : Type u_1}
[category_theory.category C]
{A B B' X Y : C}
(i : A ⟶ B)
(i' : B ⟶ B')
(p : X ⟶ Y)
[category_theory.has_lifting_property i p]
[category_theory.has_lifting_property i' p] :
category_theory.has_lifting_property (i ≫ i') p
@[protected, instance]
def
category_theory.has_lifting_property.of_comp_right
{C : Type u_1}
[category_theory.category C]
{A B X Y Y' : C}
(i : A ⟶ B)
(p : X ⟶ Y)
(p' : Y ⟶ Y')
[category_theory.has_lifting_property i p]
[category_theory.has_lifting_property i p'] :
category_theory.has_lifting_property i (p ≫ p')
theorem
category_theory.has_lifting_property.of_arrow_iso_left
{C : Type u_1}
[category_theory.category C]
{A B A' B' X Y : C}
{i : A ⟶ B}
{i' : A' ⟶ B'}
(e : category_theory.arrow.mk i ≅ category_theory.arrow.mk i')
(p : X ⟶ Y)
[hip : category_theory.has_lifting_property i p] :
theorem
category_theory.has_lifting_property.of_arrow_iso_right
{C : Type u_1}
[category_theory.category C]
{A B X Y X' Y' : C}
(i : A ⟶ B)
{p : X ⟶ Y}
{p' : X' ⟶ Y'}
(e : category_theory.arrow.mk p ≅ category_theory.arrow.mk p')
[hip : category_theory.has_lifting_property i p] :
theorem
category_theory.has_lifting_property.iff_of_arrow_iso_left
{C : Type u_1}
[category_theory.category C]
{A B A' B' X Y : C}
{i : A ⟶ B}
{i' : A' ⟶ B'}
(e : category_theory.arrow.mk i ≅ category_theory.arrow.mk i')
(p : X ⟶ Y) :
theorem
category_theory.has_lifting_property.iff_of_arrow_iso_right
{C : Type u_1}
[category_theory.category C]
{A B X Y X' Y' : C}
(i : A ⟶ B)
{p : X ⟶ Y}
{p' : X' ⟶ Y'}
(e : category_theory.arrow.mk p ≅ category_theory.arrow.mk p') :