English
If A is generated by s over R, then the A-algebra generated by t, after restricting scalars to R, equals the R-algebra generated by the image of s under the A-to-B algebra map union t.
Русский
Если A порождается над R множеством s, то алгебра над A, порождаемая t, после ограничения скаляров к R равна adjoin R((algebraMap A B)''s) ∪ t.
LaTeX
$$$\\bigl(\\operatorname{adjoin}_A t\\bigr)\\restriction_R = \\operatorname{adjoin}_R\\bigl((\\operatorname{algebraMap}\\ A B\\,''\\, s) \\cup t\\bigr)$$$
Lean4
/-- If `A` is spanned over `R` by `s`, then the algebra spanned over `A` by `t` is the equal to the
algebra spanned over `R` by `s ∪ t`.
-/
theorem adjoin_eq_adjoin_union [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (s : Set A)
(t : Set B) (hS : adjoin R s = ⊤) : (adjoin A t).restrictScalars R = adjoin R ((algebraMap A B '' s) ∪ t) :=
by
have := congr_arg (Subalgebra.map (IsScalarTower.toAlgHom R A B)) hS
rw [Algebra.map_top, AlgHom.map_adjoin, IsScalarTower.coe_toAlgHom'] at this
rw [adjoin_union_eq_adjoin_adjoin, this, ← IsScalarTower.adjoin_range_toAlgHom]
