English
There exists a maximal ideal I with I = idealOfSet 𝕜 (X \\ {x}) for some x ∈ X; this expresses the maximal–singleton complement correspondence.
Русский
Существует максимальный идеал I, который равен idealOfSet 𝕜 (X \\ {x}) для некоторой x в X; демонстрирует соответствие максимум–комплемент одиночки.
LaTeX
$$$\\exists x: X, (\\mathrm{idealOfSet}(𝕜, X\\setminus\\{x\\}))\\IsMaximal$$
Lean4
theorem continuousMapEval_bijective : Bijective (continuousMapEval X 𝕜) :=
by
refine ⟨fun x y hxy => ?_, fun φ => ?_⟩
· contrapose! hxy
rcases
exists_continuous_zero_one_of_isClosed (isClosed_singleton : _root_.IsClosed { x })
(isClosed_singleton : _root_.IsClosed { y }) (Set.disjoint_singleton.mpr hxy) with
⟨f, fx, fy, -⟩
rw [DFunLike.ne_iff]
use (⟨fun (x : ℝ) => (x : 𝕜), RCLike.continuous_ofReal⟩ : C(ℝ, 𝕜)).comp f
simpa only [continuousMapEval_apply_apply, ContinuousMap.comp_apply, coe_mk, Ne, RCLike.ofReal_inj] using
((fx (Set.mem_singleton x)).symm ▸ (fy (Set.mem_singleton y)).symm ▸ zero_ne_one : f x ≠ f y)
· obtain ⟨x, hx⟩ := (ideal_isMaximal_iff (RingHom.ker φ)).mp inferInstance
refine ⟨x, CharacterSpace.ext_ker <| Ideal.ext fun f => ?_⟩
simpa only [RingHom.mem_ker, continuousMapEval_apply_apply, mem_idealOfSet_compl_singleton, RingHom.mem_ker] using
SetLike.ext_iff.mp hx f
