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. direct/inverse images, adjunctions
source
class CategoryTheory.HasLiftingProperty {C : Type u_1} [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 : 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} [Category.{u_2, 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
    source
    theorem CategoryTheory.HasLiftingProperty.op {C : Type u_1} [Category.{u_2, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y} (h : HasLiftingProperty i p) :
    HasLiftingProperty p.op i.op
    source
    theorem CategoryTheory.HasLiftingProperty.unop {C : Type u_1} [Category.{u_2, u_1} C] {A B X Y : Cᵒᵖ} {i : A ⟶ B} {p : X ⟶ Y} (h : HasLiftingProperty i p) :
    HasLiftingProperty p.unop i.unop
    source
    theorem CategoryTheory.HasLiftingProperty.iff_op {C : Type u_1} [Category.{u_2, u_1} C] {A B X Y : C} {i : A ⟶ B} {p : X ⟶ Y} :
    HasLiftingProperty i p ↔ HasLiftingProperty p.op i.op
    source
    theorem CategoryTheory.HasLiftingProperty.iff_unop {C : Type u_1} [Category.{u_2, u_1} C] {A B X Y : Cᵒᵖ} (i : A ⟶ B) (p : X ⟶ Y) :
    HasLiftingProperty i p ↔ HasLiftingProperty p.unop i.unop
    source
    @[instance 100]
    instance CategoryTheory.HasLiftingProperty.of_left_iso {C : Type u_1} [Category.{u_2, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [IsIso i] :
    HasLiftingProperty i p
    source
    @[instance 100]
    instance CategoryTheory.HasLiftingProperty.of_right_iso {C : Type u_1} [Category.{u_2, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [IsIso p] :
    HasLiftingProperty i p
    source
    instance CategoryTheory.HasLiftingProperty.of_comp_left {C : Type u_1} [Category.{u_2, 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
    source
    instance CategoryTheory.HasLiftingProperty.of_comp_right {C : Type u_1} [Category.{u_2, u_1} C] {A B X Y Y' : C} (i : A ⟶ B) (p : X ⟶ Y) (p' : Y ⟶ Y') [HasLiftingProperty i p] [HasLiftingProperty i p'] :
    HasLiftingProperty i (CategoryStruct.comp p p')
    source
    theorem CategoryTheory.HasLiftingProperty.of_arrow_iso_left {C : Type u_1} [Category.{u_2, 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
    source
    theorem CategoryTheory.HasLiftingProperty.of_arrow_iso_right {C : Type u_1} [Category.{u_2, u_1} C] {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'} (e : Arrow.mk p ≅ Arrow.mk p') [hip : HasLiftingProperty i p] :
    HasLiftingProperty i p'
    source
    theorem CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left {C : Type u_1} [Category.{u_2, 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
    source
    theorem CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right {C : Type u_1} [Category.{u_2, u_1} C] {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'} (e : Arrow.mk p ≅ Arrow.mk p') :
    HasLiftingProperty i p ↔ HasLiftingProperty i p'
    source
    theorem CategoryTheory.RetractArrow.leftLiftingProperty {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z W Z' W' : C} {g : Z ⟶ W} {g' : Z' ⟶ W'} (h : RetractArrow g' g) (f : X ⟶ Y) [HasLiftingProperty g f] :
    HasLiftingProperty g' f
    source
    theorem CategoryTheory.RetractArrow.rightLiftingProperty {C : Type u_1} [Category.{u_2, 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'
    source
    @[reducible, inline]
    abbrev CategoryTheory.Arrow.LiftStruct {C : Type u_1} [Category.{u_2, u_1} C] {f g : Arrow C} (φ : f ⟶ g) :
    Type u_2

    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
    Instances For
      source
      theorem CategoryTheory.Arrow.hasLiftingProperty_iff {C : Type u_1} [Category.{u_2, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) :
      HasLiftingProperty i p ↔ ∀ (φ : mk i ⟶ mk p), Nonempty (LiftStruct φ)
      source
      def CategoryTheory.HasLiftingPropertyFixedTop {C : Type u_1} [Category.{u_2, 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
      Instances For
        source
        def CategoryTheory.HasLiftingPropertyFixedBot {C : Type u_1} [Category.{u_2, u_1} C] {A B X Y : 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
        Instances For