English
For any set t ⊆ A, restricting scalars to R of Algebra.adjoin (toAlgHom R S A).range t equals Algebra.adjoin S t restricted to R; i.e., the restricted algebras coincide.
Русский
Для любого множества t ⊆ A ограничение скаляров R на Algebra.adjoin (toAlgHom R S A).range t совпадает с Algebra.adjoin S t, ограниченным по R.
LaTeX
$$$\restrictScalars R (Algebra.adjoin (toAlgHom R S A).range t) = \restrictScalars R (Algebra.adjoin S t)$$$
Lean4
theorem adjoin_range_toAlgHom (t : Set A) :
(Algebra.adjoin (toAlgHom R S A).range t).restrictScalars R = (Algebra.adjoin S t).restrictScalars R :=
Subalgebra.ext fun z ↦
show
z ∈ Subsemiring.closure (Set.range (algebraMap (toAlgHom R S A).range A) ∪ t : Set A) ↔
z ∈ Subsemiring.closure (Set.range (algebraMap S A) ∪ t : Set A)
by
suffices Set.range (algebraMap (toAlgHom R S A).range A) = Set.range (algebraMap S A) by rw [this]
ext z
exact ⟨fun ⟨⟨_, y, h1⟩, h2⟩ ↦ ⟨y, h2 ▸ h1⟩, fun ⟨y, hy⟩ ↦ ⟨⟨z, y, hy⟩, rfl⟩⟩
