English
The restriction of scalars of adjoin equals the join of the scalar-range and adjoin; i.e., (adjoin S s).restrictScalars R = range ⊔ adjoin R s.
Русский
Ограничение скаляров для адъюнкта равняется объединению диапазона и адъюнкта: (adjoin S s).restrictScalars R = range ⊔ adjoin R s.
LaTeX
$$$ (adjoin S s).restrictScalars R = (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R s $$$
Lean4
theorem restrictScalars_adjoin {s : Set A} :
(adjoin S s).restrictScalars R = (IsScalarTower.toAlgHom R S A).range ⊔ adjoin R s :=
by
refine
le_antisymm
(fun _ hx ↦
adjoin_induction (fun x hx ↦ le_sup_right (α := Subalgebra R A) (subset_adjoin hx))
(fun x ↦ le_sup_left (α := Subalgebra R A) ⟨x, rfl⟩) (fun _ _ _ _ ↦ add_mem) (fun _ _ _ _ ↦ mul_mem) <|
(Subalgebra.mem_restrictScalars _).mp hx)
(sup_le ?_ <| adjoin_le subset_adjoin)
rintro _ ⟨x, rfl⟩; exact algebraMap_mem (adjoin S s) x
