Mathlib.CategoryTheory.CommSq

CategoryTheory.CommSq structure

{W X Y Z : C} (f : W ⟶ X) (g : W ⟶ Y) (h : X ⟶ Z) (i : Y ⟶ Z)

Full source

/-- The proposition that a square
```
  W ---f---> X
  |          |
  g          h
  |          |
  v          v
  Y ---i---> Z

```
is a commuting square.
-/
structure CommSq {W X Y Z : C} (f : W ⟶ X) (g : W ⟶ Y) (h : X ⟶ Z) (i : Y ⟶ Z) : Prop where
  /-- The square commutes. -/
  w : f ≫ h = g ≫ i

Commutative Square in a Category

Informal description

The structure `CommSq` represents a commutative square in a category, where the morphisms satisfy the commutativity condition $h \circ f = i \circ g$. Specifically, given four morphisms $f: W \to X$, $g: W \to Y$, $h: X \to Z$, and $i: Y \to Z$, the square formed by these morphisms is commutative if the composition of $h$ with $f$ equals the composition of $i$ with $g$.

CategoryTheory.CommSq.flip theorem

(p : CommSq f g h i) : CommSq g f i h

Full source

theorem flip (p : CommSq f g h i) : CommSq g f i h :=
  ⟨p.w.symm⟩

Commutativity of Flipped Square

Informal description

Given a commutative square in a category with morphisms $f \colon W \to X$, $g \colon W \to Y$, $h \colon X \to Z$, and $i \colon Y \to Z$ satisfying $h \circ f = i \circ g$, the flipped square with morphisms $g \colon W \to Y$, $f \colon W \to X$, $i \colon Y \to Z$, and $h \colon X \to Z$ is also commutative, i.e., $i \circ g = h \circ f$.

CategoryTheory.CommSq.of_arrow theorem

{f g : Arrow C} (h : f ⟶ g) : CommSq f.hom h.left h.right g.hom

Full source

theorem of_arrow {f g : Arrow C} (h : f ⟶ g) : CommSq f.hom h.left h.right g.hom :=
  ⟨h.w.symm⟩

Commutative Square Induced by Arrow Morphism

Informal description

Given two objects $f$ and $g$ in the arrow category of a category $\mathcal{C}$, and a morphism $h \colon f \to g$ between them, the square formed by the morphisms $f_{\mathrm{hom}} \colon \mathrm{dom}(f) \to \mathrm{cod}(f)$, $h_{\mathrm{left}} \colon \mathrm{dom}(f) \to \mathrm{dom}(g)$, $h_{\mathrm{right}} \colon \mathrm{cod}(f) \to \mathrm{cod}(g)$, and $g_{\mathrm{hom}} \colon \mathrm{dom}(g) \to \mathrm{cod}(g)$ is commutative, i.e., $g_{\mathrm{hom}} \circ h_{\mathrm{left}} = h_{\mathrm{right}} \circ f_{\mathrm{hom}}$.

CategoryTheory.CommSq.op theorem

(p : CommSq f g h i) : CommSq i.op h.op g.op f.op

Full source

/-- The commutative square in the opposite category associated to a commutative square. -/
theorem op (p : CommSq f g h i) : CommSq i.op h.op g.op f.op :=
  ⟨by simp only [← op_comp, p.w]⟩

Opposite of a Commutative Square is Commutative

Informal description

Given a commutative square in a category $\mathcal{C}$ with morphisms $f \colon W \to X$, $g \colon W \to Y$, $h \colon X \to Z$, and $i \colon Y \to Z$ such that $h \circ f = i \circ g$, the corresponding square in the opposite category $\mathcal{C}^{\mathrm{op}}$ formed by the opposite morphisms $i^{\mathrm{op}} \colon Z^{\mathrm{op}} \to Y^{\mathrm{op}}$, $h^{\mathrm{op}} \colon Z^{\mathrm{op}} \to X^{\mathrm{op}}$, $g^{\mathrm{op}} \colon Y^{\mathrm{op}} \to W^{\mathrm{op}}$, and $f^{\mathrm{op}} \colon X^{\mathrm{op}} \to W^{\mathrm{op}}$ is also commutative, i.e., $f^{\mathrm{op}} \circ h^{\mathrm{op}} = g^{\mathrm{op}} \circ i^{\mathrm{op}}$.

