English
A RingHom can be reinterpreted as a ℚ-algebra homomorphism when the source and target carry ℚ-algebra structures; this yields an algebra hom that respects the rational scalars.
Русский
Кольцеобразное отображение может рассматриваться как ℚ-алгебровый однород, если источнику и цели заданы структуры ℚ-алгебры; получается алгебраический гомоморфизм, сохраняющий рациональные скаляры.
LaTeX
$$$ f : R \\to^+* S \\Rightarrow f \\in R \\to_{\\mathbb{Q}} S. $$$
Lean4
/-- Reinterpret a `RingHom` as a `ℚ`-algebra homomorphism. This actually yields an equivalence,
see `RingHom.equivRatAlgHom`. -/
def toRatAlgHom [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) : R →ₐ[ℚ] S :=
{ f with commutes' := f.map_rat_algebraMap }
