imageUnopOp — Mathlib

English

The opposite of the image of g.unop is isomorphic to the image of g.

Русский

Противоположность образа g.unop изоморфна образу g.

LaTeX

$$$ \operatorname{Opposite.op}(\operatorname{image}(g.unop)) \cong \operatorname{image}(g) $$$

Lean4

/-- The opposite of the image of `g.unop` is the image of `g.` -/
def imageUnopOp : Opposite.op (image g.unop) ≅ image g :=
  (Abelian.imageIsoImage _).op ≪≫
    (cokernelOpOp _).symm ≪≫
      cokernelIsoOfEq (cokernel.π_unop _) ≪≫ cokernelEpiComp _ _ ≪≫ cokernelCompIsIso _ _ ≪≫ Abelian.coimageIsoImage' _

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