Exact source: MathlibAnnex/Analysis/CStarAlgebra/AtomicConstruction/GeneratedReduction.lean
Pinned GitHub source · Raw UTF-8 source
Back to An irreducible target representation has a surviving fixed space · Back to The cyclic sum fills every irreducible target representation
1import MathlibAnnex.Analysis.CStarAlgebra.Cyclic2import MathlibAnnex.Analysis.CStarAlgebra.Generated3import MathlibAnnex.Analysis.CStarAlgebra.Representation.GeneratedReduction4import Mathlib.Analysis.CStarAlgebra.Spectrum5import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.Concrete67/-!8# Reduction for the Nmk norm-closed generated concrete target910A closed subspace which reduces every nominated generator reduces every11element of the concrete norm-closed generated algebra. The proof uses the12commutant of the orthogonal projection and density of the algebraic star13algebra; no operator-topology closure is asserted.14-/1516set_option autoImplicit false1718noncomputable section1920open Topology21open scoped CStarAlgebra InnerProduct2223namespace MathlibAnnex.CStarAlgebra.AtomicConstruction2425open MathlibAnnex.Analysis.CStarAlgebra2627universe u v w z2829variable {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]3536/-- Reduction by the represented source and every additional generator37extends to the whole concrete target by norm-closed generation. -/38theorem reduces_concreteTarget_of_generators39 (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) := by45 letI : CompleteSpace M := hMclosed.completeSpace_coe46 letI : M.HasOrthogonalProjection := inferInstance47 let P : K →L[ℂ] K := M.starProjection48 let C : StarSubalgebra ℂ (concreteTarget pi U) :=49 (StarSubalgebra.centralizer ℂ ({P} : Set (K →L[ℂ] K))).comap rho50 have hCclosed : IsClosed (C : Set (concreteTarget pi U)) := by51 change IsClosed (rho ⁻¹'52 (StarSubalgebra.centralizer ℂ ({P} : Set (K →L[ℂ] K)) :53 Set (K →L[ℂ] K)))54 have hcentralizer : IsClosed55 (StarSubalgebra.centralizer ℂ ({P} : Set (K →L[ℂ] K)) :56 Set (K →L[ℂ] K)) := by57 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 := by62 change rho x ∈ StarSubalgebra.centralizer ℂ ({P} : Set (K →L[ℂ] K))63 rw [StarSubalgebra.mem_centralizer_iff]64 intro g hg65 rw [Set.mem_singleton_iff] at hg66 subst g67 have hcomm := (Submodule.reduces_iff_starProjection_commute).mp hx68 constructor69 · exact hcomm70 · have hpstar : star P = P := by71 change P† = P72 exact M.starProjection_isSymmetric.clm_adjoint_eq73 rw [hpstar]74 exact hcomm75 let S : Set (H →L[ℂ] H) := Set.range pi ∪ Set.range U76 let B : StarSubalgebra ℂ (H →L[ℂ] H) := StarAlgebra.adjoin ℂ S77 have hlift (x : H →L[ℂ] H) (hx : x ∈ B) :78 (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ : concreteTarget pi U) ∈ C := by79 induction hx using StarAlgebra.adjoin_induction with80 | mem x hx =>81 rcases hx with hx | hx82 · 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) ∈ C88 exact C.algebraMap_mem c89 | 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⟩ ∈ C93 exact C.add_mem hxc hyc94 | 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⟩ ∈ C98 exact C.mul_mem hxc hyc99 | star x hx hxc =>100 change star (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ :101 concreteTarget pi U) ∈ C102 exact star_mem hxc103 let inclusion : B →⋆ₐ[ℂ] concreteTarget pi U :=104 StarSubalgebra.inclusion (StarSubalgebra.le_topologicalClosure B)105 have hinclusion (x : B) : inclusion x ∈ C := by106 exact hlift x x.property107 have hdense : DenseRange inclusion := by108 change DenseRange109 (Set.inclusion (StarSubalgebra.le_topologicalClosure B))110 apply (denseRange_inclusion_iff _).2111 change closure (B : Set (H →L[ℂ] H)) ⊆ closure (B : Set (H →L[ℂ] H))112 exact le_rfl113 intro x114 have hxC : x ∈ C := by115 have hrange : Set.range inclusion ⊆ (C : Set (concreteTarget pi U)) := by116 rintro _ ⟨y, rfl⟩117 exact hinclusion y118 apply closure_minimal hrange hCclosed119 rw [hdense.closure_range]120 exact Set.mem_univ x121 apply Submodule.reduces_iff_starProjection_commute.mpr122 change rho x ∈ StarSubalgebra.centralizer ℂ123 ({P} : Set (K →L[ℂ] K)) at hxC124 rw [StarSubalgebra.mem_centralizer_iff] at hxC125 exact (hxC P (Set.mem_singleton P)).1126127/-- An isometric equivalence which intertwines the represented source and all128nominated generators intertwines every element of the norm-closed concrete129target. Closure is taken in operator norm; no strong-operator continuity is130used. -/131theorem intertwines_concreteTarget_of_generators132 (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) := by143 let S : Set (H →L[ℂ] H) := Set.range pi ∪ Set.range U144 let B : StarSubalgebra ℂ (H →L[ℂ] H) := StarAlgebra.adjoin ℂ S145 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 := by149 apply isClosed_eq150 · exact Continuous.const_clm_comp151 (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 := by156 induction hx using StarAlgebra.adjoin_induction with157 | mem x hx =>158 rcases hx with hx | hx159 · rcases hx with ⟨a, rfl⟩160 exact hsource a161 · rcases hx with ⟨j, rfl⟩162 exact hgenerator j163 | algebraMap c =>164 change (e : H →L[ℂ] K).comp165 (algebraMap ℂ (H →L[ℂ] H) c) =166 (rho (algebraMap ℂ (concreteTarget pi U) c)).comp167 (e : H →L[ℂ] K)168 apply ContinuousLinearMap.ext169 intro z170 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 c173 rw [hc]174 simpa using e.map_smul c z175 | 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 hxc179 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 hyc182 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⟩)).comp186 (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 hxc193 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 hyc196 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⟩)).comp200 (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)).comp205 (rho (⟨y, StarSubalgebra.le_topologicalClosure B hy⟩ :206 concreteTarget pi U))).comp (e : H →L[ℂ] K)207 calc208 (e : H →L[ℂ] K).comp (x.comp y) =209 ((e : H →L[ℂ] K).comp x).comp y :=210 (ContinuousLinearMap.comp_assoc _ _ _).symm211 _ = ((rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ :212 concreteTarget pi U)).comp (e : H →L[ℂ] K)).comp y := by213 rw [hxc]214 _ = (rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ :215 concreteTarget pi U)).comp216 ((e : H →L[ℂ] K).comp y) :=217 ContinuousLinearMap.comp_assoc _ _ _218 _ = (rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ :219 concreteTarget pi U)).comp220 ((rho (⟨y, StarSubalgebra.le_topologicalClosure B hy⟩ :221 concreteTarget pi U)).comp (e : H →L[ℂ] K)) := by222 rw [hyc]223 _ = ((rho (⟨x, StarSubalgebra.le_topologicalClosure B hx⟩ :224 concreteTarget pi U)).comp225 (rho (⟨y, StarSubalgebra.le_topologicalClosure B hy⟩ :226 concreteTarget pi U))).comp (e : H →L[ℂ] K) :=227 (ContinuousLinearMap.comp_assoc _ _ _).symm228 | 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 hxc232 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 hxc238 let inclusion : B →⋆ₐ[ℂ] concreteTarget pi U :=239 StarSubalgebra.inclusion (StarSubalgebra.le_topologicalClosure B)240 have hdense : DenseRange inclusion := by241 change DenseRange (Set.inclusion (StarSubalgebra.le_topologicalClosure B))242 apply (denseRange_inclusion_iff _).2243 change closure (B : Set (H →L[ℂ] H)) ⊆ closure (B : Set (H →L[ℂ] H))244 exact le_rfl245 intro x246 have hrange : Set.range inclusion ⊆ good := by247 rintro _ ⟨y, rfl⟩248 exact hlift y y.property249 apply closure_minimal hrange hgoodClosed250 rw [hdense.closure_range]251 exact Set.mem_univ x252253end MathlibAnnex.CStarAlgebra.AtomicConstruction