English
There is a canonical ℚ-algebra homomorphism from A to B whose underlying ring hom is the algebra map algebraMap A B, and it coheres with the scalar action (IsScalarTower).
Русский
Существует канонический ℚ-алгебра-гомоморфизм от A к B, чьим основанным кольцевым гомоморфизмом является алгебраическая карта algebraMap A B, который согласуется с действием скаляров (IsScalarTower).
LaTeX
$$$\\exists \\varphi: A \\to_{\\mathbb{Q}} B \\text{ with } \\varphi\\text{ underlying }(a) = algebraMap A B(a)$$$
Lean4
/-- The algebra morphism underlying `algebraMap` -/
def algHom (R A B : Type*) [CommSemiring R] [CommSemiring A] [Semiring B] [Algebra R A] [Algebra R B] [Algebra A B]
[IsScalarTower R A B] : A →ₐ[R] B where
toRingHom := algebraMap A B
commutes' r := by simpa [Algebra.smul_def] using smul_assoc r (1 : A) (1 : B)
