English
If i: L ≃ₐ[F] L' is an isomorphism compatible with E-over-L towers, then for any S ⊆ E the restricted adjoin over F is equal for L and L'.
Русский
Если i: L ≃ₐ[F] L' совместим с E-расширениями L и L', то для любого S⊆E равны ограниченные скалярами адъюнкции по F для L и L'.
LaTeX
$$$\\forall S,\\; (\\operatorname{adjoin}_L S).restrictScalars F = (\\operatorname{adjoin}_{L'} S).restrictScalars F$$$
Lean4
/-- If `E / L / F` and `E / L' / F` are two ring extension towers, `L ≃ₐ[F] L'` is an isomorphism
compatible with `E / L` and `E / L'`, then for any subset `S` of `E`, `L[S]` and `L'[S]` are
equal as subalgebras of `E / F`. -/
theorem restrictScalars_adjoin_of_algEquiv {F E L L' : Type*} [CommSemiring F] [CommSemiring L] [CommSemiring L']
[Semiring E] [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E] [Algebra F E] [IsScalarTower F L E]
[IsScalarTower F L' E] (i : L ≃ₐ[F] L') (hi : algebraMap L E = (algebraMap L' E) ∘ i) (S : Set E) :
(Algebra.adjoin L S).restrictScalars F = (Algebra.adjoin L' S).restrictScalars F :=
by
apply_fun Subalgebra.toSubsemiring using fun K K' h ↦ by rwa [SetLike.ext'_iff] at h ⊢
change Subsemiring.closure _ = Subsemiring.closure _
rw [hi, Set.range_comp, EquivLike.range_eq_univ, Set.image_univ]
