English
There is a natural equivalence between semigroup homomorphisms M → N and Mᵒᵖ → Nᵒᵖ, given by f ↦ (MulOpposite.op ∘ f ∘ unop).
Русский
Существует естественное эквивалентность между гомоморфизмами полугрупп M → N и Mᵒᵖ → Nᵒᵖ, заданная отображением f ↦ (MulOpposite.op ∘ f ∘ unop).
LaTeX
$$$ \mathrm{MulHom}(M,N) \cong \mathrm{MulHom}(M^{\mathrm{op}},N^{\mathrm{op}}),\quad f \mapsto (x^{\mathrm{op}} \mapsto f(x)^{\mathrm{op}}) $$$
Lean4
/-- A semigroup homomorphism `M →ₙ* N` can equivalently be viewed as a semigroup homomorphism
`Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[to_additive (attr := simps) /--
An additive semigroup homomorphism `AddHom M N` can equivalently be viewed as an additive
semigroup homomorphism `AddHom Mᵃᵒᵖ Nᵃᵒᵖ`. This is the action of the (fully faithful)`ᵃᵒᵖ`-functor
on morphisms. -/
]
def op {M N} [Mul M] [Mul N] : (M →ₙ* N) ≃ (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ)
where
toFun f := { toFun := MulOpposite.op ∘ f ∘ unop, map_mul' x y := unop_injective (f.map_mul y.unop x.unop) }
invFun
f :=
{ toFun := unop ∘ f ∘ MulOpposite.op,
map_mul' x y := congrArg unop (f.map_mul (MulOpposite.op y) (MulOpposite.op x)) }
