factorThruCoimage_iso_inv — Mathlib

English

The inverse of the coimage isomorphism interacts with the mapped factorThroughCoimage in a canonical way: the inverse composed with F.map of factorThroughCoimage f equals factorThroughCoimage of F.map f.

Русский

Обратный к изоморфизму кообраза взаимодействует с отображением через кообраз в каноническом виде: обратное композиционное с отображением F.map от factorThroughCoimage f равно factorThroughCoimage (F.map f).

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem factorThruCoimage_iso_inv :
    (PreservesCoimage.iso F f).inv ≫ F.map (Abelian.factorThruCoimage f) = Abelian.factorThruCoimage (F.map f) := by
  ext; simp [iso]

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