Lifting properties #
This file defines the lifting property of two morphisms in a category and shows basic properties of this notion.
Main results #
HasLiftingProperty: 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
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
fandghas a lift
Instances
theorem
CategoryTheory.HasLiftingProperty.sq_hasLift
{C : Type u_1}
:
∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {A B X 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
- ⋯ = ⋯
theorem
CategoryTheory.HasLiftingProperty.op
{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}
(h : CategoryTheory.HasLiftingProperty i p)
:
CategoryTheory.HasLiftingProperty p.op i.op
theorem
CategoryTheory.HasLiftingProperty.unop
{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}
(h : CategoryTheory.HasLiftingProperty i p)
:
CategoryTheory.HasLiftingProperty p.unop i.unop
theorem
CategoryTheory.HasLiftingProperty.iff_op
{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}
:
theorem
CategoryTheory.HasLiftingProperty.iff_unop
{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)
:
CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty p.unop i.unop
@[instance 100]
instance
CategoryTheory.HasLiftingProperty.of_left_iso
{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)
[CategoryTheory.IsIso i]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
CategoryTheory.HasLiftingProperty.of_right_iso
{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)
[CategoryTheory.IsIso p]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.HasLiftingProperty.of_comp_left
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{B' : C}
{X : C}
{Y : C}
(i : A ⟶ B)
(i' : B ⟶ B')
(p : X ⟶ Y)
[CategoryTheory.HasLiftingProperty i p]
[CategoryTheory.HasLiftingProperty i' p]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.HasLiftingProperty.of_comp_right
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{Y' : C}
(i : A ⟶ B)
(p : X ⟶ Y)
(p' : Y ⟶ Y')
[CategoryTheory.HasLiftingProperty i p]
[CategoryTheory.HasLiftingProperty i p']
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.HasLiftingProperty.of_arrow_iso_left
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{A' : C}
{B' : C}
{X : C}
{Y : C}
{i : A ⟶ B}
{i' : A' ⟶ B'}
(e : CategoryTheory.Arrow.mk i ≅ CategoryTheory.Arrow.mk i')
(p : X ⟶ Y)
[hip : CategoryTheory.HasLiftingProperty i p]
:
theorem
CategoryTheory.HasLiftingProperty.of_arrow_iso_right
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{X' : C}
{Y' : C}
(i : A ⟶ B)
{p : X ⟶ Y}
{p' : X' ⟶ Y'}
(e : CategoryTheory.Arrow.mk p ≅ CategoryTheory.Arrow.mk p')
[hip : CategoryTheory.HasLiftingProperty i p]
:
theorem
CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{A' : C}
{B' : C}
{X : C}
{Y : C}
{i : A ⟶ B}
{i' : A' ⟶ B'}
(e : CategoryTheory.Arrow.mk i ≅ CategoryTheory.Arrow.mk i')
(p : X ⟶ Y)
:
theorem
CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{X' : C}
{Y' : C}
(i : A ⟶ B)
{p : X ⟶ Y}
{p' : X' ⟶ Y'}
(e : CategoryTheory.Arrow.mk p ≅ CategoryTheory.Arrow.mk p')
: