English
There exists a commutative square linking kernel.lift and kernel.map when a commutative diagram with zero compositions is given.
Русский
Существует коммутативный квадрат, связывающий kernel.lift и kernel.map при заданном диаграмме с нулевыми композициями.
LaTeX
$$$\\forall f,g,\\; w:\\; f\\circ g=0\\;\\Rightarrow\\; \\text{коммутативность между } \\mathrm{lift} \\text{ и } \\mathrm{map}$$$
Lean4
/-- Given a commutative diagram
```
X --f--> Y --g--> Z
| | |
| | |
v v v
X' -f'-> Y' -g'-> Z'
```
with horizontal arrows composing to zero,
then we obtain a commutative square
```
X ---> kernel g
| |
| | kernel.map
| |
v v
X' --> kernel g'
```
-/
theorem lift_map {X Y Z X' Y' Z' : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKernel g] (w : f ≫ g = 0) (f' : X' ⟶ Y')
(g' : Y' ⟶ Z') [HasKernel g'] (w' : f' ≫ g' = 0) (p : X ⟶ X') (q : Y ⟶ Y') (r : Z ⟶ Z') (h₁ : f ≫ q = p ≫ f')
(h₂ : g ≫ r = q ≫ g') : kernel.lift g f w ≫ kernel.map g g' q r h₂ = p ≫ kernel.lift g' f' w' := by ext; simp [h₁]
