English
Let s be a compact subset of the base field 𝕜 with 0 ∈ s. Suppose φ is a continuous nonunital star-algebra homomorphism from the algebra of continuous 𝕜-valued functions on s to A, and a ∈ A satisfies φ(id_s) a = 0 and φ(star(id_s)) a = 0. Then for every f in the relevant function algebra, φ(f) a = 0.
Русский
Пусть s — компактный подмножество поля 𝕜 с 0 ∈ s. Пусть φ: C(s, 𝕜)₀ →⋆ₙₐ[𝕜] A — непрерывное ненульевое звёздно-алгомоморфизмfrom алгебры непрерывных функций на s в A, и a ∈ A удовлетворяет φ(id_s) a = 0 и φ(star(id_s)) a = 0. Тогда для каждого f ∈ C(s, 𝕜)₀ выполнено φ(f) a = 0.
LaTeX
$$$\forall s,\, (0 \in s) \Rightarrow \big(\forall φ: C(s, \mathbb{K})_{0} \to_{\ast n a}[\mathbb{K}] A,\; a \in A,\; φ(\mathrm{id}_s)\,a = 0,\; φ(\mathrm{star}(\mathrm{id}_s))\,a = 0,\; φ \text{ continuous} \Rightarrow \forall f \in C(s, \mathbb{K})_{0},\; φ(f)\,a = 0 \big).$$$
Lean4
theorem nonUnitalStarAlgHom_apply_mul_eq_zero {𝕜 A : Type*} [RCLike 𝕜] [NonUnitalSemiring A] [Star A]
[TopologicalSpace A] [ContinuousMul A] [T2Space A] [DistribMulAction 𝕜 A] [IsScalarTower 𝕜 A A] {s : Set 𝕜}
[Fact (0 ∈ s)] [CompactSpace s] (φ : C(s, 𝕜)₀ →⋆ₙₐ[𝕜] A) (a : A) (hmul_id : φ (.id s) * a = 0)
(hmul_star_id : φ (star (.id s)) * a = 0) (hφ : Continuous φ) (f : C(s, 𝕜)₀) : φ f * a = 0 := by
induction f using ContinuousMapZero.induction_on_of_compact with
| zero => simp [map_zero]
| id => exact hmul_id
| star_id => exact hmul_star_id
| add _ _ h₁ h₂ => simp only [map_add, add_mul, h₁, h₂, zero_add]
| mul _ _ _ h => simp only [map_mul, mul_assoc, h, mul_zero]
| smul _ _ h => rw [map_smul, smul_mul_assoc, h, smul_zero]
| frequently f h => exact h.mem_of_closed <| isClosed_eq (by fun_prop) continuous_zero
