English
Two continuous algebra homomorphisms from C(s, ℝ) into an ℝ-algebra A that agree on the coordinate X must be equal.
Русский
Два непрерывных алгебра-гомоморфизма из C(s, ℝ) в A, которые совпадают на координате X, совпадают.
LaTeX
$$$\varphi = \psi$ if $\varphi(\mathrm{toContinuousMapOnAlgHom}(s, X)) = \psi(\mathrm{toContinuousMapOnAlgHom}(s, X)).$$$
Lean4
/-- Continuous algebra homomorphisms from `C(s, ℝ)` into an `ℝ`-algebra `A` which agree
at `X : 𝕜[X]` (interpreted as a continuous map) are, in fact, equal. -/
@[ext (iff := false)]
theorem algHom_ext_map_X {A : Type*} [Semiring 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 (⊤ : Subalgebra ℝ C(s, ℝ)) ≤ AlgHom.equalizer φ ψ from AlgHom.ext fun x => this (by trivial)
rw [← polynomialFunctions.topologicalClosure s]
exact Subalgebra.topologicalClosure_minimal (polynomialFunctions.le_equalizer s φ ψ h) (isClosed_eq hφ hψ)
