English
There is a natural equivalence between non-unital ring homomorphisms R → S and Rᵐᵒᵖ → Sᵐᵒᵖ.
Русский
Существует естественное эквивалентность между неабсолютно не единичными гомоморфизмами R → S и Rᵐᵒᵖ → Sᵐᵒᵖ.
LaTeX
$$$\operatorname{NonUnitalRingHom}(R,S) \cong \operatorname{NonUnitalRingHom}(R^{\mathrm{op}}, S^{\mathrm{op}})$$$
Lean4
/-- A non-unital ring hom `R →ₙ+* S` can equivalently be viewed as a non-unital ring hom
`Rᵐᵒᵖ →+* Sᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[simps]
def op {R S} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : (R →ₙ+* S) ≃ (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ)
where
toFun f := { AddMonoidHom.mulOp f.toAddMonoidHom, MulHom.op f.toMulHom with }
invFun f := { AddMonoidHom.mulUnop f.toAddMonoidHom, MulHom.unop f.toMulHom with }
