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
source
class CategoryTheory.HasLiftingProperty {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) :
Prop

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
    source
    @[instance 100]
    instance CategoryTheory.sq_hasLift_of_hasLiftingProperty {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B X 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
    source
    theorem CategoryTheory.HasLiftingProperty.op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y} (h : CategoryTheory.HasLiftingProperty i p) :
    CategoryTheory.HasLiftingProperty p.op i.op
    source
    theorem CategoryTheory.HasLiftingProperty.unop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B X Y : Cᵒᵖ} {i : A ⟶ B} {p : X ⟶ Y} (h : CategoryTheory.HasLiftingProperty i p) :
    CategoryTheory.HasLiftingProperty p.unop i.unop
    source
    theorem CategoryTheory.HasLiftingProperty.iff_op {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y} :
    CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty p.op i.op
    source
    theorem CategoryTheory.HasLiftingProperty.iff_unop {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B X Y : Cᵒᵖ} (i : A ⟶ B) (p : X ⟶ Y) :
    CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty p.unop i.unop
    source
    @[instance 100]
    instance CategoryTheory.HasLiftingProperty.of_left_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [CategoryTheory.IsIso i] :
    CategoryTheory.HasLiftingProperty i p
    source
    @[instance 100]
    instance CategoryTheory.HasLiftingProperty.of_right_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [CategoryTheory.IsIso p] :
    CategoryTheory.HasLiftingProperty i p
    source
    instance CategoryTheory.HasLiftingProperty.of_comp_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B B' X Y : C} (i : A ⟶ B) (i' : B ⟶ B') (p : X ⟶ Y) [CategoryTheory.HasLiftingProperty i p] [CategoryTheory.HasLiftingProperty i' p] :
    CategoryTheory.HasLiftingProperty (CategoryTheory.CategoryStruct.comp i i') p
    source
    instance CategoryTheory.HasLiftingProperty.of_comp_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B X Y Y' : C} (i : A ⟶ B) (p : X ⟶ Y) (p' : Y ⟶ Y') [CategoryTheory.HasLiftingProperty i p] [CategoryTheory.HasLiftingProperty i p'] :
    CategoryTheory.HasLiftingProperty i (CategoryTheory.CategoryStruct.comp p p')
    source
    theorem CategoryTheory.HasLiftingProperty.of_arrow_iso_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B A' B' X 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] :
    CategoryTheory.HasLiftingProperty i' p
    source
    theorem CategoryTheory.HasLiftingProperty.of_arrow_iso_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B X Y X' 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] :
    CategoryTheory.HasLiftingProperty i p'
    source
    theorem CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'} (e : CategoryTheory.Arrow.mk i ≅ CategoryTheory.Arrow.mk i') (p : X ⟶ Y) :
    CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty i' p
    source
    theorem CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'} (e : CategoryTheory.Arrow.mk p ≅ CategoryTheory.Arrow.mk p') :
    CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty i p'