English
The map_desc lemma describes how a commutative diagram with cokernels induces a compatible map between cokernel objects.
Русский
Лемма map_desc описывает, как коммутативный диаграмм с коканалами индуцирует совместимую карту между коканалами.
LaTeX
$$$\text{map_desc } f g w f' g' w' p q r h₁ h₂$ expresses the commutativity of the induced square.$$
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
```
cokernel f ---> Z
| |
| cokernel.map |
| |
v v
cokernel f' --> Z'
```
-/
theorem map_desc {X Y Z X' Y' Z' : C} (f : X ⟶ Y) [HasCokernel f] (g : Y ⟶ Z) (w : f ≫ g = 0) (f' : X' ⟶ Y')
[HasCokernel f'] (g' : Y' ⟶ Z') (w' : f' ≫ g' = 0) (p : X ⟶ X') (q : Y ⟶ Y') (r : Z ⟶ Z') (h₁ : f ≫ q = p ≫ f')
(h₂ : g ≫ r = q ≫ g') : cokernel.map f f' p q h₁ ≫ cokernel.desc f' g' w' = cokernel.desc f g w ≫ r := by ext;
simp [h₂]
