factorThruCoimage_iso_hom — Mathlib

English

The coimage isomorphism hom, followed by the mapped factorThroughCoimage, equals the mapped coimage factorThroughCoimage: the isomorphism preserves the factorThroughCoimage via its hom.

Русский

Гомоморфизм изоморфизма кообраза, затем отображение через F от factorThroughCoimage, равен отображению coimage через F.

LaTeX

$$$(\mathrm{PreservesCoimage.iso} F f).hom \;\gg\; \operatorname{Abelian.factorThruCoimage} (F.map f) = F.map(\operatorname{Abelian.factorThruCoimage} f)$$$

Lean4

@[reassoc (attr := simp)]
theorem factorThruCoimage_iso_hom :
    (PreservesCoimage.iso F f).hom ≫ Abelian.factorThruCoimage (F.map f) = F.map (Abelian.factorThruCoimage f) := by
  simp [← Iso.eq_inv_comp]

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