MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.countable_characterSpace_of_nonUnital_singleton

Raw UTF-8 source

theorem countable_characterSpace_of_nonUnital_singleton [Nontrivial A]
    [TopologicalSpace.SeparableSpace H]
    (pi : NonUnitalCStarRepresentation A H)
    (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
    (D : StarSubalgebra ℂ (Unitization ℂ A))
    [IsClosed (D : Set (Unitization ℂ A))] :
    Countable (WeakDual.characterSpace ℂ D)

1 import Mathlib.Topology.Bases
2 import Mathlib.Analysis.InnerProductSpace.Adjoint
3 import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.CharacterEigenvector
4 
5 /-!
6 # Countability of unitization characters represented by a non-unital algebra
7 
8 Characters other than the scalar character of the unitization give mutually
9 orthogonal unit vectors.  Separability therefore makes that complement
10 countable; adjoining the scalar character makes the full character space
11 countable as well.
12 -/
13 
14 set_option autoImplicit false
15 
16 open Function Metric Set
17 open scoped ComplexOrder InnerProduct
18 
19 namespace MathlibAnnex.Analysis.CStarAlgebra
20 
21 universe u v
22 
23 variable {A : Type u} [NonUnitalCStarAlgebra A]
24   [PartialOrder A] [StarOrderedRing A]
25 variable {H : Type v}
26 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
27 
28 namespace NonUnitalCStarRepresentation
29 
30 /-- The non-scalar characters of a closed unital star subalgebra of a
31 minimal unitization. -/
32 abbrev NonScalarCharacterSpace
33     (D : StarSubalgebra ℂ (Unitization ℂ A))
34     [IsClosed (D : Set (Unitization ℂ A))] :=
35   {chi : WeakDual.characterSpace ℂ D //
36     chi ≠ infinityCharacterOn (A := A) D}
37 
38 /-- The non-scalar characters of a closed star subalgebra of the unitization
39 are countable when they are represented in a separable singleton model. -/
40 theorem countable_nonScalarCharacterSpace_of_singleton [Nontrivial A]
41     [TopologicalSpace.SeparableSpace H]
42     (pi : NonUnitalCStarRepresentation A H)
43     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
44     (D : StarSubalgebra ℂ (Unitization ℂ A))
45     [IsClosed (D : Set (Unitization ℂ A))] :
46     Countable (NonScalarCharacterSpace (A := A) D) := by
47   choose eta heta_norm heta_eigen using
48     fun chi : NonScalarCharacterSpace (A := A) D =>
49       exists_unit_eigenvector_of_character_ne_infinity pi hsingle D chi.1 chi.2
50   have horth : Pairwise fun chi psi : NonScalarCharacterSpace (A := A) D =>
51       inner ℂ (eta chi) (eta psi) = 0 := by
52     intro chi psi hne
53     obtain ⟨d, hd⟩ : ∃ d : D, chi.1 d ≠ psi.1 d := by
54       by_contra hall
55       push Not at hall
56       apply hne
57       apply Subtype.ext
58       exact WeakDual.CharacterSpace.ext hall
59     have hadj : ContinuousLinearMap.adjoint (pi.unitization (d : Unitization ℂ A)) =
60         pi.unitization (star (d : Unitization ℂ A)) := by
61       rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star]
62     have heq := (pi.unitization (d : Unitization ℂ A)).adjoint_inner_right
63       (eta chi) (eta psi)
64     rw [hadj] at heq
65     change inner ℂ (eta chi)
66         (pi.unitization ((star d : D) : Unitization ℂ A) (eta psi)) =
67       inner ℂ (pi.unitization (d : Unitization ℂ A) (eta chi)) (eta psi) at heq
68     rw [heta_eigen psi (star d), heta_eigen chi d] at heq
69     simp only [inner_smul_left, inner_smul_right, map_star] at heq
70     by_contra hinner
71     have hstar : star (psi.1 d) = star (chi.1 d) :=
72       mul_right_cancel₀ hinner heq
73     exact hd (star_injective hstar).symm
74   have hdist (chi psi : NonScalarCharacterSpace (A := A) D) (hne : chi ≠ psi) :
75       1 ≤ dist (eta chi) (eta psi) := by
76     rw [dist_eq_norm]
77     have hsq := norm_sub_mul_self (𝕜 := ℂ) (eta chi) (eta psi)
78     rw [horth hne, map_zero, heta_norm chi, heta_norm psi] at hsq
79     norm_num at hsq
80     nlinarith [norm_nonneg (eta chi - eta psi)]
81   have hballs : Pairwise (Disjoint on
82       fun chi : NonScalarCharacterSpace (A := A) D =>
83         ball (eta chi) (1 / 3 : ℝ)) := by
84     intro chi psi hne
85     apply ball_disjoint_ball
86     have := hdist chi psi hne
87     norm_num at this ⊢
88     linarith
89   exact hballs.countable_of_isOpen_disjoint
90     (fun _ => isOpen_ball)
91     (fun chi => ⟨eta chi, mem_ball_self (by norm_num)⟩)
92 
93 /-- The whole character space is countable: it consists of the preceding
94 complement and the one scalar character. -/
95 theorem countable_characterSpace_of_nonUnital_singleton [Nontrivial A]
96     [TopologicalSpace.SeparableSpace H]
97     (pi : NonUnitalCStarRepresentation A H)
98     (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi)
99     (D : StarSubalgebra ℂ (Unitization ℂ A))
100     [IsClosed (D : Set (Unitization ℂ A))] :
101     Countable (WeakDual.characterSpace ℂ D) := by
102   let X := WeakDual.characterSpace ℂ D
103   let chiInf : X := infinityCharacterOn (A := A) D
104   let Y := {chi : X // chi ≠ chiInf}
105   have hY : Countable Y :=
106     countable_nonScalarCharacterSpace_of_singleton pi hsingle D
107   letI : Countable Y := hY
108   let f : Y ⊕ Unit → X := Sum.elim Subtype.val (fun _ => chiInf)
109   have hf : Surjective f := by
110     intro chi
111     by_cases hchi : chi = chiInf
112     · exact ⟨Sum.inr (), by simp [f, hchi]⟩
113     · exact ⟨Sum.inl ⟨chi, hchi⟩, rfl⟩
114   exact hf.countable
115 
116 end NonUnitalCStarRepresentation
117 
118 end MathlibAnnex.Analysis.CStarAlgebra