Mathlib.CategoryTheory.LiftingProperties.Basic

CategoryTheory.HasLiftingProperty structure

Full source

/-- `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`. -/
class HasLiftingProperty : Prop where
  /-- Unique field expressing that any commutative square built from `f` and `g` has a lift -/
  sq_hasLift : ∀ {f : A ⟶ X} {g : B ⟶ Y} (sq : CommSq f i p g), sq.HasLift

Lifting Property of Morphisms

Informal description

The structure `HasLiftingProperty i p` indicates that the morphism `i` has the left lifting property with respect to `p`, or equivalently that `p` has the right lifting property with respect to `i`. This means that for any commutative square formed by `i` and `p`, there exists a lift completing the diagram.

CategoryTheory.sq_hasLift_of_hasLiftingProperty instance

{f : A ⟶ X} {g : B ⟶ Y} (sq : CommSq f i p g) [hip : HasLiftingProperty i p] : sq.HasLift

Full source

instance (priority := 100) sq_hasLift_of_hasLiftingProperty {f : A ⟶ X} {g : B ⟶ Y}
    (sq : CommSq f i p g) [hip : HasLiftingProperty i p] : sq.HasLift := hip.sq_hasLift _

Existence of Lift in Commutative Squares with Lifting Property

Informal description

Given a commutative square in a category with morphisms $f \colon A \to X$ and $g \colon B \to Y$, and morphisms $i \colon A \to B$ and $p \colon X \to Y$ such that $i$ has the left lifting property with respect to $p$, there exists a lift completing the diagram.

CategoryTheory.HasLiftingProperty.op theorem

(h : HasLiftingProperty i p) : HasLiftingProperty p.op i.op

Full source

theorem op (h : HasLiftingProperty i p) : HasLiftingProperty p.op i.op :=
  ⟨fun {f} {g} sq => by
    simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]
    infer_instance⟩

Opposite Lifting Property: $i \perp p$ implies $p^{\mathrm{op}} \perp i^{\mathrm{op}}$

Informal description

Given morphisms $i \colon A \to B$ and $p \colon X \to Y$ in a category $C$, if $i$ has the left lifting property with respect to $p$, then in the opposite category $C^{\mathrm{op}}$, the morphism $p^{\mathrm{op}} \colon Y \to X$ has the left lifting property with respect to $i^{\mathrm{op}} \colon B \to A$.

CategoryTheory.HasLiftingProperty.unop theorem

{A B X Y : Cᵒᵖ} {i : A ⟶ B} {p : X ⟶ Y} (h : HasLiftingProperty i p) : HasLiftingProperty p.unop i.unop

Full source

theorem unop {A B X Y : Cᵒᵖ} {i : A ⟶ B} {p : X ⟶ Y} (h : HasLiftingProperty i p) :
    HasLiftingProperty p.unop i.unop :=
  ⟨fun {f} {g} sq => by
    rw [CommSq.HasLift.iff_op]
    simp only [Quiver.Hom.op_unop]
    infer_instance⟩

Unop preserves lifting property

Informal description

Given morphisms $i \colon A \to B$ and $p \colon X \to Y$ in the opposite category $C^{\mathrm{op}}$, if $i$ has the left lifting property with respect to $p$ in $C^{\mathrm{op}}$, then the corresponding morphisms $p^{\mathrm{unop}} \colon Y \to X$ and $i^{\mathrm{unop}} \colon B \to A$ in the original category $C$ satisfy that $p^{\mathrm{unop}}$ has the left lifting property with respect to $i^{\mathrm{unop}}$.

CategoryTheory.HasLiftingProperty.iff_op theorem

: HasLiftingProperty i p ↔ HasLiftingProperty p.op i.op

Full source

theorem iff_op : HasLiftingPropertyHasLiftingProperty i p ↔ HasLiftingProperty p.op i.op :=
  ⟨op, unop⟩

Lifting Property Duality: $i \perp p \leftrightarrow p^{\mathrm{op}} \perp i^{\mathrm{op}}$

Informal description

For any morphisms $i \colon A \to B$ and $p \colon X \to Y$ in a category $C$, the morphism $i$ has the left lifting property with respect to $p$ if and only if the opposite morphism $p^{\mathrm{op}} \colon Y \to X$ has the left lifting property with respect to the opposite morphism $i^{\mathrm{op}} \colon B \to A$ in the opposite category $C^{\mathrm{op}}$.

CategoryTheory.HasLiftingProperty.iff_unop theorem

{A B X Y : Cᵒᵖ} (i : A ⟶ B) (p : X ⟶ Y) : HasLiftingProperty i p ↔ HasLiftingProperty p.unop i.unop

Full source

theorem iff_unop {A B X Y : Cᵒᵖ} (i : A ⟶ B) (p : X ⟶ Y) :
    HasLiftingPropertyHasLiftingProperty i p ↔ HasLiftingProperty p.unop i.unop :=
  ⟨unop, op⟩

Lifting Property Duality via Unop: $i \perp p \leftrightarrow p^{\mathrm{unop}} \perp i^{\mathrm{unop}}$

