opHom — Mathlib

English

There is an additive monoid homomorphism opHom(X,Y) from Hom(X,Y) to Hom(op Y, op X) given by f ↦ f^{op}. This respects addition.

Русский

Существует аддитивное однородное отображение opHom(X,Y): Hom(X,Y) →+ Hom(op Y, op X), заданное f ↦ f^{op}. Оно сохраняет сложение.

LaTeX

$$$ \\mathrm{opHom}(X,Y): \\mathrm{Hom}(X,Y) \\to^+ \\mathrm{Hom}(\\mathrm{op}\\,Y, \\mathrm{op}\,X), \\quad f \\mapsto f^{\\mathrm{op}} $$$

Lean4

/-- `op` induces morphisms of monoids on hom groups of a preadditive category -/
@[simps!]
def opHom (X Y : C) : (X ⟶ Y) →+ (Opposite.op Y ⟶ Opposite.op X) :=
  AddMonoidHom.mk' (fun f => f.op) fun f g => op_add _ f g

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