Exact source: MathlibAnnex/Analysis/CStarAlgebra/ClosedIdealCharacter.lean
Pinned GitHub source · Raw UTF-8 source
Back to Every operator in a singleton image is compact · Back to A character separating a closed ideal
1import Mathlib.Analysis.CStarAlgebra.GelfandDuality23/-!4# Characters separating closed ideals in commutative C-star algebras56Gelfand duality identifies a norm-closed ideal with the continuous7functions vanishing off its associated open set. Consequently every8element outside such an ideal is detected by a character annihilating the9ideal.10-/1112set_option autoImplicit false1314open Set1516namespace MathlibAnnex.Analysis.CStarAlgebra1718universe u1920/-- A character separates an element from a norm-closed ideal of a21commutative unital complex C-star algebra. -/22theorem exists_character_annihilating_closedIdeal_of_not_mem23 {D : Type u} [CommCStarAlgebra D]24 (J : Ideal D) (hJclosed : IsClosed (J : Set D))25 {d : D} (hd : d ∉ J) :26 ∃ chi : WeakDual.characterSpace ℂ D,27 (∀ x : D, x ∈ J → chi x = 0) ∧ chi d ≠ 0 := by28 let e := gelfandStarTransform D29 let K : Ideal C(WeakDual.characterSpace ℂ D, ℂ) :=30 J.map e.toRingEquiv.toRingHom31 have he : Isometry e := gelfandTransform_isometry D32 have hKcarrier : (K : Set C(WeakDual.characterSpace ℂ D, ℂ)) =33 e '' (J : Set D) := by34 ext f35 rw [Set.mem_image]36 simp only [K, SetLike.mem_coe]37 rw [Ideal.mem_map_iff_of_surjective e.toRingEquiv.toRingHom e.surjective]38 constructor39 · rintro ⟨x, hx, hxf⟩40 exact ⟨x, hx, hxf⟩41 · rintro ⟨x, hx, hxf⟩42 exact ⟨x, hx, hxf⟩43 have hKclosed : IsClosed (K : Set C(WeakDual.characterSpace ℂ D, ℂ)) := by44 rw [hKcarrier]45 exact he.isClosedEmbedding.isClosedMap (J : Set D) hJclosed46 have hed_not : e d ∉ K := by47 intro hed48 have hed' : e d ∈ (K : Set C(WeakDual.characterSpace ℂ D, ℂ)) := hed49 rw [hKcarrier] at hed'50 obtain ⟨x, hx, heq⟩ := hed'51 apply hd52 simpa [he.injective heq] using hx53 have hed_not_vanish :54 e d ∉ ContinuousMap.idealOfSet ℂ (ContinuousMap.setOfIdeal K) := by55 rwa [ContinuousMap.idealOfSet_ofIdeal_isClosed hKclosed]56 obtain ⟨chi, hchiOutside, hdchi⟩ :=57 ContinuousMap.notMem_idealOfSet.mp hed_not_vanish58 refine ⟨chi, ?_, ?_⟩59 · intro x hx60 have hexK : e x ∈ K := by61 have : e x ∈ (e '' (J : Set D)) := ⟨x, hx, rfl⟩62 rwa [← hKcarrier] at this63 have hvanish := ContinuousMap.notMem_setOfIdeal.mp hchiOutside hexK64 exact hvanish65 · exact hdchi6667end MathlibAnnex.Analysis.CStarAlgebra