English
An extensionality lemma for cokernel relative to an image: if x = y plus a boundary coming from the image, then their cokernel images coincide.
Русский
Лемма экстенсивности для котонела по изображению: если x равно y плюс границе из образа, то их образы в котокелле равны.
LaTeX
$$$x = y + g(\operatorname{factorThruImageSubobject}(f)(l)) \Rightarrow \pi_g(x) = \pi_g(y)$$$
Lean4
/-- An extensionality lemma showing that two elements of a cokernel by an image
are equal if they differ by an element of the image.
The application is for homology:
two elements in homology are equal if they differ by a boundary.
-/
theorem cokernel_π_imageSubobject_ext {L M N : ModuleCat.{v} R} (f : L ⟶ M) [HasImage f]
(g : (imageSubobject f : ModuleCat.{v} R) ⟶ N) [HasCokernel g] {x y : N} (l : L)
(w : x = y + g (factorThruImageSubobject f l)) : cokernel.π g x = cokernel.π g y :=
by
subst w
simp
