English
There is an equivalence RingHom R S ≃ RingHom Rᵐᵒᵖ Sᵐᵒᵖ.
Русский
Существует эквивалентность RingHom R S ≃ RingHom Rᵐᵒᵖ Sᵐᵒᵖ.
LaTeX
$$$\text{RingHom}(R,S) \simeq \text{RingHom}(R^{\mathrm{op}}, S^{\mathrm{op}})$$$
Lean4
/-- A ring hom `R →+* S` can equivalently be viewed as a ring hom `Rᵐᵒᵖ →+* Sᵐᵒᵖ`. This is the
action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[simps!]
def op {R S} [NonAssocSemiring R] [NonAssocSemiring S] : (R →+* S) ≃ (Rᵐᵒᵖ →+* Sᵐᵒᵖ)
where
toFun f := { AddMonoidHom.mulOp f.toAddMonoidHom, MonoidHom.op f.toMonoidHom with }
invFun f := { AddMonoidHom.mulUnop f.toAddMonoidHom, MonoidHom.unop f.toMonoidHom with }
