coimageIsoImage'_hom — Mathlib

English

A precise description of the hom component of the map coimageIsoImage' f, equal to a cokernel-desc from kernel to image factors.

Русский

Точная формула для гомоморфизма coimageIsoImage' f через описатель cokernel-desc от kernel к image.

LaTeX

$$$$ (coimageIsoImage' f).hom = \\operatorname{cokernel.desc} \\, (\\operatorname{kernel.}\\iota f) \\, (\\operatorname{factorThruImage} f) \\, \\cdots $$$$

Lean4

theorem coimageIsoImage'_hom :
    (coimageIsoImage' f).hom = cokernel.desc _ (factorThruImage f) (by simp [← cancel_mono (Limits.image.ι f)]) :=
  by
  ext
  simp only [← cancel_mono (Limits.image.ι f), IsImage.isoExt_hom, cokernel.π_desc, Category.assoc, IsImage.lift_ι,
    coimageStrongEpiMonoFactorisation_m, Limits.image.fac]

Похожие утверждения