English
The unop operation provides an inverse to op on monoid homomorphisms, establishing an equivalence between MonoidHom(M^op,N^op) and MonoidHom M N.
Русский
Операция разоплощения является обратной к Opposite на моноидных гомоморфизмах, устанавливая эквиваленцию между MonoIdHom(M^op,N^op) и MonoidHom M N.
LaTeX
$$$\\operatorname{MonoidHom}(M^{op},N^{op}) \\simeq \\operatorname{MonoidHom}(M,N)$$$
Lean4
/-- The 'unopposite' of a monoid homomorphism `Mᵐᵒᵖ →* Nᵐᵒᵖ`. Inverse to `MonoidHom.op`. -/
@[to_additive (attr := simp) /-- The 'unopposite' of an additive monoid homomorphism
`Mᵃᵒᵖ →+ Nᵃᵒᵖ`. Inverse to `AddMonoidHom.op`. -/
]
def unop {M N} [MulOneClass M] [MulOneClass N] : (Mᵐᵒᵖ →* Nᵐᵒᵖ) ≃ (M →* N) :=
MonoidHom.op.symm
