English
For f and g with depends on p, q and hpq, the equality cokernel.map ... ≫ cokernelComparison g G = cokernelComparison f G ≫ G.map (cokernel.map f g p q hpq) holds.
Русский
Для f, g с параметрами p, q и hpq выполняется тождество между cokernel.map и cokernelComparison после отображения.
LaTeX
$$$cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) (by rw [\u2190 G.map_comp, hpq, G.map_comp]) ≫ cokernelComparison g G = cokernelComparison f G ≫ G.map (cokernel.map f g p q hpq)$$$
Lean4
@[reassoc]
theorem cokernel_map_comp_cokernelComparison {X' Y' : C} [HasCokernel f] [HasCokernel (G.map f)] (g : X' ⟶ Y')
[HasCokernel g] [HasCokernel (G.map g)] (p : X ⟶ X') (q : Y ⟶ Y') (hpq : f ≫ q = p ≫ g) :
cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) (by rw [← G.map_comp, hpq, G.map_comp]) ≫
cokernelComparison _ G =
cokernelComparison _ G ≫ G.map (cokernel.map f g p q hpq) :=
cokernel.map_desc _ _ (by rw [← G.map_comp, cokernel.condition, G.map_zero]) _ _
(by rw [← G.map_comp, cokernel.condition, G.map_zero]) _ _ _ _
(by simp only [← G.map_comp]; exact G.congr_map (cokernel.π_desc _ _ _))
