English
An additive semigroup homomorphism f: M →+ N is equivalently viewed as a homomorphism f: M^op →+ N^op via the 'op' operation, yielding a natural equivalence between AddHom M N and AddHom M^op N^op.
Русский
Аддитивный полугрупповый гомоморфизм f: M →+ N эквивалентно рассматривается как гомоморфизм f: M^op →+ N^op через операцию 'op', образуя естественное эквивалентное соответствие между AddHom M N и AddHom M^op N^op.
LaTeX
$$$\\operatorname{AddHom}(M,N) \\simeq \\operatorname{AddHom}(M^{op}, N^{op})$$$
Lean4
/-- An additive semigroup homomorphism `AddHom M N` can equivalently be viewed as an additive
homomorphism `AddHom Mᵐᵒᵖ Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on
morphisms. -/
@[simps]
def mulOp {M N} [Add M] [Add N] : AddHom M N ≃ AddHom Mᵐᵒᵖ Nᵐᵒᵖ
where
toFun
f := { toFun := MulOpposite.op ∘ f ∘ MulOpposite.unop, map_add' x y := unop_injective (f.map_add x.unop y.unop) }
invFun
f :=
{ toFun := MulOpposite.unop ∘ f ∘ MulOpposite.op,
map_add' := fun x y => congrArg MulOpposite.unop (f.map_add (MulOpposite.op x) (MulOpposite.op y)) }
