English
The kernel of evalStarAlgHom equals the closure of adjoin of id.
Русский
Ядро evalStarAlgHom равно замыканию адъойн id.
LaTeX
$$$\ker(\mathrm{evalStarAlgHom}_{\mathbb{K},\mathbb{K}}(\langle 0, h_{0} \rangle)) = \overline{\operatorname{adjoin}_{\mathbb{K}}\{\mathrm{restrict}_{s}(\mathrm{id}_{\mathbb{K}})\}}.$$$
Lean4
theorem ker_evalStarAlgHom_eq_closure_adjoin_id (s : Set 𝕜) (h0 : 0 ∈ s) [CompactSpace s] :
(RingHom.ker (evalStarAlgHom 𝕜 𝕜 (⟨0, h0⟩ : s)) : Set C(s, 𝕜)) = closure (adjoin 𝕜 {(restrict s (.id 𝕜))}) :=
by
rw [← ker_evalStarAlgHom_inter_adjoin_id s h0,
AlgHom.closure_ker_inter (φ := evalStarAlgHom 𝕜 𝕜 (X := s) ⟨0, h0⟩) (continuous_eval_const _) _]
convert (Set.univ_inter _).symm
rw [← Polynomial.toContinuousMapOn_X_eq_restrict_id, ← Polynomial.toContinuousMapOnAlgHom_apply, ←
polynomialFunctions.starClosure_eq_adjoin_X s]
congrm (($(polynomialFunctions.starClosure_topologicalClosure s) : Set C(s, 𝕜)))
