English
The subalgebra of polynomial functions on s is generated by the image of X under the algebra hom: polynomialFunctions s = Algebra.adjoin_R {toContinuousMapOnAlgHom s X}.
Русский
Подалгебра полином-функций на s порождается образцом X через алгебра-гомоморфизм: polynomialFunctions s = Algebra.adjoin_R {toContinuousMapOnAlgHom s X}.
LaTeX
$$$polynomialFunctions\\,s = Algebra.adjoin\\,R\\{toContinuousMapOnAlgHom\\,s\\,X\\}$$$
Lean4
theorem eq_adjoin_X (s : Set R) : polynomialFunctions s = Algebra.adjoin R {toContinuousMapOnAlgHom s X} :=
by
refine le_antisymm ?_ (Algebra.adjoin_le fun _ h => ⟨X, trivial, (Set.mem_singleton_iff.1 h).symm⟩)
rintro - ⟨p, -, rfl⟩
rw [AlgHom.coe_toRingHom]
refine p.induction_on (fun r => ?_) (fun f g hf hg => ?_) fun n r hn => ?_
· rw [Polynomial.C_eq_algebraMap, AlgHomClass.commutes]
exact Subalgebra.algebraMap_mem _ r
· rw [map_add]
exact add_mem hf hg
· rw [pow_succ, ← mul_assoc, map_mul]
exact mul_mem hn (Algebra.subset_adjoin <| Set.mem_singleton _)
