MATHLIBANNEX / EXACT SOURCE v0.4.0
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.isCompactOperator_map_of_singleton
theorem isCompactOperator_map_of_singleton [Nontrivial A]
[TopologicalSpace.SeparableSpace H]
(pi : NonUnitalCStarRepresentation A H)
(hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :
∀ a : A, IsCompactOperator (pi a)1 import Mathlib.RingTheory.TwoSidedIdeal.Operations 2 import MathlibAnnex.Analysis.CStarAlgebra.ClosedIdealCharacter 3 import MathlibAnnex.Analysis.CStarAlgebra.CompactPreimage 4 import MathlibAnnex.Analysis.CStarAlgebra.MaximalAbelianContaining 5 import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.CompactRange 6 import MathlibAnnex.Analysis.InnerProductSpace.RankOne 7 8 /-! 9 # Excluding noncompact elements from a non-unital singleton model 10 11 If a represented self-adjoint element were noncompact, put it in a maximal 12 abelian subalgebra of the unitization. The compact-preimage ideal in that 13 subalgebra is closed. A character separating the element from this ideal is 14 non-scalar, hence is realized by a unit eigenvector. The corresponding 15 rank-one projection is already in the range of the original algebra. Its 16 operator commutes with the maximal abelian subalgebra, so faithfulness puts 17 the projection itself in that subalgebra. The separating character must 18 then take both values zero and one on it, a contradiction. 19 -/ 20 21 set_option autoImplicit false 22 23 open Set 24 open scoped ComplexOrder ComplexStarModule InnerProduct IsMulCommutative 25 26 namespace MathlibAnnex.Analysis.CStarAlgebra 27 28 universe u v 29 30 variable {A : Type u} [NonUnitalCStarAlgebra A] 31 [PartialOrder A] [StarOrderedRing A] 32 variable {H : Type v} 33 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 34 35 namespace NonUnitalCStarRepresentation 36 37 /-- If an operator-valued complex-linear map sends both real and imaginary 38 parts of an element to compact operators, it sends the element itself to a 39 compact operator. -/ 40 private theorem isCompactOperator_of_realPart_of_imaginaryPart 41 (pi : NonUnitalCStarRepresentation A H) (a : A) 42 (hre : IsCompactOperator (pi (ℜ a : A))) 43 (him : IsCompactOperator (pi (ℑ a : A))) : 44 IsCompactOperator (pi a) := by 45 have hsum : IsCompactOperator 46 (pi (ℜ a : A) + Complex.I • pi (ℑ a : A)) := 47 hre.add (him.smul Complex.I) 48 have hop : pi a = pi (ℜ a : A) + Complex.I • pi (ℑ a : A) := by 49 calc 50 pi a = pi ((ℜ a : A) + Complex.I • (ℑ a : A)) := by 51 rw [realPart_add_I_smul_imaginaryPart] 52 _ = pi (ℜ a : A) + Complex.I • pi (ℑ a : A) := by simp 53 rw [hop] 54 exact hsum 55 56 /-- A noncompact represented element has a self-adjoint part whose image is 57 still noncompact. -/ 58 private theorem exists_selfAdjoint_not_isCompactOperator 59 (pi : NonUnitalCStarRepresentation A H) {a : A} 60 (ha : ¬ IsCompactOperator (pi a)) : 61 ∃ b : A, IsSelfAdjoint b ∧ ¬ IsCompactOperator (pi b) := by 62 by_cases hre : IsCompactOperator (pi (ℜ a : A)) 63 · refine ⟨(ℑ a : A), (ℑ a).property, ?_⟩ 64 intro him 65 exact ha (isCompactOperator_of_realPart_of_imaginaryPart pi a hre him) 66 · exact ⟨(ℜ a : A), (ℜ a).property, hre⟩ 67 68 /-- In a genuinely non-unital separable singleton irreducible model every 69 represented operator is compact. No simplicity assumption is used. -/ 70 theorem isCompactOperator_map_of_singleton [Nontrivial A] 71 [TopologicalSpace.SeparableSpace H] 72 (pi : NonUnitalCStarRepresentation A H) 73 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) : 74 ∀ a : A, IsCompactOperator (pi a) := by 75 intro a 76 by_contra ha 77 obtain ⟨b, hbself, hbcompact⟩ := 78 exists_selfAdjoint_not_isCompactOperator pi ha 79 have hbinrself : IsSelfAdjoint (b : Unitization ℂ A) := hbself.inr ℂ 80 obtain ⟨D, hD, hbD⟩ := 81 exists_maximalAbelian_containing_isSelfAdjoint 82 (b : Unitization ℂ A) hbinrself 83 letI : IsClosed (D : Set (Unitization ℂ A)) := hD.isClosed 84 letI : IsMulCommutative D := hD.1 85 letI : CommCStarAlgebra D := {} 86 let rhoD : Representation D H := pi.unitization.comp D.subtype 87 let Jtwo : TwoSidedIdeal D := 88 MathlibAnnex.CStarAlgebra.compactPreimageIdeal 89 rhoD.toNonUnitalStarAlgHom 90 let J : Ideal D := Jtwo.asIdeal 91 have hJclosed : IsClosed (J : Set D) := by 92 change IsClosed (Jtwo : Set D) 93 exact MathlibAnnex.CStarAlgebra.isClosed_compactPreimageIdeal 94 rhoD.toNonUnitalStarAlgHom 95 let d : D := ⟨(b : Unitization ℂ A), hbD⟩ 96 have hdnot : d ∉ J := by 97 intro hd 98 have hdTwo : d ∈ Jtwo := hd 99 have hcompact : IsCompactOperator (rhoD d) := 100 (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal 101 rhoD.toNonUnitalStarAlgHom d).1 hdTwo 102 apply hbcompact 103 simpa [rhoD, d] using hcompact 104 obtain ⟨chi, hchiJ, hchid⟩ := 105 exists_character_annihilating_closedIdeal_of_not_mem J hJclosed hdnot 106 have hchiInf : chi ≠ infinityCharacterOn (A := A) D := by 107 intro heq 108 apply hchid 109 rw [heq] 110 simp [d] 111 obtain ⟨eta, heta, heigen⟩ := 112 exists_unit_eigenvector_of_character_ne_infinity 113 pi hsingle D chi hchiInf 114 obtain ⟨q, hq⟩ := 115 exists_preimage_rankOne_of_singleton pi hsingle eta eta 116 have hinj : Function.Injective pi := injective_of_singleton pi hsingle 117 have heta_ne : eta ≠ 0 := by 118 intro hzero 119 simp [hzero] at heta 120 have hcommute (x : D) : 121 (q : Unitization ℂ A) * (x : Unitization ℂ A) = 122 (x : Unitization ℂ A) * (q : Unitization ℂ A) := by 123 have hadj : ContinuousLinearMap.adjoint (rhoD x) eta = 124 star (chi x) • eta := by 125 have hadjmap : ContinuousLinearMap.adjoint (rhoD x) = rhoD (star x) := by 126 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star] 127 rw [hadjmap] 128 exact heigen (star x) |>.trans (by rw [map_star]) 129 have hoperator : 130 rhoD x * InnerProductSpace.rankOne ℂ eta eta = 131 InnerProductSpace.rankOne ℂ eta eta * rhoD x := 132 MathlibAnnex.Analysis.InnerProductSpace.commute_rankOne_self_of_apply_eq_smul_of_adjoint_apply_eq_star_smul 133 (rhoD x) eta (chi x) (heigen x) hadj 134 have hrhoD : rhoD x = 135 (x : Unitization ℂ A).fst • (1 : H →L[ℂ] H) + 136 pi (x : Unitization ℂ A).snd := by 137 change pi.unitization (x : Unitization ℂ A) = _ 138 induction (x : Unitization ℂ A) using Unitization.ind with 139 | inl_add_inr c y => simp [unitization, Algebra.algebraMap_eq_smul_one] 140 have hpiComm : 141 pi (x : Unitization ℂ A).snd * 142 InnerProductSpace.rankOne ℂ eta eta = 143 InnerProductSpace.rankOne ℂ eta eta * 144 pi (x : Unitization ℂ A).snd := by 145 apply add_left_cancel (a := 146 (x : Unitization ℂ A).fst • 147 InnerProductSpace.rankOne ℂ eta eta) 148 simpa [hrhoD, add_mul, mul_add, smul_mul_assoc, mul_smul_comm] using 149 hoperator 150 have hqCommA : q * (x : Unitization ℂ A).snd = 151 (x : Unitization ℂ A).snd * q := by 152 apply hinj 153 simpa [map_mul, hq] using hpiComm.symm 154 apply Unitization.ext 155 · simp 156 · simpa [hqCommA] 157 have hqDmem : (q : Unitization ℂ A) ∈ D := 158 hD.mem_of_commute hcommute 159 let r : D := ⟨(q : Unitization ℂ A), hqDmem⟩ 160 have hrJ : r ∈ J := by 161 have hcompactr : IsCompactOperator (rhoD r) := by 162 rw [show rhoD r = pi q by simp [rhoD, r], hq] 163 exact isCompactOperator_rankOne eta eta 164 have hrTwo : r ∈ Jtwo := 165 (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal 166 rhoD.toNonUnitalStarAlgHom r).2 hcompactr 167 exact hrTwo 168 have hchirZero : chi r = 0 := hchiJ r hrJ 169 have hmapr : rhoD r = InnerProductSpace.rankOne ℂ eta eta := by 170 simpa [rhoD, r] using hq 171 have hprojectionEta : 172 InnerProductSpace.rankOne ℂ eta eta eta = eta := by 173 simp [InnerProductSpace.rankOne_apply, 174 inner_self_eq_norm_sq_to_K, heta] 175 have hchirOne : chi r = 1 := by 176 apply smul_left_injective ℂ heta_ne 177 calc 178 chi r • eta = rhoD r eta := (heigen r).symm 179 _ = InnerProductSpace.rankOne ℂ eta eta eta := by rw [hmapr] 180 _ = eta := hprojectionEta 181 _ = (1 : ℂ) • eta := (one_smul ℂ eta).symm 182 exact one_ne_zero (hchirOne ▸ hchirZero) 183 184 end NonUnitalCStarRepresentation 185 186 end MathlibAnnex.Analysis.CStarAlgebra