English
The additive op functor yields an equivalence between AddMonoidEnd M and MonoidEnd (Multiplicative M) via AddMonoidHom.toMultiplicative, with the multiplicative structure preserved.
Русский
Функтор противоположности задаёт эквиваленцию между End AddMonoid и End Monoid (Multiplicative M) через AddMonoidHom.toMultiplicative, сохраняя умножение.
LaTeX
$$$\\operatorname{AddMonoidEnd}(M) \\simeq \\operatorname{MonoidEnd}(\\text{Multiplicative } M)$$$
Lean4
/-- An additive homomorphism `M →+ N` can equivalently be viewed as an additive homomorphism
`Mᵐᵒᵖ →+ Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[simps]
def mulOp {M N} [AddZeroClass M] [AddZeroClass N] : (M →+ N) ≃ (Mᵐᵒᵖ →+ Nᵐᵒᵖ)
where
toFun
f :=
{ toFun := MulOpposite.op ∘ f ∘ MulOpposite.unop, map_zero' := unop_injective f.map_zero,
map_add' x y := unop_injective (f.map_add x.unop y.unop) }
invFun
f :=
{ toFun := MulOpposite.unop ∘ f ∘ MulOpposite.op, map_zero' := congrArg MulOpposite.unop f.map_zero,
map_add' := fun x y => congrArg MulOpposite.unop (f.map_add (MulOpposite.op x) (MulOpposite.op y)) }
