imageOpOp — Mathlib

English

Let C be an abelian category and f: X → Y a morphism. Then the opposite of the image of f is canonically isomorphic to the image of f^{op}.

Русский

Пусть C является абелевой категорией и f: X → Y — морфизм. Тогда противоположность образа f естественно изоморфна образу f^{op}.

LaTeX

$$$ (\operatorname{image} f)^{op} \cong \operatorname{image}(f^{op}) $$$

Lean4

/-- The opposite of the image of `f` is the image of `f.op`. -/
def imageOpOp : Opposite.op (image f) ≅ image f.op :=
  imageUnopOp f.op

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