English
A ring hom from R to S with commute property yields a ring hom from Rᵐᵒᵖ to S.
Русский
Гомоморфизм кольца f: R → S с условием коммутирования порождает кольцевой гомоморфизм Rᵐᵒᵖ → S.
LaTeX
$$$\exists \; f^{\mathrm{op}} : R^{\mathrm{op}} \to+* S$ such that $f^{\mathrm{op}}(x) = f(x)$$$
Lean4
/-- A ring homomorphism `f : R →+* S` such that `f x` commutes with `f y` for all `x, y` defines
a ring homomorphism from `Rᵐᵒᵖ`. -/
@[simps -fullyApplied]
def fromOpposite {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ x y, Commute (f x) (f y)) : Rᵐᵒᵖ →+* S :=
{ (f.toAddMonoidHom.comp (opAddEquiv : R ≃+ Rᵐᵒᵖ).symm.toAddMonoidHom : Rᵐᵒᵖ →+ S), f.toMonoidHom.fromOpposite hf with
toFun := f ∘ MulOpposite.unop }
