English
The process of adjoining a set and then restricting scalars to a smaller base commutes with restricting scalars from the larger ambient; i.e., two equivalent constructions yield the same restricted subalgebra.
Русский
Объединение множества и последующая строгая редукция по основанию совместимы с редукцией по меньшему основанию: две эквивалентные конструкции дают одну и ту же ограниченную подалгебру.
LaTeX
$$$\\text{Algebra.adjoin C S} \\text{ restricted to } D = \\text{Algebra.adjoin D (image under maps) S } \\text{ restricted to } C$$$
Lean4
theorem adjoin_restrictScalars (C D E : Type*) [CommSemiring C] [CommSemiring D] [CommSemiring E] [Algebra C D]
[Algebra C E] [Algebra D E] [IsScalarTower C D E] (S : Set E) :
(Algebra.adjoin D S).restrictScalars C =
(Algebra.adjoin ((⊤ : Subalgebra C D).map (IsScalarTower.toAlgHom C D E)) S).restrictScalars C :=
by
suffices
Set.range (algebraMap D E) = Set.range (algebraMap ((⊤ : Subalgebra C D).map (IsScalarTower.toAlgHom C D E)) E)
by
ext x
change x ∈ Subsemiring.closure (_ ∪ S) ↔ x ∈ Subsemiring.closure (_ ∪ S)
rw [this]
ext x
constructor
· rintro ⟨y, hy⟩
exact ⟨⟨algebraMap D E y, ⟨y, ⟨Algebra.mem_top, rfl⟩⟩⟩, hy⟩
· rintro ⟨⟨y, ⟨z, ⟨h0, h1⟩⟩⟩, h2⟩
exact ⟨z, Eq.trans h1 h2⟩
