English
Let f be a ring homomorphism f: R →+* S. Then f induces an f-semilinear map from R to S, with toFun equal to f and the scalar compatibility given by map_smul' = f.map_mul; i.e., for all r, a ∈ R one has f(ra) = f(r) f(a).
Русский
Пусть f: R →+* S — кольцевой гомоморфизм. Тогда он порождает f‑семилинейное отображение R → S, у которого функция‑основа равна f, и для скалярного умножения выполняется совместимость f(r a) = f(r) f(a) для всех r, a ∈ R.
LaTeX
$$$\exists \varphi: R \to S\;\;\text{such that}\;\;\varphi = f \;\land\; \forall r,a \in R:\; \varphi(ra) = f(r)\,\varphi(a) \land \varphi(r+s)=\varphi(r)+\varphi(s).$$$
Lean4
/-- Interpret a `RingHom` `f` as an `f`-semilinear map. -/
@[simps]
def _root_.RingHom.toSemilinearMap (f : R →+* S) : R →ₛₗ[f] S :=
{ f with map_smul' := f.map_mul }