CategoryTheory.CommSq.unop theorem

 {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CommSq f g h i) :
  CommSq i.unop h.unop g.unop f.unop

Full source

/-- The commutative square associated to a commutative square in the opposite category. -/
theorem unop {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CommSq f g h i) :
    CommSq i.unop h.unop g.unop f.unop :=
  ⟨by simp only [← unop_comp, p.w]⟩

Commutative Square in Opposite Category Induces Commutative Square in Original Category

Informal description

Given a commutative square in the opposite category $\mathcal{C}^{\mathrm{op}}$ with morphisms $f \colon W \to X$, $g \colon W \to Y$, $h \colon X \to Z$, and $i \colon Y \to Z$ such that $h \circ f = i \circ g$, the corresponding square in the original category $\mathcal{C}$ formed by the unopposite morphisms $i^{\mathrm{unop}} \colon \mathrm{unop}\, Z \to \mathrm{unop}\, Y$, $h^{\mathrm{unop}} \colon \mathrm{unop}\, Z \to \mathrm{unop}\, X$, $g^{\mathrm{unop}} \colon \mathrm{unop}\, Y \to \mathrm{unop}\, W$, and $f^{\mathrm{unop}} \colon \mathrm{unop}\, X \to \mathrm{unop}\, W$ is also commutative, i.e., $f^{\mathrm{unop}} \circ h^{\mathrm{unop}} = g^{\mathrm{unop}} \circ i^{\mathrm{unop}}$.

CategoryTheory.CommSq.vert_inv theorem

{g : W ≅ Y} {h : X ≅ Z} (p : CommSq f g.hom h.hom i) : CommSq i g.inv h.inv f

Full source

theorem vert_inv {g : W ≅ Y} {h : X ≅ Z} (p : CommSq f g.hom h.hom i) :
    CommSq i g.inv h.inv f :=
  ⟨by rw [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, p.w]⟩

Commutative Square with Vertical Isomorphisms Inverted

Informal description

Given a commutative square in a category $\mathcal{C}$ with morphisms $f: W \to X$, $g: W \to Y$, $h: X \to Z$, and $i: Y \to Z$ such that $h \circ f = i \circ g$, and given isomorphisms $g: W \cong Y$ and $h: X \cong Z$, the square formed by the inverses of these isomorphisms is also commutative. Specifically, the square with morphisms $i: Y \to Z$, $g^{-1}: Y \to W$, $h^{-1}: Z \to X$, and $f: W \to X$ satisfies $h^{-1} \circ i = f \circ g^{-1}$.

CategoryTheory.CommSq.horiz_inv theorem

{f : W ≅ X} {i : Y ≅ Z} (p : CommSq f.hom g h i.hom) : CommSq f.inv h g i.inv

Full source

theorem horiz_inv {f : W ≅ X} {i : Y ≅ Z} (p : CommSq f.hom g h i.hom) :
    CommSq f.inv h g i.inv :=
  flip (vert_inv (flip p))

Commutative Square with Horizontal Isomorphisms Inverted

Informal description

Given a commutative square in a category $\mathcal{C}$ with morphisms $f \colon W \to X$, $g \colon W \to Y$, $h \colon X \to Z$, and $i \colon Y \to Z$ such that $h \circ f = i \circ g$, and given isomorphisms $f \colon W \cong X$ and $i \colon Y \cong Z$, the square formed by the inverses of these isomorphisms is also commutative. Specifically, the square with morphisms $f^{-1} \colon X \to W$, $h \colon X \to Z$, $g \colon W \to Y$, and $i^{-1} \colon Z \to Y$ satisfies $g \circ f^{-1} = i^{-1} \circ h$.

CategoryTheory.CommSq.horiz_comp theorem

 {W X X' Y Z Z' : C} {f : W ⟶ X} {f' : X ⟶ X'} {g : W ⟶ Y} {h : X ⟶ Z} {h' : X' ⟶ Z'} {i : Y ⟶ Z} {i' : Z ⟶ Z'}
  (hsq₁ : CommSq f g h i) (hsq₂ : CommSq f' h h' i') : CommSq (f ≫ f') g h' (i ≫ i')

Full source

