English
Let M and N be semigroups. The operation that sends a homomorphism from M^op to N^op to a homomorphism from M to N establishes a natural equivalence between the two hom-sets; this equivalence is inverse to the opposite operation on morphisms.
Русский
Пусть M и N — полугруппы. Операция, отправляющая гомоморфизм M^op → N^op в гомоморфизм M → N, образует естественное эквивалентное соответствие между двумя множествами гомоморфизмов; это соответствие обратимо относительно операции Opp на морфизмах.
LaTeX
$$$\\operatorname{MulHom}(M^{op}, N^{op}) \\simeq \\operatorname{MulHom}(M, N)$$$
Lean4
/-- The 'unopposite' of a semigroup homomorphism `Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ`. Inverse to `MulHom.op`. -/
@[to_additive (attr := simp) /-- The 'unopposite' of an additive semigroup homomorphism
`Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ`. Inverse to `AddHom.op`. -/
]
def unop {M N} [Mul M] [Mul N] : (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N) :=
MulHom.op.symm
