English
There is a canonical equivalence between RingHom R S and RingHom Rᵐᵒᵖ Sᵐᵒᵖ.
Русский
Существует каноническая эквивалентность между RingHom R S и RingHom Rᵐᵒᵖ Sᵐᵒᵖ.
LaTeX
$$$\text{RingHom}(R,S) \cong \text{RingHom}(R^{\mathrm{op}}, S^{\mathrm{op}})$$$
Lean4
/-- A ring homomorphism `f : R →+* S` such that `f x` commutes with `f y` for all `x, y` defines
a ring homomorphism to `Sᵐᵒᵖ`. -/
@[simps -fullyApplied]
def toOpposite {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ x y, Commute (f x) (f y)) : R →+* Sᵐᵒᵖ :=
{ ((opAddEquiv : S ≃+ Sᵐᵒᵖ).toAddMonoidHom.comp ↑f : R →+ Sᵐᵒᵖ), f.toMonoidHom.toOpposite hf with
toFun := MulOpposite.op ∘ f }