/-- The horizontal composition of two commutative squares as below is a commutative square.
```
  W ---f---> X ---f'--> X'
  |          |          |
  g          h          h'
  |          |          |
  v          v          v
  Y ---i---> Z ---i'--> Z'

```
-/
lemma horiz_comp {W X X' Y Z Z' : C} {f : W ⟶ X} {f' : X ⟶ X'} {g : W ⟶ Y} {h : X ⟶ Z}
    {h' : X' ⟶ Z'} {i : Y ⟶ Z} {i' : Z ⟶ Z'} (hsq₁ : CommSq f g h i) (hsq₂ : CommSq f' h h' i') :
    CommSq (f ≫ f') g h' (i ≫ i') :=
  ⟨by rw [← Category.assoc, Category.assoc, ← hsq₁.w, hsq₂.w, Category.assoc]⟩

Horizontal Composition of Commutative Squares in a Category

Informal description

Given a category $\mathcal{C}$ and objects $W, X, X', Y, Z, Z'$ in $\mathcal{C}$, consider morphisms forming two commutative squares: 1. $f: W \to X$, $g: W \to Y$, $h: X \to Z$, $i: Y \to Z$ with $h \circ f = i \circ g$ 2. $f': X \to X'$, $h: X \to Z$, $h': X' \to Z'$, $i': Z \to Z'$ with $h' \circ f' = i' \circ h$ Then the horizontal composition of these squares forms a new commutative square with: - Top edge: $f \circ f' : W \to X'$ - Left edge: $g: W \to Y$ - Right edge: $h': X' \to Z'$ - Bottom edge: $i \circ i' : Y \to Z'$ satisfying $h' \circ (f \circ f') = (i \circ i') \circ g$.

CategoryTheory.CommSq.vert_comp theorem

 {W X Y Y' Z Z' : C} {f : W ⟶ X} {g : W ⟶ Y} {g' : Y ⟶ Y'} {h : X ⟶ Z} {h' : Z ⟶ Z'} {i : Y ⟶ Z} {i' : Y' ⟶ Z'}
  (hsq₁ : CommSq f g h i) (hsq₂ : CommSq i g' h' i') : CommSq f (g ≫ g') (h ≫ h') i'

Full source

/-- The vertical composition of two commutative squares as below is a commutative square.
```
  W ---f---> X
  |          |
  g          h
  |          |
  v          v
  Y ---i---> Z
  |          |
  g'         h'
  |          |
  v          v
  Y'---i'--> Z'

```
-/
lemma vert_comp {W X Y Y' Z Z' : C} {f : W ⟶ X} {g : W ⟶ Y} {g' : Y ⟶ Y'} {h : X ⟶ Z}
    {h' : Z ⟶ Z'} {i : Y ⟶ Z} {i' : Y' ⟶ Z'} (hsq₁ : CommSq f g h i) (hsq₂ : CommSq i g' h' i') :
    CommSq f (g ≫ g') (h ≫ h') i' :=
  flip (horiz_comp (flip hsq₁) (flip hsq₂))

Vertical Composition of Commutative Squares in a Category

Informal description

Given a category $\mathcal{C}$ and objects $W, X, Y, Y', Z, Z'$ in $\mathcal{C}$, consider morphisms forming two commutative squares: 1. $f: W \to X$, $g: W \to Y$, $h: X \to Z$, $i: Y \to Z$ with $h \circ f = i \circ g$ 2. $g': Y \to Y'$, $h': Z \to Z'$, $i': Y' \to Z'$ with $h' \circ i = i' \circ g'$ Then the vertical composition of these squares forms a new commutative square with: - Top edge: $f: W \to X$ - Left edge: $g \circ g': W \to Y'$ - Right edge: $h \circ h': X \to Z'$ - Bottom edge: $i': Y' \to Z'$ satisfying $(h \circ h') \circ f = i' \circ (g \circ g')$.

CategoryTheory.Functor.map_commSq theorem

(s : CommSq f g h i) : CommSq (F.map f) (F.map g) (F.map h) (F.map i)

Full source

theorem map_commSq (s : CommSq f g h i) : CommSq (F.map f) (F.map g) (F.map h) (F.map i) :=
  ⟨by simpa using congr_arg (fun k : W ⟶ Z => F.map k) s.w⟩

Functorial Preservation of Commutative Squares

Informal description

Given a commutative square in a category $C$ with morphisms $f: W \to X$, $g: W \to Y$, $h: X \to Z$, and $i: Y \to Z$ such that $h \circ f = i \circ g$, then for any functor $F: C \to D$, the image of this square under $F$ is also commutative, i.e., $F(h) \circ F(f) = F(i) \circ F(g)$.

CategoryTheory.CommSq.LiftStruct structure

(sq : CommSq f i p g)

Full source

/-- Now we consider a square:
```
  A ---f---> X
  |          |
  i          p
  |          |
  v          v
  B ---g---> Y
```

The datum of a lift in a commutative square, i.e. an up-right-diagonal
morphism which makes both triangles commute. -/
@[ext]
structure LiftStruct (sq : CommSq f i p g) where
  /-- The lift. -/
  l : B ⟶ X
  /-- The upper left triangle commutes. -/
  fac_left : i ≫ l = f := by aesop_cat
  /-- The lower right triangle commutes. -/
  fac_right : l ≫ p = g := by aesop_cat

Lifting structure for commutative squares

Informal description

Given a commutative square in a category with morphisms as shown: ``` A ---f---> X | | i p | | v v B ---g---> Y ``` a `LiftStruct` for this square is a morphism `l : X ⟶ B` (the "lift") such that both triangles commute: `i = l ∘ f` and `p = g ∘ l`.

CategoryTheory.CommSq.LiftStruct.op definition

{sq : CommSq f i p g} (l : LiftStruct sq) : LiftStruct sq.op

Full source

/-- A `LiftStruct` for a commutative square gives a `LiftStruct` for the
corresponding square in the opposite category. -/
@[simps]
def op {sq : CommSq f i p g} (l : LiftStruct sq) : LiftStruct sq.op where
  l := l.l.op
  fac_left := by rw [← op_comp, l.fac_right]
  fac_right := by rw [← op_comp, l.fac_left]

Opposite lifting structure for a commutative square

Informal description

Given a lifting structure `l` for a commutative square in a category, the opposite lifting structure in the opposite category is obtained by taking the opposite morphism of `l`. Specifically, if `l` is a morphism making the original square commute, then `l.op` makes the opposite square commute.

CategoryTheory.CommSq.LiftStruct.unop definition

 {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} {sq : CommSq f i p g} (l : LiftStruct sq) :
  LiftStruct sq.unop

Full source

/-- A `LiftStruct` for a commutative square in the opposite category
gives a `LiftStruct` for the corresponding square in the original category. -/
@[simps]
def unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} {sq : CommSq f i p g}
    (l : LiftStruct sq) : LiftStruct sq.unop where
  l := l.l.unop
  fac_left := by rw [← unop_comp, l.fac_right]
  fac_right := by rw [← unop_comp, l.fac_left]

Lifting structure for commutative squares in the opposite category induces lifting structure in the original category

Informal description

Given a lifting structure `l` for a commutative square in the opposite category $\mathcal{C}^{\mathrm{op}}$ with morphisms $f \colon A \to X$, $i \colon A \to B$, $p \colon X \to Y$, and $g \colon B \to Y$ such that $p \circ f = g \circ i$, the unopposite lifting structure `l.unop` provides a lift for the corresponding commutative square in the original category $\mathcal{C}$ with morphisms $f^{\mathrm{unop}} \colon \mathrm{unop}\, X \to \mathrm{unop}\, A$, $i^{\mathrm{unop}} \colon \mathrm{unop}\, B \to \mathrm{unop}\, A$, $p^{\mathrm{unop}} \colon \mathrm{unop}\, Y \to \mathrm{unop}\, X$, and $g^{\mathrm{unop}} \colon \mathrm{unop}\, Y \to \mathrm{unop}\, B$ such that $f^{\mathrm{unop}} \circ p^{\mathrm{unop}} = i^{\mathrm{unop}} \circ g^{\mathrm{unop}}$. Specifically, the lift `l.unop` is given by the unopposite of the original lift, ensuring the commutativity of the resulting triangles in $\mathcal{C}$.

CategoryTheory.CommSq.LiftStruct.opEquiv definition

(sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.op

Full source

/-- Equivalences of `LiftStruct` for a square and the corresponding square
in the opposite category. -/
@[simps]
def opEquiv (sq : CommSq f i p g) : LiftStructLiftStruct sq ≃ LiftStruct sq.op where
  toFun := op
  invFun := unop
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Equivalence between lifting structures for a commutative square and its opposite

Informal description

Given a commutative square `sq` in a category $\mathcal{C}$ with morphisms $f \colon A \to X$, $i \colon A \to B$, $p \colon X \to Y$, and $g \colon B \to Y$ such that $p \circ f = g \circ i$, there is an equivalence between the lifting structures for `sq` and the lifting structures for the opposite square `sq.op` in the opposite category $\mathcal{C}^{\mathrm{op}}$. The equivalence is given by taking opposites of lifts and their inverses.

CategoryTheory.CommSq.LiftStruct.unopEquiv definition

 {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : CommSq f i p g) :
  LiftStruct sq ≃ LiftStruct sq.unop

Full source

/-- Equivalences of `LiftStruct` for a square in the oppositive category and
the corresponding square in the original category. -/
def unopEquiv {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
    (sq : CommSq f i p g) : LiftStructLiftStruct sq ≃ LiftStruct sq.unop where
  toFun := unop
  invFun := op
  left_inv := by aesop_cat
  right_inv := by aesop_cat

Equivalence of lifting structures between opposite and original commutative squares

Informal description

Given a commutative square in the opposite category $\mathcal{C}^{\mathrm{op}}$ with morphisms $f \colon A \to X$, $i \colon A \to B$, $p \colon X \to Y$, and $g \colon B \to Y$ such that $p \circ f = g \circ i$, there is an equivalence between the lifting structures for this square and the lifting structures for the corresponding unopposite square in the original category $\mathcal{C}$. The equivalence is given by taking opposites and unopposites of the lifting morphisms.

CategoryTheory.CommSq.subsingleton_liftStruct_of_epi instance

(sq : CommSq f i p g) [Epi i] : Subsingleton (LiftStruct sq)

Full source

instance subsingleton_liftStruct_of_epi (sq : CommSq f i p g) [Epi i] :
    Subsingleton (LiftStruct sq) :=
  ⟨fun l₁ l₂ => by
    ext
    rw [← cancel_epi i]
    simp only [LiftStruct.fac_left]⟩

Uniqueness of Lifts in Commutative Squares with Epimorphisms

Informal description

For any commutative square in a category with morphisms forming the square and with $i$ being an epimorphism, the set of lift structures for this square is a subsingleton (i.e., it has at most one element).

CategoryTheory.CommSq.subsingleton_liftStruct_of_mono instance

(sq : CommSq f i p g) [Mono p] : Subsingleton (LiftStruct sq)

Full source

instance subsingleton_liftStruct_of_mono (sq : CommSq f i p g) [Mono p] :
    Subsingleton (LiftStruct sq) :=
  ⟨fun l₁ l₂ => by
    ext
    rw [← cancel_mono p]
    simp only [LiftStruct.fac_right]⟩

Uniqueness of Lifts in Commutative Squares with Monomorphisms

Informal description

For any commutative square in a category with morphisms forming the square: ``` W ---f---> X | | g h | | v v Y ---i---> Z ``` if the morphism $h$ is a monomorphism, then there is at most one lift structure for this square. That is, the type of lift structures is a subsingleton.

CategoryTheory.CommSq.HasLift structure

Full source

/-- The assertion that a square has a `LiftStruct`. -/
class HasLift : Prop where
  /-- Square has a `LiftStruct`. -/
  exists_lift : Nonempty sq.LiftStruct

Existence of a lift in a commutative square

Informal description

The structure `HasLift` asserts that a given commutative square in a category admits a lift, meaning there exists a morphism that makes the diagram commute. Specifically, for a commutative square formed by morphisms $f: W \to X$, $g: W \to Y$, $h: X \to Z$, and $i: Y \to Z$, the property `HasLift` indicates the existence of a morphism $l: X \to Y$ such that $g = l \circ f$ and $h = i \circ l$.

CategoryTheory.CommSq.HasLift.mk' theorem

(l : sq.LiftStruct) : HasLift sq

Full source

theorem mk' (l : sq.LiftStruct) : HasLift sq :=
  ⟨Nonempty.intro l⟩

Existence of Lift from Lift Structure in Commutative Square

Informal description

Given a commutative square in a category with morphisms forming the square: ``` W ---f---> X | | g h | | v v Y ---i---> Z ``` and a lift structure `l` for this square, the square has a lift, i.e., there exists a morphism that makes the diagram commute.

CategoryTheory.CommSq.HasLift.iff theorem

: HasLift sq ↔ Nonempty sq.LiftStruct

Full source

theorem iff : HasLiftHasLift sq ↔ Nonempty sq.LiftStruct := by
  constructor
  exacts [fun h => h.exists_lift, fun h => mk h]

Existence of Lift in Commutative Square is Equivalent to Nonempty Lifting Structure

Informal description

A commutative square in a category admits a lift if and only if there exists a lifting structure for that square. In other words, given a commutative square formed by morphisms $f: W \to X$, $g: W \to Y$, $h: X \to Z$, and $i: Y \to Z$, the square has a lift precisely when there exists a morphism $l: X \to Y$ such that $g = l \circ f$ and $h = i \circ l$.

CategoryTheory.CommSq.HasLift.iff_op theorem

: HasLift sq ↔ HasLift sq.op

Full source

theorem iff_op : HasLiftHasLift sq ↔ HasLift sq.op := by
  rw [iff, iff]
  exact Nonempty.congr (LiftStruct.opEquiv sq).toFun (LiftStruct.opEquiv sq).invFun

Lift Existence in Commutative Square is Equivalent to Lift Existence in Opposite Square

Informal description

For a commutative square `sq` in a category $\mathcal{C}$, the square has a lift if and only if its opposite square `sq.op` in the opposite category $\mathcal{C}^{\mathrm{op}}$ has a lift.

CategoryTheory.CommSq.HasLift.iff_unop theorem

 {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} (sq : CommSq f i p g) : HasLift sq ↔ HasLift sq.unop

Full source

theorem iff_unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
    (sq : CommSq f i p g) : HasLiftHasLift sq ↔ HasLift sq.unop := by
  rw [iff, iff]
  exact Nonempty.congr (LiftStruct.unopEquiv sq).toFun (LiftStruct.unopEquiv sq).invFun

Equivalence of Liftability in a Commutative Square and its Opposite

Informal description

For a commutative square in the opposite category $\mathcal{C}^{\mathrm{op}}$ with morphisms $f \colon A \to X$, $i \colon A \to B$, $p \colon X \to Y$, and $g \colon B \to Y$, the square admits a lift if and only if the corresponding unopposite square in $\mathcal{C}$ admits a lift.

CategoryTheory.CommSq.lift definition

[hsq : HasLift sq] : B ⟶ X

Full source

/-- A choice of a diagonal morphism that is part of a `LiftStruct` when
the square has a lift. -/
noncomputable def lift [hsq : HasLift sq] : B ⟶ X :=
  hsq.exists_lift.some.l

Diagonal morphism in a commutative square with lift

Informal description

Given a commutative square in a category with a proof that it has a lift, the function `lift` selects a specific diagonal morphism $l \colon B \to X$ that makes both resulting triangles commute. That is, $l$ satisfies $i = l \circ f$ and $p = g \circ l$, where the square is formed by morphisms $f \colon A \to X$, $i \colon A \to B$, $p \colon X \to Y$, and $g \colon B \to Y$.

CategoryTheory.CommSq.fac_left theorem

[hsq : HasLift sq] : i ≫ sq.lift = f

Full source

@[reassoc (attr := simp)]
theorem fac_left [hsq : HasLift sq] : i ≫ sq.lift = f :=
  hsq.exists_lift.some.fac_left

Left Triangle Commutativity in a Liftable Commutative Square

Informal description

Given a commutative square in a category with morphisms $f \colon A \to X$, $i \colon A \to B$, $p \colon X \to Y$, and $g \colon B \to Y$, if the square has a lift (i.e., there exists a morphism $l \colon X \to B$ making both triangles commute), then the composition $i \circ l$ equals $f$.

CategoryTheory.CommSq.fac_right theorem

[hsq : HasLift sq] : sq.lift ≫ p = g

Full source

@[reassoc (attr := simp)]
theorem fac_right [hsq : HasLift sq] : sq.lift ≫ p = g :=
  hsq.exists_lift.some.fac_right

Right Triangle Commutativity in a Lifted Commutative Square

Informal description

Given a commutative square in a category with a lift, the composition of the lift morphism $l$ with the right morphism $p$ equals the bottom morphism $g$, i.e., $l \circ p = g$.

Future work