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

1. direct/inverse images, adjunctions

class CategoryTheory.HasLiftingProperty {C : Type u_1} [Category.{v_1, 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 : 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} [Category.{v_1, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) {f : A ⟶ X} {g : B ⟶ Y} (sq : CommSq f i p g) [hip : HasLiftingProperty i p] : sq.HasLift

theorem CategoryTheory.HasLiftingProperty.op {C : Type u_1} [Category.{v_1, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y} (h : HasLiftingProperty i p) : HasLiftingProperty p.op i.op

theorem CategoryTheory.HasLiftingProperty.unop {C : Type u_1} [Category.{v_1, u_1} C] {A B X Y : Cᵒᵖ} {i : A ⟶ B} {p : X ⟶ Y} (h : HasLiftingProperty i p) : HasLiftingProperty p.unop i.unop

theorem CategoryTheory.HasLiftingProperty.iff_op {C : Type u_1} [Category.{v_1, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y} : HasLiftingProperty i p ↔ HasLiftingProperty p.op i.op

theorem CategoryTheory.HasLiftingProperty.iff_unop {C : Type u_1} [Category.{v_1, u_1} C] {A B X Y : Cᵒᵖ} (i : A ⟶ B) (p : X ⟶ Y) : HasLiftingProperty i p ↔ HasLiftingProperty p.unop i.unop

@[instance 100]

instance CategoryTheory.HasLiftingProperty.of_left_iso {C : Type u_1} [Category.{v_1, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [IsIso i] : HasLiftingProperty i p

@[instance 100]

instance CategoryTheory.HasLiftingProperty.of_right_iso {C : Type u_1} [Category.{v_1, u_1} C] {Y X B A : C} (p : X ⟶ Y) (i : A ⟶ B) [IsIso p] : HasLiftingProperty i p

instance CategoryTheory.HasLiftingProperty.of_comp_left {C : Type u_1} [Category.{v_1, u_1} C] {A B B' X Y : C} (i : A ⟶ B) (i' : B ⟶ B') (p : X ⟶ Y) [HasLiftingProperty i p] [HasLiftingProperty i' p] : HasLiftingProperty (CategoryStruct.comp i i') p

instance CategoryTheory.HasLiftingProperty.of_comp_right {C : Type u_1} [Category.{v_1, u_1} C] {Y X X' B A : C} (p : X ⟶ Y) (p' : X' ⟶ X) (i : A ⟶ B) [HasLiftingProperty i p] [HasLiftingProperty i p'] : HasLiftingProperty i (CategoryStruct.comp p' p)

theorem CategoryTheory.HasLiftingProperty.of_arrow_iso_left {C : Type u_1} [Category.{v_1, u_1} C] {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'} (e : Arrow.mk i ≅ Arrow.mk i') (p : X ⟶ Y) [hip : HasLiftingProperty i p] : HasLiftingProperty i' p

theorem CategoryTheory.HasLiftingProperty.of_arrow_iso_right {C : Type u_1} [Category.{v_1, u_1} C] {Y X Y' X' B A : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'} (e : Arrow.mk p ≅ Arrow.mk p') [hip : HasLiftingProperty i p] : HasLiftingProperty i p'

theorem CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left {C : Type u_1} [Category.{v_1, u_1} C] {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'} (e : Arrow.mk i ≅ Arrow.mk i') (p : X ⟶ Y) : HasLiftingProperty i p ↔ HasLiftingProperty i' p

theorem CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right {C : Type u_1} [Category.{v_1, u_1} C] {Y X Y' X' B A : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'} (e : Arrow.mk p ≅ Arrow.mk p') : HasLiftingProperty i p ↔ HasLiftingProperty i p'

theorem CategoryTheory.RetractArrow.rightLiftingProperty {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z W X' Y' : C} {f : X ⟶ Y} {f' : X' ⟶ Y'} (h : RetractArrow f' f) (g : Z ⟶ W) [HasLiftingProperty g f] : HasLiftingProperty g f'

theorem CategoryTheory.RetractArrow.leftLiftingProperty {C : Type u_1} [Category.{v_1, u_1} C] {B A Z W B' A' : C} {f : A ⟶ B} {f' : A' ⟶ B'} (h : RetractArrow f' f) (g : W ⟶ Z) [HasLiftingProperty f g] : HasLiftingProperty f' g

@[reducible, inline]

abbrev CategoryTheory.Arrow.LiftStruct {C : Type u_1} [Category.{v_1, u_1} C] {f g : Arrow C} (φ : f ⟶ g) : Type v_1

Given a morphism φ : f ⟶ g in the category Arrow C, this is an abbreviation for the CommSq.LiftStruct structure for the square corresponding to φ.

Equations

• CategoryTheory.Arrow.LiftStruct φ = ⋯.LiftStruct

theorem CategoryTheory.Arrow.hasLiftingProperty_iff {C : Type u_1} [Category.{v_1, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) : HasLiftingProperty i p ↔ ∀ (φ : mk i ⟶ mk p), Nonempty (LiftStruct φ)

def CategoryTheory.HasLiftingPropertyFixedTop {C : Type u_1} [Category.{v_1, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) (t : A ⟶ X) : Prop

Given morphisms i : A ⟶ B, p : X ⟶ Y, t : A ⟶ X, this is the property that a lifting exists for all squares with i on left, p on the right and t on the top.

Equations

• CategoryTheory.HasLiftingPropertyFixedTop i p t = ∀ (b : B ⟶ Y) (sq : CategoryTheory.CommSq t i p b), sq.HasLift

def CategoryTheory.HasLiftingPropertyFixedBot {C : Type u_1} [Category.{v_1, u_1} C] {Y X B A : C} (i : A ⟶ B) (p : X ⟶ Y) (b : B ⟶ Y) : Prop

Given morphisms i : A ⟶ B, p : X ⟶ Y, b : B ⟶ Y, this is the property that a lifting exists for all squares with i on left, p on the right and b on the bottom.

Equations

• CategoryTheory.HasLiftingPropertyFixedBot p i t = ∀ (b : Y ⟶ B) (sq : CategoryTheory.CommSq b p i t), sq.HasLift