English
If 0 ∈ s, then the nonunital star-algebra generated by restricting the identity to s lies inside the kernel of the evaluation-star-algebra-homomorphism at ⟨0, h0⟩.
Русский
Если 0 ∈ s, то недопустимо единичное звездное подальгебра, порожденное ограничением идентичности на s, содержится в ядре отображения-алгебры, оценивающего в точке ⟨0, h0⟩.
LaTeX
$$$ \operatorname{adjoin}_{\mathbb{k}} \{\operatorname{restrict}_s(\mathrm{id}_{\mathbb{k}})\} \subseteq \ker(\operatorname{evalStarAlgHom}_{\mathbb{k},\mathbb{k}}(\langle 0, h_0 \rangle)) $$$
Lean4
theorem nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom {s : Set 𝕜} (h0 : 0 ∈ s) :
(adjoin 𝕜 {restrict s (.id 𝕜)} : Set C(s, 𝕜)) ⊆ RingHom.ker (evalStarAlgHom 𝕜 𝕜 (⟨0, h0⟩ : s)) :=
by
intro f hf
induction hf using adjoin_induction with
| mem f hf =>
obtain rfl := Set.mem_singleton_iff.mp hf
rfl
| add f g _ _ hf hg => exact add_mem hf hg
| zero => exact zero_mem _
| mul f g _ _ _ hg => exact Ideal.mul_mem_left _ f hg
| smul r f _ hf =>
rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢
rw [map_smul, hf, smul_zero]
| star f _ hf =>
rw [SetLike.mem_coe, RingHom.mem_ker] at hf ⊢
rw [map_star, hf, star_zero]
