MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.exists_character_annihilating_closedIdeal_of_not_mem

Raw UTF-8 source

theorem exists_character_annihilating_closedIdeal_of_not_mem
    {D : Type u} [CommCStarAlgebra D]
    (J : Ideal D) (hJclosed : IsClosed (J : Set D))
    {d : D} (hd : d ∉ J) :
    ∃ chi : WeakDual.characterSpace ℂ D,
      (∀ x : D, x ∈ J → chi x = 0) ∧ chi d ≠ 0

1 import Mathlib.Analysis.CStarAlgebra.GelfandDuality
2 
3 /-!
4 # Characters separating closed ideals in commutative C-star algebras
5 
6 Gelfand duality identifies a norm-closed ideal with the continuous
7 functions vanishing off its associated open set.  Consequently every
8 element outside such an ideal is detected by a character annihilating the
9 ideal.
10 -/
11 
12 set_option autoImplicit false
13 
14 open Set
15 
16 namespace MathlibAnnex.Analysis.CStarAlgebra
17 
18 universe u
19 
20 /-- A character separates an element from a norm-closed ideal of a
21 commutative unital complex C-star algebra. -/
22 theorem exists_character_annihilating_closedIdeal_of_not_mem
23     {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 := by
28   let e := gelfandStarTransform D
29   let K : Ideal C(WeakDual.characterSpace ℂ D, ℂ) :=
30     J.map e.toRingEquiv.toRingHom
31   have he : Isometry e := gelfandTransform_isometry D
32   have hKcarrier : (K : Set C(WeakDual.characterSpace ℂ D, ℂ)) =
33       e '' (J : Set D) := by
34     ext f
35     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     constructor
39     · 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, ℂ)) := by
44     rw [hKcarrier]
45     exact he.isClosedEmbedding.isClosedMap (J : Set D) hJclosed
46   have hed_not : e d ∉ K := by
47     intro hed
48     have hed' : e d ∈ (K : Set C(WeakDual.characterSpace ℂ D, ℂ)) := hed
49     rw [hKcarrier] at hed'
50     obtain ⟨x, hx, heq⟩ := hed'
51     apply hd
52     simpa [he.injective heq] using hx
53   have hed_not_vanish :
54       e d ∉ ContinuousMap.idealOfSet ℂ (ContinuousMap.setOfIdeal K) := by
55     rwa [ContinuousMap.idealOfSet_ofIdeal_isClosed hKclosed]
56   obtain ⟨chi, hchiOutside, hdchi⟩ :=
57     ContinuousMap.notMem_idealOfSet.mp hed_not_vanish
58   refine ⟨chi, ?_, ?_⟩
59   · intro x hx
60     have hexK : e x ∈ K := by
61       have : e x ∈ (e '' (J : Set D)) := ⟨x, hx, rfl⟩
62       rwa [← hKcarrier] at this
63     have hvanish := ContinuousMap.notMem_setOfIdeal.mp hchiOutside hexK
64     exact hvanish
65   · exact hdchi
66 
67 end MathlibAnnex.Analysis.CStarAlgebra