English
A monoid homomorphism f: M →* N corresponds to a monoid homomorphism f^op: M^op →* N^op, yielding a natural equivalence MonoidHom.op between MonoidHom M N and MonoidHom M^op N^op.
Русский
Моноидный гомоморфизм f: M →* N эквивалентно гомоморфизму f^op: M^op →* N^op, образуя естественное эквивалентное отображение MonoidHom.op между MonoidHom M N и MonoidHom M^op N^op.
LaTeX
$$$\\mathrm{MonoidHom}(M,N) \\simeq \\mathrm{MonoidHom}(M^{op},N^{op})$$$
Lean4
/-- A monoid homomorphism `M →* N` can equivalently be viewed as a monoid homomorphism
`Mᵐᵒᵖ →* Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[to_additive (attr := simps) /--
An additive monoid homomorphism `M →+ N` can equivalently be viewed as an additive monoid
homomorphism `Mᵃᵒᵖ →+ Nᵃᵒᵖ`. This is the action of the (fully faithful)
`ᵃᵒᵖ`-functor on morphisms. -/
]
def op {M N} [MulOneClass M] [MulOneClass N] : (M →* N) ≃ (Mᵐᵒᵖ →* Nᵐᵒᵖ)
where
toFun
f :=
{ toFun := MulOpposite.op ∘ f ∘ unop, map_one' := congrArg MulOpposite.op f.map_one,
map_mul' x y := unop_injective (f.map_mul y.unop x.unop) }
invFun
f :=
{ toFun := unop ∘ f ∘ MulOpposite.op, map_one' := congrArg unop f.map_one,
map_mul' x y := congrArg unop (f.map_mul (MulOpposite.op y) (MulOpposite.op x)) }
