MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_scalar_corner
theorem exists_nonzero_projection_scalar_corner [Nontrivial A]
[TopologicalSpace.SeparableSpace H]
(pi : NonUnitalCStarRepresentation A H)
(hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
∃ p : A, IsStarProjection p ∧ p ≠ 0 ∧
∀ a : A, ∃ c : ℂ, p * a * p = c • p1 import Mathlib.Topology.Baire.LocallyCompactRegular 2 import MathlibAnnex.Topology.CountableBaire 3 import MathlibAnnex.Analysis.CStarAlgebra.IsolatedCharacter 4 import MathlibAnnex.Analysis.CStarAlgebra.MaximalAbelianContaining 5 import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.CharacterCountable 6 import MathlibAnnex.Analysis.CStarAlgebra.Representation.MinimalProjection 7 8 /-! 9 # A minimal projection in a non-unital singleton model 10 11 A maximal abelian subalgebra of the unitization is chosen to contain a 12 nonzero element of the original algebra. Its non-scalar character space is 13 a nonempty open countable Baire space, so it has an isolated point away from 14 the scalar character. The associated Gelfand projection consequently lies 15 in the original algebra. 16 -/ 17 18 set_option autoImplicit false 19 20 open Set 21 open scoped ComplexOrder IsMulCommutative 22 23 namespace MathlibAnnex.Analysis.CStarAlgebra 24 25 universe u v 26 27 variable {A : Type u} [NonUnitalCStarAlgebra A] 28 [PartialOrder A] [StarOrderedRing A] 29 variable {H : Type v} 30 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 31 32 namespace NonUnitalCStarRepresentation 33 34 /-- If a closed commutative subalgebra of a minimal unitization contains a 35 nonzero element with zero scalar coordinate, its countable character space 36 has an isolated character different from the scalar character. -/ 37 theorem exists_isolated_character_ne_infinity 38 (D : StarSubalgebra ℂ (Unitization ℂ A)) 39 [IsClosed (D : Set (Unitization ℂ A))] 40 [IsMulCommutative D] 41 [Countable (WeakDual.characterSpace ℂ D)] 42 (d : D) (hd : d ≠ 0) 43 (hdfst : (d : Unitization ℂ A).fst = 0) : 44 ∃ chi : WeakDual.characterSpace ℂ D, 45 chi ≠ infinityCharacterOn (A := A) D ∧ 46 IsOpen ({chi} : Set (WeakDual.characterSpace ℂ D)) := by 47 letI : CommCStarAlgebra D := {} 48 let X := WeakDual.characterSpace ℂ D 49 let chiInf : X := infinityCharacterOn (A := A) D 50 let U : Set X := {chiInf}ᶜ 51 have hUopen : IsOpen U := isClosed_singleton.isOpen_compl 52 have hchar : ∃ chi : X, chi d ≠ 0 := by 53 by_contra hex 54 have hall : ∀ chi : X, chi d = 0 := by 55 intro chi 56 by_contra hne 57 exact hex ⟨chi, hne⟩ 58 apply hd 59 apply (gelfandTransform_isometry D).injective 60 ext chi 61 simpa using hall chi 62 have hUne : U.Nonempty := by 63 obtain ⟨chi, hchi⟩ := hchar 64 refine ⟨chi, ?_⟩ 65 change chi ≠ chiInf 66 intro heq 67 apply hchi 68 rw [heq] 69 exact hdfst 70 letI : Nonempty U := hUne.to_subtype 71 letI : BaireSpace U := hUopen.baireSpace 72 obtain ⟨chi, hchiOpen⟩ := 73 MathlibAnnex.Topology.exists_isOpen_singleton (X := U) 74 refine ⟨chi.1, chi.2, ?_⟩ 75 simpa using hUopen.isOpenMap_subtype_val ({chi} : Set U) hchiOpen 76 77 /-- For the Gelfand projection attached to `chi`, every different character 78 vanishes on that projection. -/ 79 theorem character_apply_eq_zero_of_projection_mul_eq_smul 80 (D : StarSubalgebra ℂ (Unitization ℂ A)) 81 [IsClosed (D : Set (Unitization ℂ A))] 82 [IsMulCommutative D] 83 (chi psi : WeakDual.characterSpace ℂ D) 84 (hchi : chi ≠ psi) (p : D) (hp : IsStarProjection p) (hpne : p ≠ 0) 85 (hpd : ∀ d : D, p * d = chi d • p) : 86 psi p = 0 := by 87 have hchip : chi p = 1 := by 88 apply smul_left_injective ℂ hpne 89 calc 90 (chi p) • p = p * p := (hpd p).symm 91 _ = p := hp.isIdempotentElem.eq 92 _ = (1 : ℂ) • p := (one_smul ℂ p).symm 93 by_contra hpsine 94 apply hchi 95 apply WeakDual.CharacterSpace.ext 96 intro d 97 have heq := congrArg psi (hpd d) 98 have heq' : psi p * psi d = psi p * chi d := by 99 simpa [mul_comm (chi d) (psi p)] using heq 100 exact (mul_left_cancel₀ hpsine heq').symm 101 102 /-- A separable singleton irreducible model of a genuinely non-unital 103 C-star algebra forces a nonzero projection with scalar corner in that 104 algebra. -/ 105 theorem exists_nonzero_projection_scalar_corner [Nontrivial A] 106 [TopologicalSpace.SeparableSpace H] 107 (pi : NonUnitalCStarRepresentation A H) 108 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) : 109 ∃ p : A, IsStarProjection p ∧ p ≠ 0 ∧ 110 ∀ a : A, ∃ c : ℂ, p * a * p = c • p := by 111 obtain ⟨a, ha⟩ : ∃ a : A, a ≠ 0 := exists_ne 0 112 let b : A := star a * a 113 have hbne : b ≠ 0 := CStarRing.star_mul_self_ne_zero_iff a |>.2 ha 114 have hbself : IsSelfAdjoint b := IsSelfAdjoint.star_mul_self a 115 have hbinrself : IsSelfAdjoint (b : Unitization ℂ A) := hbself.inr ℂ 116 obtain ⟨D, hD, hbD⟩ := 117 exists_maximalAbelian_containing_isSelfAdjoint (b : Unitization ℂ A) hbinrself 118 letI : IsClosed (D : Set (Unitization ℂ A)) := hD.isClosed 119 letI : IsMulCommutative D := hD.1 120 letI : CommCStarAlgebra D := {} 121 let d : D := ⟨(b : Unitization ℂ A), hbD⟩ 122 have hdne : d ≠ 0 := by 123 intro hzero 124 apply hbne 125 apply Unitization.inr_injective (R := ℂ) 126 exact congrArg Subtype.val hzero 127 have hdfst : (d : Unitization ℂ A).fst = 0 := rfl 128 have hcount := countable_characterSpace_of_nonUnital_singleton pi hsingle D 129 letI : Countable (WeakDual.characterSpace ℂ D) := hcount 130 obtain ⟨chi, hchiInf, hchiOpen⟩ := 131 exists_isolated_character_ne_infinity D d hdne hdfst 132 obtain ⟨p, hp, hpne, hpd⟩ := 133 exists_projection_mul_eq_smul_of_isOpen_singleton chi hchiOpen 134 have hpInf : infinityCharacterOn (A := A) D p = 0 := 135 character_apply_eq_zero_of_projection_mul_eq_smul D chi 136 (infinityCharacterOn (A := A) D) hchiInf p hp hpne hpd 137 have hpfst : (p : Unitization ℂ A).fst = 0 := by 138 simpa using hpInf 139 let pA : A := (p : Unitization ℂ A).snd 140 have hp_eq : (p : Unitization ℂ A) = (pA : Unitization ℂ A) := by 141 ext <;> simp [pA, hpfst] 142 have hpA : IsStarProjection pA := by 143 apply IsStarProjection.of_inr (R := ℂ) 144 rw [← hp_eq] 145 exact hp.map D.subtype 146 have hpAne : pA ≠ 0 := by 147 intro hzero 148 apply hpne 149 apply Subtype.ext 150 rw [hp_eq, hzero] 151 rfl 152 have hcornerU := 153 corner_eq_smul_of_maximalAbelian D hD chi p hp hpd 154 refine ⟨pA, hpA, hpAne, ?_⟩ 155 intro x 156 obtain ⟨c, hc⟩ := hcornerU (x : Unitization ℂ A) 157 refine ⟨c, ?_⟩ 158 apply Unitization.inr_injective (R := ℂ) 159 simpa [← hp_eq] using hc 160 161 end NonUnitalCStarRepresentation 162 163 end MathlibAnnex.Analysis.CStarAlgebra