English
For a Submonoid M of R, the algebra map to B sends the image of M through A to the same submonoid as mapping M directly, i.e. algebraMapSubmonoid B (algebraMapSubmonoid A M) = algebraMapSubmonoid B M.
Русский
Для подмоноида M в R отображение через алгебраMap в B дает тот же подмножество, что и прямое отображение M в B, то есть равенство алгебраMapSubmonoid B (algebraMapSubmonoid A M) = algebraMapSubmonoid B M.
LaTeX
$$$\\\\operatorname{algebraMapSubmonoid} B (\\\\operatorname{algebraMapSubmonoid} A M) = \\\\operatorname{algebraMapSubmonoid} B M$$$
Lean4
@[simp]
theorem algebraMapSubmonoid_map_map {R A B : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A] (M : Submonoid R)
[CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] :
algebraMapSubmonoid B (algebraMapSubmonoid A M) = algebraMapSubmonoid B M :=
algebraMapSubmonoid_map_eq _ (IsScalarTower.toAlgHom R A B)
