Exact source: MathlibAnnex/Analysis/CStarAlgebra/NonUnital/CharacterCountable.lean
Pinned GitHub source · Raw UTF-8 source
Back to The full character space is countable · Back to A nonzero projection with scalar corner
1import Mathlib.Topology.Bases2import Mathlib.Analysis.InnerProductSpace.Adjoint3import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.CharacterEigenvector45/-!6# Countability of unitization characters represented by a non-unital algebra78Characters other than the scalar character of the unitization give mutually9orthogonal unit vectors. Separability therefore makes that complement10countable; adjoining the scalar character makes the full character space11countable as well.12-/1314set_option autoImplicit false1516open Function Metric Set17open scoped ComplexOrder InnerProduct1819namespace MathlibAnnex.Analysis.CStarAlgebra2021universe u v2223variable {A : Type u} [NonUnitalCStarAlgebra A]24 [PartialOrder A] [StarOrderedRing A]25variable {H : Type v}26variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2728namespace NonUnitalCStarRepresentation2930/-- The non-scalar characters of a closed unital star subalgebra of a31minimal unitization. -/32abbrev NonScalarCharacterSpace33 (D : StarSubalgebra ℂ (Unitization ℂ A))34 [IsClosed (D : Set (Unitization ℂ A))] :=35 {chi : WeakDual.characterSpace ℂ D //36 chi ≠ infinityCharacterOn (A := A) D}3738/-- The non-scalar characters of a closed star subalgebra of the unitization39are countable when they are represented in a separable singleton model. -/40theorem 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) := by47 choose eta heta_norm heta_eigen using48 fun chi : NonScalarCharacterSpace (A := A) D =>49 exists_unit_eigenvector_of_character_ne_infinity pi hsingle D chi.1 chi.250 have horth : Pairwise fun chi psi : NonScalarCharacterSpace (A := A) D =>51 inner ℂ (eta chi) (eta psi) = 0 := by52 intro chi psi hne53 obtain ⟨d, hd⟩ : ∃ d : D, chi.1 d ≠ psi.1 d := by54 by_contra hall55 push Not at hall56 apply hne57 apply Subtype.ext58 exact WeakDual.CharacterSpace.ext hall59 have hadj : ContinuousLinearMap.adjoint (pi.unitization (d : Unitization ℂ A)) =60 pi.unitization (star (d : Unitization ℂ A)) := by61 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star]62 have heq := (pi.unitization (d : Unitization ℂ A)).adjoint_inner_right63 (eta chi) (eta psi)64 rw [hadj] at heq65 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 heq68 rw [heta_eigen psi (star d), heta_eigen chi d] at heq69 simp only [inner_smul_left, inner_smul_right, map_star] at heq70 by_contra hinner71 have hstar : star (psi.1 d) = star (chi.1 d) :=72 mul_right_cancel₀ hinner heq73 exact hd (star_injective hstar).symm74 have hdist (chi psi : NonScalarCharacterSpace (A := A) D) (hne : chi ≠ psi) :75 1 ≤ dist (eta chi) (eta psi) := by76 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 hsq79 norm_num at hsq80 nlinarith [norm_nonneg (eta chi - eta psi)]81 have hballs : Pairwise (Disjoint on82 fun chi : NonScalarCharacterSpace (A := A) D =>83 ball (eta chi) (1 / 3 : ℝ)) := by84 intro chi psi hne85 apply ball_disjoint_ball86 have := hdist chi psi hne87 norm_num at this ⊢88 linarith89 exact hballs.countable_of_isOpen_disjoint90 (fun _ => isOpen_ball)91 (fun chi => ⟨eta chi, mem_ball_self (by norm_num)⟩)9293/-- The whole character space is countable: it consists of the preceding94complement and the one scalar character. -/95theorem 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) := by102 let X := WeakDual.characterSpace ℂ D103 let chiInf : X := infinityCharacterOn (A := A) D104 let Y := {chi : X // chi ≠ chiInf}105 have hY : Countable Y :=106 countable_nonScalarCharacterSpace_of_singleton pi hsingle D107 letI : Countable Y := hY108 let f : Y ⊕ Unit → X := Sum.elim Subtype.val (fun _ => chiInf)109 have hf : Surjective f := by110 intro chi111 by_cases hchi : chi = chiInf112 · exact ⟨Sum.inr (), by simp [f, hchi]⟩113 · exact ⟨Sum.inl ⟨chi, hchi⟩, rfl⟩114 exact hf.countable115116end NonUnitalCStarRepresentation117118end MathlibAnnex.Analysis.CStarAlgebra