English
Two continuous star-algebra homomorphisms from C(s, 𝕜) into a star algebra A that agree on the X-coordinate are equal.
Русский
Два непрерывных звездно-алгеброморфизма из C(s, 𝕜) в A, совпадающие на X, равны.
LaTeX
$$$\varphi = \psi$ if $\varphi(\mathrm{toContinuousMapOnAlgHom}(s, X)) = \psi(\mathrm{toContinuousMapOnAlgHom}(s, X)).$$$
Lean4
/-- Continuous star algebra homomorphisms from `C(s, 𝕜)` into a star `𝕜`-algebra `A` which agree
at `X : 𝕜[X]` (interpreted as a continuous map) are, in fact, equal. -/
@[ext (iff := false)]
theorem starAlgHom_ext_map_X {𝕜 A : Type*} [RCLike 𝕜] [Ring A] [StarRing A] [Algebra 𝕜 A] [TopologicalSpace A]
[T2Space A] {s : Set 𝕜} [CompactSpace s] {φ ψ : C(s, 𝕜) →⋆ₐ[𝕜] A} (hφ : Continuous φ) (hψ : Continuous ψ)
(h : φ (toContinuousMapOnAlgHom s X) = ψ (toContinuousMapOnAlgHom s X)) : φ = ψ :=
by
suffices (⊤ : StarSubalgebra 𝕜 C(s, 𝕜)) ≤ StarAlgHom.equalizer φ ψ from StarAlgHom.ext fun x => this mem_top
rw [← polynomialFunctions.starClosure_topologicalClosure s]
exact
StarSubalgebra.topologicalClosure_minimal (polynomialFunctions.starClosure_le_equalizer s φ ψ h) (isClosed_eq hφ hψ)
