English
Let f: X → Y be a morphism in an abelian category with kernels and cokernels. The mono component of the canonical image factorisation of f coincides with the composite of the cokernel projection from X to the cokernel of ker f and the coimage–image comparison map. In symbols, (imageMonoFactorisation f).e = cokernel.π(ker.ι f) ≫ Abelian.coimageImageComparison f.
Русский
Пусть f: X → Y — морфизм в абелевой категории, имеющей канонические ядра и коки. Моно-компонента канонической факторизации изображения f совпадает с композицией отделения коконера ядра f и отображения кообраза в образ. Формально: (imageMonoFactorisation f).e = cokernel.π(ker.ι f) ≫ Abelian.coimageImageComparison f.
LaTeX
$$$$ (imageMonoFactorisation f).e \;=\; \\operatorname{cokernel}.\\pi(\\ker\\iota_f) \\;\\circ\\; \\operatorname{coimageImageComparison}(f). $$$$
Lean4
theorem imageMonoFactorisation_e' {X Y : C} (f : X ⟶ Y) :
(imageMonoFactorisation f).e = cokernel.π _ ≫ Abelian.coimageImageComparison f :=
by
dsimp
ext
simp only [Abelian.coimageImageComparison, Category.assoc, cokernel.π_desc_assoc]