Informal description

For any morphisms $i \colon A \to B$ and $p \colon X \to Y$ in the opposite category $C^{\mathrm{op}}$, the morphism $i$ has the left lifting property with respect to $p$ if and only if the corresponding morphisms $p^{\mathrm{unop}} \colon Y \to X$ and $i^{\mathrm{unop}} \colon B \to A$ in the original category $C$ satisfy that $p^{\mathrm{unop}}$ has the left lifting property with respect to $i^{\mathrm{unop}}$.

CategoryTheory.HasLiftingProperty.of_left_iso instance

[IsIso i] : HasLiftingProperty i p

Full source

instance (priority := 100) of_left_iso [IsIso i] : HasLiftingProperty i p :=
  ⟨fun {f} {g} sq =>
    CommSq.HasLift.mk'
      { l := inv i ≫ f
        fac_left := by simp only [IsIso.hom_inv_id_assoc]
        fac_right := by simp only [sq.w, assoc, IsIso.inv_hom_id_assoc] }⟩

Isomorphisms Have the Left Lifting Property

Informal description

For any morphism $i$ in a category, if $i$ is an isomorphism, then $i$ has the left lifting property with respect to any morphism $p$.

CategoryTheory.HasLiftingProperty.of_right_iso instance

[IsIso p] : HasLiftingProperty i p

Full source

instance (priority := 100) of_right_iso [IsIso p] : HasLiftingProperty i p :=
  ⟨fun {f} {g} sq =>
    CommSq.HasLift.mk'
      { l := g ≫ inv p
        fac_left := by simp only [← sq.w_assoc, IsIso.hom_inv_id, comp_id]
        fac_right := by simp only [assoc, IsIso.inv_hom_id, comp_id] }⟩

Isomorphisms Have the Right Lifting Property

Informal description

For any morphism $i$ in a category, if $p$ is an isomorphism, then $i$ has the left lifting property with respect to $p$.

CategoryTheory.HasLiftingProperty.of_comp_left instance

[HasLiftingProperty i p] [HasLiftingProperty i' p] : HasLiftingProperty (i ≫ i') p

Full source

