Exact source: MathlibAnnex/Analysis/CStarAlgebra/AtomicConstruction/GeneratedReduction.lean, lines 127–251.
Back to Every irreducible representation is unitarily equivalent to the inclusion
1import MathlibAnnex.Analysis.CStarAlgebra.Cyclic 2import MathlibAnnex.Analysis.CStarAlgebra.Generated 3import MathlibAnnex.Analysis.CStarAlgebra.Representation.GeneratedReduction 4import Mathlib.Analysis.CStarAlgebra.Spectrum 5import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.Concrete 6 7/-! 8# Reduction for the Nmk norm-closed generated concrete target 9 10A closed subspace which reduces every nominated generator reduces every 11element of the concrete norm-closed generated algebra. The proof uses the 12commutant of the orthogonal projection and density of the algebraic star 13algebra; no operator-topology closure is asserted. 14-/ 15 16set_option autoImplicit false 17 18noncomputable section 19 20open Topology 21open scoped CStarAlgebra InnerProduct 22 23namespace MathlibAnnex.CStarAlgebra.AtomicConstruction 24 25open MathlibAnnex.Analysis.CStarAlgebra 26 27universe u v w z 28 29variable {A : Type u} [CStarAlgebra A] 30variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 31 [CompleteSpace H] 32variable {J : Type w} 33variable {K : Type z} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 34 [CompleteSpace K] 35 36/-- Reduction by the represented source and every additional generator 37extends to the whole concrete target by norm-closed generation. -/ 38theorem reduces_concreteTarget_of_generators 39 (pi : Representation A H) (U : J → H →L[ℂ] H) 40 (rho : Representation (concreteTarget pi U) K) 41 (M : Submodule ℂ K) (hMclosed : IsClosed (M : Set K)) 42 (hsource : ∀ a : A, M.Reduces (rho (sourceHom pi U a))) 43 (hgenerator : ∀ j : J, M.Reduces (rho (generator pi U j))) : 44 ∀ x : concreteTarget pi U, M.Reduces (rho x) := by 45 letI : CompleteSpace M := hMclosed.completeSpace_coe 46 letI : M.HasOrthogonalProjection := inferInstance 47 let P : K →L[ℂ] K := M.starProjection 48 let C : StarSubalgebra ℂ (concreteTarget pi U) := 49 (StarSubalgebra.centralizer ℂ ({P} : Set (K →L[ℂ] K))).comap rho 50 have hCclosed : IsClosed (C : Set (concreteTarget pi U)) := by 51 change IsClosed (rho ⁻¹' 52 (StarSubalgebra.centralizer ℂ ({P} : Set (K →L[ℂ] K)) : 53 Set (K →L[ℂ] K))) 54 have hcentralizer : IsClosed 55 (StarSubalgebra.centralizer ℂ ({P} : Set (K →L[ℂ] K)) : 56 Set (K →L[ℂ] K)) := by 57 rw [StarSubalgebra.coe_centralizer] 58 exact Set.isClosed_centralizer _ 59 exact hcentralizer.preimage (map_continuous rho) 60 have memC_of_reduces {x : concreteTarget pi U} 61 (hx : M.Reduces (rho x)) : x ∈ C := by 62 change rho x ∈ StarSubalgebra.centralizer ℂ ({P} : Set (K →L[ℂ] K)) 63 rw [StarSubalgebra.mem_centralizer_iff] 64 intro g hg 65 rw [Set.mem_singleton_iff] at hg 66 subst g 67 have hcomm := (Submodule.reduces_iff_starProjection_commute).mp hx 68 constructor 69 · exact hcomm 70 · have hpstar : star P = P := by 71 change P† = P 72 exact M.starProjection_isSymmetric.clm_adjoint_eq 73 rw [hpstar] 74 exact hcomm 75 let S : Set (H →L[ℂ] H) := Set.range pi ∪ Set.range U 76 let B : StarSubalgebra ℂ (H →L[ℂ] H) := StarAlgebra.adjoin ℂ S 77 have hlift (x : H →L[ℂ] H) (hx : x ∈ B) : 78 (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : concreteTarget pi U) ∈ C := by 79 induction hx using StarAlgebra.adjoin_induction with 80 | mem x hx => 81 rcases hx with hx | hx 82 · rcases hx with ⟨a, rfl⟩ 83 exact memC_of_reduces (hsource a) 84 · rcases hx with ⟨j, rfl⟩ 85 exact memC_of_reduces (hgenerator j) 86 | algebraMap c => 87 change (algebraMap ℂ (concreteTarget pi U) c) ∈ C 88 exact C.algebraMap_mem c 89 | add x y hx hy hxc hyc => 90 change (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 91 concreteTarget pi U) + 92 ⟨y, StarSubalgebra.le_topologicalClosure B hy⟩ ∈ C 93 exact C.add_mem hxc hyc 94 | mul x y hx hy hxc hyc => 95 change (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 96 concreteTarget pi U) * 97 ⟨y, StarSubalgebra.le_topologicalClosure B hy⟩ ∈ C 98 exact C.mul_mem hxc hyc 99 | star x hx hxc => 100 change star (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 101 concreteTarget pi U) ∈ C 102 exact star_mem hxc 103 let inclusion : B →⋆ₐ[ℂ] concreteTarget pi U := 104 StarSubalgebra.inclusion (StarSubalgebra.le_topologicalClosure B) 105 have hinclusion (x : B) : inclusion x ∈ C := by 106 exact hlift x x.property 107 have hdense : DenseRange inclusion := by 108 change DenseRange 109 (Set.inclusion (StarSubalgebra.le_topologicalClosure B)) 110 apply (denseRange_inclusion_iff _).2 111 change closure (B : Set (H →L[ℂ] H)) ⊆ closure (B : Set (H →L[ℂ] H)) 112 exact le_rfl 113 intro x 114 have hxC : x ∈ C := by 115 have hrange : Set.range inclusion ⊆ (C : Set (concreteTarget pi U)) := by 116 rintro _ ⟨y, rfl⟩ 117 exact hinclusion y 118 apply closure_minimal hrange hCclosed 119 rw [hdense.closure_range] 120 exact Set.mem_univ x 121 apply Submodule.reduces_iff_starProjection_commute.mpr 122 change rho x ∈ StarSubalgebra.centralizer ℂ 123 ({P} : Set (K →L[ℂ] K)) at hxC 124 rw [StarSubalgebra.mem_centralizer_iff] at hxC 125 exact (hxC P (Set.mem_singleton P)).1 126 127/-- An isometric equivalence which intertwines the represented source and all 128nominated generators intertwines every element of the norm-closed concrete 129target. Closure is taken in operator norm; no strong-operator continuity is 130used. -/ 131theorem intertwines_concreteTarget_of_generators 132 (pi : Representation A H) (U : J → H →L[ℂ] H) 133 (e : H ≃ₗᵢ[ℂ] K) (rho : Representation (concreteTarget pi U) K) 134 (hsource : ∀ a : A, 135 (e : H →L[ℂ] K).comp (pi a) = 136 (rho (sourceHom pi U a)).comp (e : H →L[ℂ] K)) 137 (hgenerator : ∀ j : J, 138 (e : H →L[ℂ] K).comp (U j) = 139 (rho (generator pi U j)).comp (e : H →L[ℂ] K)) : 140 ∀ x : concreteTarget pi U, 141 (e : H →L[ℂ] K).comp (ambientInclusion pi U x) = 142 (rho x).comp (e : H →L[ℂ] K) := by 143 let S : Set (H →L[ℂ] H) := Set.range pi ∪ Set.range U 144 let B : StarSubalgebra ℂ (H →L[ℂ] H) := StarAlgebra.adjoin ℂ S 145 let good : Set (concreteTarget pi U) := {x | 146 (e : H →L[ℂ] K).comp (ambientInclusion pi U x) = 147 (rho x).comp (e : H →L[ℂ] K)} 148 have hgoodClosed : IsClosed good := by 149 apply isClosed_eq 150 · exact Continuous.const_clm_comp 151 (map_continuous (ambientInclusion pi U)) (e : H →L[ℂ] K) 152 · exact Continuous.clm_comp_const (map_continuous rho) (e : H →L[ℂ] K) 153 have hlift (x : H →L[ℂ] H) (hx : x ∈ B) : 154 (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : concreteTarget pi U) ∈ 155 good := by 156 induction hx using StarAlgebra.adjoin_induction with 157 | mem x hx => 158 rcases hx with hx | hx 159 · rcases hx with ⟨a, rfl⟩ 160 exact hsource a 161 · rcases hx with ⟨j, rfl⟩ 162 exact hgenerator j 163 | algebraMap c => 164 change (e : H →L[ℂ] K).comp 165 (algebraMap ℂ (H →L[ℂ] H) c) = 166 (rho (algebraMap ℂ (concreteTarget pi U) c)).comp 167 (e : H →L[ℂ] K) 168 apply ContinuousLinearMap.ext 169 intro z 170 rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply] 171 have hc : rho (algebraMap ℂ (concreteTarget pi U) c) = 172 algebraMap ℂ (K →L[ℂ] K) c := rho.toAlgHom.commutes c 173 rw [hc] 174 simpa using e.map_smul c z 175 | add x y hx hy hxc hyc => 176 change (e : H →L[ℂ] K).comp x = 177 (rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 178 concreteTarget pi U)).comp (e : H →L[ℂ] K) at hxc 179 change (e : H →L[ℂ] K).comp y = 180 (rho (⟨y, StarSubalgebra.le_topologicalClosure B hy⟩ : 181 concreteTarget pi U)).comp (e : H →L[ℂ] K) at hyc 182 change (e : H →L[ℂ] K).comp (x + y) = 183 (rho ((⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 184 concreteTarget pi U) + 185 ⟨y, StarSubalgebra.le_topologicalClosure B hy⟩)).comp 186 (e : H →L[ℂ] K) 187 rw [map_add, ContinuousLinearMap.comp_add, 188 ContinuousLinearMap.add_comp, hxc, hyc] 189 | mul x y hx hy hxc hyc => 190 change (e : H →L[ℂ] K).comp x = 191 (rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 192 concreteTarget pi U)).comp (e : H →L[ℂ] K) at hxc 193 change (e : H →L[ℂ] K).comp y = 194 (rho (⟨y, StarSubalgebra.le_topologicalClosure B hy⟩ : 195 concreteTarget pi U)).comp (e : H →L[ℂ] K) at hyc 196 change (e : H →L[ℂ] K).comp (x * y) = 197 (rho ((⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 198 concreteTarget pi U) * 199 ⟨y, StarSubalgebra.le_topologicalClosure B hy⟩)).comp 200 (e : H →L[ℂ] K) 201 rw [map_mul] 202 change (e : H →L[ℂ] K).comp (x.comp y) = 203 ((rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 204 concreteTarget pi U)).comp 205 (rho (⟨y, StarSubalgebra.le_topologicalClosure B hy⟩ : 206 concreteTarget pi U))).comp (e : H →L[ℂ] K) 207 calc 208 (e : H →L[ℂ] K).comp (x.comp y) = 209 ((e : H →L[ℂ] K).comp x).comp y := 210 (ContinuousLinearMap.comp_assoc _ _ _).symm 211 _ = ((rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 212 concreteTarget pi U)).comp (e : H →L[ℂ] K)).comp y := by 213 rw [hxc] 214 _ = (rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 215 concreteTarget pi U)).comp 216 ((e : H →L[ℂ] K).comp y) := 217 ContinuousLinearMap.comp_assoc _ _ _ 218 _ = (rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 219 concreteTarget pi U)).comp 220 ((rho (⟨y, StarSubalgebra.le_topologicalClosure B hy⟩ : 221 concreteTarget pi U)).comp (e : H →L[ℂ] K)) := by 222 rw [hyc] 223 _ = ((rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 224 concreteTarget pi U)).comp 225 (rho (⟨y, StarSubalgebra.le_topologicalClosure B hy⟩ : 226 concreteTarget pi U))).comp (e : H →L[ℂ] K) := 227 (ContinuousLinearMap.comp_assoc _ _ _).symm 228 | star x hx hxc => 229 change (e : H →L[ℂ] K).comp x = 230 (rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 231 concreteTarget pi U)).comp (e : H →L[ℂ] K) at hxc 232 change (e : H →L[ℂ] K).comp (star x) = 233 (rho (star (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : 234 concreteTarget pi U))).comp (e : H →L[ℂ] K) 235 rw [map_star, ContinuousLinearMap.star_eq_adjoint, 236 ContinuousLinearMap.star_eq_adjoint] 237 exact e.intertwines_adjoint hxc 238 let inclusion : B →⋆ₐ[ℂ] concreteTarget pi U := 239 StarSubalgebra.inclusion (StarSubalgebra.le_topologicalClosure B) 240 have hdense : DenseRange inclusion := by 241 change DenseRange (Set.inclusion (StarSubalgebra.le_topologicalClosure B)) 242 apply (denseRange_inclusion_iff _).2 243 change closure (B : Set (H →L[ℂ] H)) ⊆ closure (B : Set (H →L[ℂ] H)) 244 exact le_rfl 245 intro x 246 have hrange : Set.range inclusion ⊆ good := by 247 rintro _ ⟨y, rfl⟩ 248 exact hlift y y.property 249 apply closure_minimal hrange hgoodClosed 250 rw [hdense.closure_range] 251 exact Set.mem_univ x 252 253end MathlibAnnex.CStarAlgebra.AtomicConstruction