hom_coimageImageComparison — Mathlib

English

The Hom version of the coimage iso commutes with the coimage-to-image comparison: the isomorphism hom composed with the coimage comparison on F.map f equals the mapped coimage comparison then composed with the image iso on F.

Русский

Гомоморфизм изоморфизма кообраза коммутирует с сопоставлением кообраз-образ: композиция гомоморфизма изоморфизма кообраза с сопоставлением кообраз-образ для F.map f равна отображению сопоставления кообраз-образ и гомоморфизмомобраза.

LaTeX

$$$(\mathrm{PreservesCoimage.iso} F f).hom \;\gg\; coimageImageComparison (F.map f) = F.map (coimageImageComparison f) \;\gg\; (\mathrm{PreservesImage.iso} F f).hom$$$

Lean4

theorem hom_coimageImageComparison :
    (PreservesCoimage.iso F f).hom ≫ coimageImageComparison (F.map f) =
      F.map (coimageImageComparison f) ≫ (PreservesImage.iso F f).hom :=
  by
  simp [← Functor.map_comp, ← Iso.eq_inv_comp, ← cancel_epi (Abelian.coimage.π (F.map f)),
    ← cancel_mono (Abelian.image.ι (F.map f))]

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