Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/AtomicCommutant.lean, lines 64–64.
Back to An irreducible operator algebra constructed from projection shells
1import MathlibAnnex.Analysis.CStarAlgebra.Intertwiner 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Atomic 3import MathlibAnnex.Analysis.InnerProductSpace.HilbertSumCoordinates 4 5/-! 6# The commutant of an atomic sum joined by inter-block links 7 8For an arbitrary dependent family of pairwise inequivalent irreducible 9representations, a commuting operator has scalar diagonal blocks and zero 10off-diagonal blocks. Operators linking a selected unit vector in every block 11to one root block force all diagonal scalars to agree. The proof uses the 12density of the arbitrary-index finite-support expansion `lp.hasSum_single`; 13there is no finite or countable index restriction. 14-/ 15 16set_option autoImplicit false 17 18open scoped ENNReal lp InnerProduct 19 20namespace MathlibAnnex.Analysis.CStarAlgebra 21 22universe u v w 23 24variable {A : Type u} [CStarAlgebra A] 25variable {I : Type v} {H : I → Type w} 26variable [DecidableEq I] 27variable [∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℂ (H i)] 28variable [∀ i, CompleteSpace (H i)] [∀ i, Nontrivial (H i)] 29 30open MathlibAnnex.Analysis.InnerProductSpace 31 32/-- The `(j,i)` block of an operator on a dependent Hilbert sum. -/ 33noncomputable def atomicBlock (T : HilbertSum H →L[ℂ] HilbertSum H) 34 (i j : I) : H i →L[ℂ] H j := 35 (coordinateProjection j).comp (T.comp (coordinateEmbedding i)) 36 37@[simp] 38theorem atomicBlock_apply (T : HilbertSum H →L[ℂ] HilbertSum H) 39 (i j : I) (x : H i) : 40 atomicBlock T i j x = T (coordinateEmbedding i x) j := 41 rfl 42 43/-- Every matrix block of an operator in the atomic commutant is an 44intertwiner between the corresponding fiber representations. -/ 45theorem intertwines_atomicBlock_of_inCommutant 46 (pi : ∀ i, Representation A (H i)) 47 (T : HilbertSum H →L[ℂ] HilbertSum H) 48 (hT : StarAlgHom.InCommutant (atomicRepresentation pi) T) 49 (i j : I) : 50 StarAlgHom.Intertwines (pi i) (pi j) (atomicBlock T i j) := by 51 intro a 52 apply ContinuousLinearMap.ext 53 intro x 54 have hcomm := congrArg 55 (fun R : HilbertSum H →L[ℂ] HilbertSum H ↦ R (coordinateEmbedding i x)) 56 (hT a).eq 57 have hcoord := congrArg (fun y : HilbertSum H ↦ y j) hcomm 58 simpa [atomicBlock, ContinuousLinearMap.comp_apply, 59 coordinateEmbedding_apply] using hcoord 60 61/-- The atomic source and one vector-link from every block to a root block 62have scalar commutant. Link unitarity is not needed for this implication; 63the source-derived model supplies it separately from rank-one completion. -/ 64theorem eq_algebraMap_of_atomic_of_links 65 (pi : ∀ i, Representation A (H i)) 66 (hirr : ∀ i, StarAlgHom.IsIrreducible (pi i)) 67 (hno : ∀ ⦃i j : I⦄, i ≠ j → ∀ U : H i ≃ₗᵢ[ℂ] H j, 68 ¬ StarAlgHom.Intertwines (pi i) (pi j) (U : H i →L[ℂ] H j)) 69 (o : I) (xi : ∀ i, H i) (hxi : ∀ i, ‖xi i‖ = 1) 70 (L : I → HilbertSum H →L[ℂ] HilbertSum H) 71 (hL : ∀ i, L i (coordinateEmbedding i (xi i)) = 72 coordinateEmbedding o (xi o)) 73 (T : HilbertSum H →L[ℂ] HilbertSum H) 74 (hTsource : StarAlgHom.InCommutant (atomicRepresentation pi) T) 75 (hTlink : ∀ i, Commute T (L i)) : 76 ∃ z : ℂ, T = algebraMap ℂ (HilbertSum H →L[ℂ] HilbertSum H) z := by 77 have hblocks (i : I) : ∃ z : ℂ, 78 atomicBlock T i i = algebraMap ℂ (H i →L[ℂ] H i) z := by 79 apply StarAlgHom.eq_algebraMap_of_irreducible (pi i) (hirr i) 80 intro a 81 exact intertwines_atomicBlock_of_inCommutant pi T hTsource i i a 82 choose z hz using hblocks 83 have hoff {i j : I} (hij : i ≠ j) : atomicBlock T i j = 0 := by 84 exact (intertwines_atomicBlock_of_inCommutant pi T hTsource i j).eq_zero_of_no_unitary 85 (hirr i) (hirr j) (hno hij) 86 have hsingle (i : I) (x : H i) : 87 T (coordinateEmbedding i x) = coordinateEmbedding i (z i • x) := by 88 apply lp.ext 89 funext j 90 by_cases hji : j = i 91 · subst j 92 have h := congrArg (fun R : H i →L[ℂ] H i ↦ R x) (hz i) 93 simpa [atomicBlock, ContinuousLinearMap.comp_apply, 94 ContinuousLinearMap.algebraMap_apply] using h 95 · have h := congrArg (fun R : H i →L[ℂ] H j ↦ R x) (hoff (Ne.symm hji)) 96 simpa [atomicBlock, ContinuousLinearMap.comp_apply, 97 coordinateEmbedding_apply, hji] using h 98 have hzi (i : I) : z i = z o := by 99 have hcomm := congrArg 100 (fun R : HilbertSum H →L[ℂ] HilbertSum H ↦ 101 R (coordinateEmbedding i (xi i))) (hTlink i).eq 102 change T (L i (coordinateEmbedding i (xi i))) = 103 L i (T (coordinateEmbedding i (xi i))) at hcomm 104 rw [hL, hsingle, hsingle, 105 map_smul (coordinateEmbedding o) (z o) (xi o), 106 map_smul (coordinateEmbedding i) (z i) (xi i), 107 map_smul (L i) (z i) (coordinateEmbedding i (xi i)), hL] at hcomm 108 have hcoord := congrArg (fun y : HilbertSum H ↦ y o) hcomm 109 have hxine : xi o ≠ 0 := norm_ne_zero_iff.mp (by rw [hxi]; exact one_ne_zero) 110 apply smul_left_injective ℂ hxine 111 simpa [coordinateEmbedding_apply] using hcoord.symm 112 refine ⟨z o, ?_⟩ 113 apply ContinuousLinearMap.ext 114 intro x 115 have hxsum : HasSum (fun i ↦ coordinateEmbedding i (x i)) x := by 116 simpa [coordinateEmbedding_apply] using 117 (lp.hasSum_single (p := (2 : ℝ≥0∞)) (by norm_num) x) 118 have hTsum : HasSum (fun i ↦ T (coordinateEmbedding i (x i))) (T x) := 119 hxsum.mapL T 120 have hzsum : HasSum (fun i ↦ z o • coordinateEmbedding i (x i)) (z o • x) := 121 hxsum.const_smul (z o) 122 have hterms : (fun i ↦ T (coordinateEmbedding i (x i))) = 123 (fun i ↦ z o • coordinateEmbedding i (x i)) := by 124 funext i 125 rw [hsingle, hzi] 126 exact map_smul (coordinateEmbedding i) (z o) (x i) 127 have hTsum' : HasSum (fun i ↦ z o • coordinateEmbedding i (x i)) (T x) := 128 hTsum.congr_fun fun i ↦ (congrFun hterms i).symm 129 have heq : T x = z o • x := hTsum'.unique hzsum 130 simpa [ContinuousLinearMap.algebraMap_apply] using heq 131 132/-- A unital star representation with scalar bounded commutant is 133topologically irreducible. -/ 134theorem StarAlgHom.isIrreducible_of_commutant_eq_algebraMap 135 {B K : Type*} [CStarAlgebra B] 136 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 137 [Nontrivial K] (rho : B →⋆ₐ[ℂ] (K →L[ℂ] K)) 138 (hscalar : ∀ T : K →L[ℂ] K, StarAlgHom.InCommutant rho T → 139 ∃ z : ℂ, T = algebraMap ℂ (K →L[ℂ] K) z) : 140 StarAlgHom.IsIrreducible rho := by 141 intro M hMclosed hMreduces 142 letI : IsClosed (M : Set K) := hMclosed 143 letI : CompleteSpace M := inferInstance 144 letI : M.HasOrthogonalProjection := inferInstance 145 let P : K →L[ℂ] K := M.starProjection 146 have hPcomm : StarAlgHom.InCommutant rho P := by 147 intro b 148 change P.comp (rho b) = (rho b).comp P 149 exact Submodule.Reduces.starProjection_commute (hMreduces b) 150 obtain ⟨z, hz⟩ := hscalar P hPcomm 151 by_cases hM : M = ⊥ 152 · exact Or.inl hM 153 right 154 obtain ⟨x, hxM, hxne⟩ := M.ne_bot_iff.mp hM 155 have hPx : P x = x := by 156 exact M.starProjection_eq_self_iff.mpr hxM 157 have hzapply : P x = z • x := by 158 simpa [ContinuousLinearMap.algebraMap_apply] using 159 congrArg (fun T : K →L[ℂ] K ↦ T x) hz 160 have hzx : z • x = (1 : ℂ) • x := by 161 rw [← hzapply, hPx, one_smul] 162 have hzone : z = 1 := smul_left_injective ℂ hxne hzx 163 rw [← M.range_starProjection, show M.starProjection = 1 by simpa [P, hz, hzone]] 164 exact LinearMap.range_eq_top.mpr fun y ↦ ⟨y, rfl⟩ 165 166end MathlibAnnex.Analysis.CStarAlgebra