English
The intersection of adjoin of restrict(id) with the kernel is equal to adjoin of restrict(id) itself.
Русский
Пересечение адъойн ограниченного id и ядра равно адъойн ограниченного id.
LaTeX
$$$\big(\operatorname{adjoin}_{\mathbb{K}}\{\mathrm{restrict}_{s}(\mathrm{id}_{\mathbb{K}})\}\big) \cap \ker(\mathrm{evalStarAlgHom}_{\mathbb{K},\mathbb{K}}(\langle 0, h_{0} \rangle)) = \operatorname{adjoin}_{\mathbb{K}}\{\mathrm{restrict}_{s}(\mathrm{id}_{\mathbb{K}})\}.$$$
Lean4
theorem ker_evalStarAlgHom_inter_adjoin_id (s : Set 𝕜) (h0 : 0 ∈ s) :
(StarAlgebra.adjoin 𝕜 {restrict s (.id 𝕜)} : Set C(s, 𝕜)) ∩ RingHom.ker (evalStarAlgHom 𝕜 𝕜 (⟨0, h0⟩ : s)) =
adjoin 𝕜 {restrict s (.id 𝕜)} :=
by
ext f
constructor
· rintro ⟨hf₁, hf₂⟩
rw [SetLike.mem_coe] at hf₂ ⊢
simp_rw [adjoin_id_eq_span_one_add, Set.mem_add, SetLike.mem_coe, mem_span_singleton] at hf₁
obtain ⟨-, ⟨r, rfl⟩, f, hf, rfl⟩ := hf₁
have := nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf
simp only [SetLike.mem_coe, RingHom.mem_ker, evalStarAlgHom_apply] at hf₂ this
rw [add_apply, this, add_zero, smul_apply, one_apply, smul_eq_mul, mul_one] at hf₂
rwa [hf₂, zero_smul, zero_add]
· simp only [Set.mem_inter_iff, SetLike.mem_coe]
refine fun hf ↦ ⟨?_, nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom h0 hf⟩
exact adjoin_le_starAlgebra_adjoin _ _ hf