instance of_comp_left [HasLiftingProperty i p] [HasLiftingProperty i' p] :
    HasLiftingProperty (i ≫ i') p :=
  ⟨fun {f} {g} sq => by
    have fac := sq.w
    rw [assoc] at fac
    exact
      CommSq.HasLift.mk'
        { l := (CommSq.mk (CommSq.mk fac).fac_right).lift
          fac_left := by simp only [assoc, CommSq.fac_left]
          fac_right := by simp only [CommSq.fac_right] }⟩

Composition Preserves Left Lifting Property

Informal description

Given morphisms $i \colon A \to B$ and $i' \colon B \to C$ in a category, if both $i$ and $i'$ have the left lifting property with respect to a morphism $p \colon X \to Y$, then their composition $i \circ i'$ also has the left lifting property with respect to $p$.

CategoryTheory.HasLiftingProperty.of_comp_right instance

[HasLiftingProperty i p] [HasLiftingProperty i p'] : HasLiftingProperty i (p ≫ p')

Full source

instance of_comp_right [HasLiftingProperty i p] [HasLiftingProperty i p'] :
    HasLiftingProperty i (p ≫ p') :=
  ⟨fun {f} {g} sq => by
    have fac := sq.w
    rw [← assoc] at fac
    let _ := (CommSq.mk (CommSq.mk fac).fac_left.symm).lift
    exact
      CommSq.HasLift.mk'
        { l := (CommSq.mk (CommSq.mk fac).fac_left.symm).lift
          fac_left := by simp only [CommSq.fac_left]
          fac_right := by simp only [CommSq.fac_right_assoc, CommSq.fac_right] }⟩

Composition Preserves Right Lifting Property

Informal description

Given morphisms $i \colon A \to B$, $p \colon X \to Y$, and $p' \colon Y \to Z$ in a category, if $i$ has the left lifting property with respect to both $p$ and $p'$, then $i$ also has the left lifting property with respect to the composition $p \circ p'$.

CategoryTheory.HasLiftingProperty.of_arrow_iso_left theorem

 {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

Full source

theorem of_arrow_iso_left {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'}
    (e : Arrow.mkArrow.mk i ≅ Arrow.mk i') (p : X ⟶ Y) [hip : HasLiftingProperty i p] :
    HasLiftingProperty i' p := by
  rw [Arrow.iso_w' e]
  infer_instance

Left Lifting Property is Preserved Under Arrow Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $i \colon A \to B$ and $i' \colon A' \to B'$ be morphisms in $\mathcal{C}$ such that there exists an isomorphism $e$ between the arrows $\text{Arrow.mk } i$ and $\text{Arrow.mk } i'$. If $i$ has the left lifting property with respect to a morphism $p \colon X \to Y$, then $i'$ also has the left lifting property with respect to $p$.

CategoryTheory.HasLiftingProperty.of_arrow_iso_right theorem

 {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'

Full source

theorem of_arrow_iso_right {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'}
    (e : Arrow.mkArrow.mk p ≅ Arrow.mk p') [hip : HasLiftingProperty i p] : HasLiftingProperty i p' := by
  rw [Arrow.iso_w' e]
  infer_instance

Right Lifting Property is Preserved Under Arrow Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $i \colon A \to B$ be a morphism in $\mathcal{C}$. Suppose $p \colon X \to Y$ and $p' \colon X' \to Y'$ are morphisms in $\mathcal{C}$ such that there exists an isomorphism $e$ between the arrows $\text{Arrow.mk } p$ and $\text{Arrow.mk } p'$. If $i$ has the left lifting property with respect to $p$, then $i$ also has the left lifting property with respect to $p'$.

CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_left theorem

 {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

Full source

theorem iff_of_arrow_iso_left {A B A' B' X Y : C} {i : A ⟶ B} {i' : A' ⟶ B'}
    (e : Arrow.mkArrow.mk i ≅ Arrow.mk i') (p : X ⟶ Y) :
    HasLiftingPropertyHasLiftingProperty i p ↔ HasLiftingProperty i' p := by
  constructor <;> intro
  exacts [of_arrow_iso_left e p, of_arrow_iso_left e.symm p]

Equivalence of Lifting Properties Under Left Arrow Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $i \colon A \to B$ and $i' \colon A' \to B'$ be morphisms in $\mathcal{C}$ such that there exists an isomorphism $e$ between the arrows $\text{Arrow.mk } i$ and $\text{Arrow.mk } i'$. Then for any morphism $p \colon X \to Y$ in $\mathcal{C}$, $i$ has the left lifting property with respect to $p$ if and only if $i'$ has the left lifting property with respect to $p$.

CategoryTheory.HasLiftingProperty.iff_of_arrow_iso_right theorem

 {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'

Full source

theorem iff_of_arrow_iso_right {A B X Y X' Y' : C} (i : A ⟶ B) {p : X ⟶ Y} {p' : X' ⟶ Y'}
    (e : Arrow.mkArrow.mk p ≅ Arrow.mk p') : HasLiftingPropertyHasLiftingProperty i p ↔ HasLiftingProperty i p' := by
  constructor <;> intro
  exacts [of_arrow_iso_right i e, of_arrow_iso_right i e.symm]

Equivalence of Lifting Properties Under Arrow Isomorphism

Informal description

Let $\mathcal{C}$ be a category, and let $i \colon A \to B$ be a morphism in $\mathcal{C}$. Suppose $p \colon X \to Y$ and $p' \colon X' \to Y'$ are morphisms in $\mathcal{C}$ such that there exists an isomorphism $e$ between the arrows $\text{Arrow.mk } p$ and $\text{Arrow.mk } p'$. Then $i$ has the left lifting property with respect to $p$ if and only if $i$ has the left lifting property with respect to $p'$.

CategoryTheory.RetractArrow.leftLiftingProperty theorem

 {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

Full source

lemma RetractArrow.leftLiftingProperty
    {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 where
  sq_hasLift := fun {u v} sq ↦ by
    have sq' : CommSq (h.r.left ≫ u) g f (h.r.right ≫ v) := by simp only [Arrow.mk_left,
      Arrow.mk_right, Category.assoc, sq.w, Arrow.w_mk_right_assoc, Arrow.mk_hom, CommSq.mk]
    exact
      ⟨⟨{ l := h.i.right ≫ sq'.lift
          fac_left := by
            simp only [← h.i_w_assoc, sq'.fac_left, h.retract_left_assoc,
              Arrow.mk_left, Category.id_comp]}⟩⟩

Retract Preserves Left Lifting Property

Informal description

Let $\mathcal{C}$ be a category, and let $g \colon Z \to W$ and $g' \colon Z' \to W'$ be morphisms in $\mathcal{C}$ such that $g'$ is a retract of $g$. For any morphism $f \colon X \to Y$ in $\mathcal{C}$, if $g$ has the left lifting property with respect to $f$, then $g'$ also has the left lifting property with respect to $f$.

CategoryTheory.RetractArrow.rightLiftingProperty theorem

 {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'

Full source

lemma RetractArrow.rightLiftingProperty
    {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' where
  sq_hasLift := fun {u v} sq ↦
    have sq' : CommSq (u ≫ h.i.left) g f (v ≫ h.i.right) :=
      ⟨by rw [← Category.assoc, ← sq.w, Category.assoc, RetractArrow.i_w, Category.assoc]⟩
    ⟨⟨{ l := sq'.lift ≫ h.r.left}⟩⟩

Retract Preservation of Left Lifting Property

Informal description

Let $\mathcal{C}$ be a category, and let $f \colon X \to Y$ and $f' \colon X' \to Y'$ be morphisms in $\mathcal{C}$ such that $f'$ is a retract of $f$. For any morphism $g \colon Z \to W$ in $\mathcal{C}$, if $g$ has the left lifting property with respect to $f$, then $g$ also has the left lifting property with respect to $f'$.

Mathlib.CategoryTheory.LiftingProperties.Basic

Main results

Tags