Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/AtomicCommutant.lean
Pinned GitHub source · Raw UTF-8 source
Back to An irreducible operator algebra constructed from projection shells
1import MathlibAnnex.Analysis.CStarAlgebra.Intertwiner2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Atomic3import MathlibAnnex.Analysis.InnerProductSpace.HilbertSumCoordinates45/-!6# The commutant of an atomic sum joined by inter-block links78For an arbitrary dependent family of pairwise inequivalent irreducible9representations, a commuting operator has scalar diagonal blocks and zero10off-diagonal blocks. Operators linking a selected unit vector in every block11to one root block force all diagonal scalars to agree. The proof uses the12density of the arbitrary-index finite-support expansion `lp.hasSum_single`;13there is no finite or countable index restriction.14-/1516set_option autoImplicit false1718open scoped ENNReal lp InnerProduct1920namespace MathlibAnnex.Analysis.CStarAlgebra2122universe u v w2324variable {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)]2930open MathlibAnnex.Analysis.InnerProductSpace3132/-- 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))3637@[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 rfl4243/-- Every matrix block of an operator in the atomic commutant is an44intertwiner between the corresponding fiber representations. -/45theorem intertwines_atomicBlock_of_inCommutant46 (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) := by51 intro a52 apply ContinuousLinearMap.ext53 intro x54 have hcomm := congrArg55 (fun R : HilbertSum H →L[ℂ] HilbertSum H ↦ R (coordinateEmbedding i x))56 (hT a).eq57 have hcoord := congrArg (fun y : HilbertSum H ↦ y j) hcomm58 simpa [atomicBlock, ContinuousLinearMap.comp_apply,59 coordinateEmbedding_apply] using hcoord6061/-- The atomic source and one vector-link from every block to a root block62have 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_links65 (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 := by77 have hblocks (i : I) : ∃ z : ℂ,78 atomicBlock T i i = algebraMap ℂ (H i →L[ℂ] H i) z := by79 apply StarAlgHom.eq_algebraMap_of_irreducible (pi i) (hirr i)80 intro a81 exact intertwines_atomicBlock_of_inCommutant pi T hTsource i i a82 choose z hz using hblocks83 have hoff {i j : I} (hij : i ≠ j) : atomicBlock T i j = 0 := by84 exact (intertwines_atomicBlock_of_inCommutant pi T hTsource i j).eq_zero_of_no_unitary85 (hirr i) (hirr j) (hno hij)86 have hsingle (i : I) (x : H i) :87 T (coordinateEmbedding i x) = coordinateEmbedding i (z i • x) := by88 apply lp.ext89 funext j90 by_cases hji : j = i91 · subst j92 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 h95 · 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 h98 have hzi (i : I) : z i = z o := by99 have hcomm := congrArg100 (fun R : HilbertSum H →L[ℂ] HilbertSum H ↦101 R (coordinateEmbedding i (xi i))) (hTlink i).eq102 change T (L i (coordinateEmbedding i (xi i))) =103 L i (T (coordinateEmbedding i (xi i))) at hcomm104 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 hcomm108 have hcoord := congrArg (fun y : HilbertSum H ↦ y o) hcomm109 have hxine : xi o ≠ 0 := norm_ne_zero_iff.mp (by rw [hxi]; exact one_ne_zero)110 apply smul_left_injective ℂ hxine111 simpa [coordinateEmbedding_apply] using hcoord.symm112 refine ⟨z o, ?_⟩113 apply ContinuousLinearMap.ext114 intro x115 have hxsum : HasSum (fun i ↦ coordinateEmbedding i (x i)) x := by116 simpa [coordinateEmbedding_apply] using117 (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 T120 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)) := by124 funext i125 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).symm129 have heq : T x = z o • x := hTsum'.unique hzsum130 simpa [ContinuousLinearMap.algebraMap_apply] using heq131132/-- A unital star representation with scalar bounded commutant is133topologically irreducible. -/134theorem StarAlgHom.isIrreducible_of_commutant_eq_algebraMap135 {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 := by141 intro M hMclosed hMreduces142 letI : IsClosed (M : Set K) := hMclosed143 letI : CompleteSpace M := inferInstance144 letI : M.HasOrthogonalProjection := inferInstance145 let P : K →L[ℂ] K := M.starProjection146 have hPcomm : StarAlgHom.InCommutant rho P := by147 intro b148 change P.comp (rho b) = (rho b).comp P149 exact Submodule.Reduces.starProjection_commute (hMreduces b)150 obtain ⟨z, hz⟩ := hscalar P hPcomm151 by_cases hM : M = ⊥152 · exact Or.inl hM153 right154 obtain ⟨x, hxM, hxne⟩ := M.ne_bot_iff.mp hM155 have hPx : P x = x := by156 exact M.starProjection_eq_self_iff.mpr hxM157 have hzapply : P x = z • x := by158 simpa [ContinuousLinearMap.algebraMap_apply] using159 congrArg (fun T : K →L[ℂ] K ↦ T x) hz160 have hzx : z • x = (1 : ℂ) • x := by161 rw [← hzapply, hPx, one_smul]162 have hzone : z = 1 := smul_left_injective ℂ hxne hzx163 rw [← M.range_starProjection, show M.starProjection = 1 by simpa [P, hz, hzone]]164 exact LinearMap.range_eq_top.mpr fun y ↦ ⟨y, rfl⟩165166end MathlibAnnex.Analysis.CStarAlgebra