English
Let X′ → Y′ be a morphism g with HasCokernel g and HasCokernel (G.map g), and suppose f: X → Y, with p, q morphisms and hpq: f ≫ q = p ≫ g. Then the cokernel maps intertwine with the preservers of cokernels via the isomorphism (PreservesCokernel.iso G f).hom, giving a natural compatibility equality between mapped and non-mapped cokernel maps.
Русский
Пусть g: X′ → Y′ имеет cokernel и G сохраняет cokernel g, а также f: X → Y с отображениями p, q и hpq: f ≫ q = p ≫ g. Тогда отображения cokernel и соответствующие изоморфизмы согласованы: композиции через cokernel.map и через G.map сопряжены через (PreservesCokernel.iso G f).hom.
LaTeX
$$$(\mathrm{PreservesCokernel.iso\ G\ f}).\mathrm{hom} \; \circ \; \mathrm{cokernel.map}(G.map f, G.map g, G.map p, G.map q) = G.map(\mathrm{cokernel.map}(f,g,p,q,hpq)) \circ (\mathrm{PreservesCokernel.iso G f}).hom$$
Lean4
@[reassoc]
theorem preserves_cokernel_iso_comp_cokernel_map {X' Y' : C} (g : X' ⟶ Y') [HasCokernel g] [HasCokernel (G.map g)]
[PreservesColimit (parallelPair g 0) G] (p : X ⟶ X') (q : Y ⟶ Y') (hpq : f ≫ q = p ≫ g) :
(PreservesCokernel.iso G _).hom ≫
cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) (by rw [← G.map_comp, hpq, G.map_comp]) =
G.map (cokernel.map f g p q hpq) ≫ (PreservesCokernel.iso G _).hom :=
by
rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]
