English
Let f: R →+* S be a ring homomorphism between ℚ-algebras, and r ∈ ℚ. Then f(algebraMap ℚ R r) = algebraMap ℚ S r; i.e., f respects the canonical embedding of the rational numbers.
Русский
Пусть f: R →+* S — кольцо-гомоморфизм между ℚ-алгебрами. Тогда для любого r ∈ ℚ выполняется f(algebraMap ℚ R r) = algebraMap ℚ S r; т.е. f сохраняет каноническое вложение рациональных чисел.
LaTeX
$$$$ f \\circ algebraMap_\\mathbb{Q} R = algebraMap_\\mathbb{Q} S $$$$
Lean4
@[simp]
theorem map_rat_algebraMap [Semiring R] [Semiring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) (r : ℚ) :
f (algebraMap ℚ R r) = algebraMap ℚ S r :=
RingHom.ext_iff.1 (Subsingleton.elim (f.comp (algebraMap ℚ R)) (algebraMap ℚ S)) r
