Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/CommonFixedSubspace.lean, lines 112–134.
Back to The matching GNS fiber retains exactly its cyclic line
1import MathlibAnnex.Analysis.CStarAlgebra.Compression 2import MathlibAnnex.Analysis.CStarAlgebra.CyclicTransport 3import MathlibAnnex.Analysis.CStarAlgebra.Representation.Adapters 4import MathlibAnnex.Analysis.CStarAlgebra.Representation.Atomic 5import MathlibAnnex.Analysis.CStarAlgebra.Representation.VectorFunctional 6import MathlibAnnex.Analysis.CStarAlgebra.Intertwiner 7import MathlibAnnex.Analysis.InnerProductSpace.HilbertSumCoordinates 8import MathlibAnnex.Analysis.InnerProductSpace.RankOne 9import Mathlib.Analysis.Normed.Module.Normalize 10 11/-! 12# Fixed spaces of represented projection flags 13 14Compression identifies the common fixed projection in its cyclic fiber and 15excludes it in inequivalent irreducible fibers. A coordinate argument then 16identifies the common fixed space of an arbitrary dependent atomic sum. 17-/ 18 19set_option autoImplicit false 20 21open Filter Topology 22open scoped ENNReal lp InnerProduct 23 24namespace MathlibAnnex.Analysis.CStarAlgebra 25 26open MathlibAnnex.Analysis.InnerProductSpace 27 28universe u v w 29 30variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 31 32/-- For represented star projections, being fixed is equivalent to belonging 33to the operator range, so the common fixed subspace is the infimum of the 34ranges. -/ 35theorem commonFixedSubspace_eq_iInf_range 36 {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 37 [CompleteSpace H] 38 (pi : Representation A H) (q : ℕ → A) (hq : ∀ n, IsStarProjection (q n)) : 39 commonFixedSubspace (fun n ↦ pi (q n)) = ⨅ n, (pi (q n)).range := by 40 ext x 41 rw [mem_commonFixedSubspace_iff, Submodule.mem_iInf] 42 apply forall_congr' 43 intro n 44 exact (LinearMap.IsIdempotentElem.mem_range_iff 45 (ContinuousLinearMap.IsIdempotentElem.toLinearMap 46 ((hq n).map pi).isIdempotentElem)).symm 47 48/-- A supplied star projection with the represented common-fixed range is 49the canonical common fixed projection. -/ 50theorem starProjection_eq_commonFixedProjection_of_range_iInf 51 {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 52 [CompleteSpace H] 53 (pi : Representation A H) (q : ℕ → A) (hq : ∀ n, IsStarProjection (q n)) 54 (P : H →L[ℂ] H) (hP : IsStarProjection P) 55 (hPrange : P.range = ⨅ n, (pi (q n)).range) : 56 P = commonFixedProjection (fun n ↦ pi (q n)) := by 57 obtain ⟨hProjection, hPeq⟩ := 58 isStarProjection_iff_eq_starProjection_range.mp hP 59 have hrange : P.range = commonFixedSubspace (fun n ↦ pi (q n)) := 60 hPrange.trans (commonFixedSubspace_eq_iInf_range pi q hq).symm 61 simpa only [commonFixedProjection, hrange] using hPeq 62 63/-- A projection has to fix a unit vector when its vector state takes value 64one on that projection. -/ 65theorem projection_apply_eq_self_of_vectorFunctional_eq_one 66 {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 67 [CompleteSpace H] 68 (pi : Representation A H) (p : A) (hp : IsStarProjection p) 69 (xi : H) (hxi : ‖xi‖ = 1) 70 (hvalue : Representation.vectorFunctional pi xi p = 1) : 71 pi p xi = xi := by 72 have hcomp : IsStarProjection (1 - p) := hp.one_sub 73 have hfunctional : 74 Representation.vectorFunctional pi xi (star (1 - p) * (1 - p)) = 0 := by 75 rw [hcomp.isSelfAdjoint.star_eq, hcomp.isIdempotentElem.eq, map_sub, 76 Representation.vectorFunctional_one pi hxi, hvalue, sub_self] 77 have hinner : inner ℂ (pi (1 - p) xi) (pi (1 - p) xi) = 0 := by 78 rw [← Representation.vectorFunctional_star_mul] 79 exact hfunctional 80 have hzero : pi (1 - p) xi = 0 := inner_self_eq_zero.mp hinner 81 have hsub : xi - pi p xi = 0 := by 82 simpa [map_sub, map_one] using hzero 83 exact (sub_eq_zero.mp hsub).symm 84 85/-- A unit vector fixed by every member of a compressing self-adjoint flag 86has exactly the limiting compression functional as its vector state. -/ 87theorem vectorFunctional_eq_of_compression_tendsto 88 {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 89 [CompleteSpace H] 90 (pi : Representation A H) (q : ℕ → A) (phi : A →L[ℂ] ℂ) 91 (hq_star : ∀ n, star (q n) = q n) 92 (hcompression : ∀ b : A, 93 Tendsto (fun n ↦ q n * b * q n - phi b • q n) atTop (nhds 0)) 94 (eta : H) (heta : ‖eta‖ = 1) 95 (hfixed : ∀ n, pi (q n) eta = eta) : 96 Representation.vectorFunctional pi eta = phi := by 97 apply ContinuousLinearMap.ext 98 intro b 99 have hcoeff := inner_map_eq_of_compression_tendsto pi 100 (Representation.continuousLinearMap pi).continuous q phi b eta eta 101 hq_star hfixed hfixed (hcompression b) 102 have hself : inner ℂ eta eta = 1 := by 103 rw [inner_self_eq_norm_sq_to_K, heta] 104 norm_num 105 change inner ℂ eta (pi b eta) = phi b 106 calc 107 inner ℂ eta (pi b eta) = phi b * inner ℂ eta eta := hcoeff 108 _ = phi b := by rw [hself, mul_one] 109 110/-- In a cyclic realization of the compression state, the represented common 111fixed projection is exactly the projection onto the cyclic vector. -/ 112theorem commonFixedProjection_eq_rankOne_of_dense_orbit 113 {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] 114 [CompleteSpace H] 115 (pi : Representation A H) (q : ℕ → A) (phi : A →L[ℂ] ℂ) (xi : H) 116 (hq_star : ∀ n, star (q n) = q n) 117 (hcompression : ∀ b : A, 118 Tendsto (fun n ↦ q n * b * q n - phi b • q n) atTop (nhds 0)) 119 (hfixed : ∀ n, pi (q n) xi = xi) 120 (hphi : ∀ b : A, phi b = inner ℂ xi (pi b xi)) 121 (hdense : DenseRange (StarAlgHom.orbitMap pi xi)) : 122 commonFixedProjection (fun n ↦ pi (q n)) = 123 InnerProductSpace.rankOne ℂ xi xi := by 124 let Q : ℕ → H →L[ℂ] H := fun n ↦ pi (q n) 125 let P := commonFixedProjection Q 126 apply projection_eq_rankOne_of_dense_orbit pi phi P xi 127 · exact (commonFixedProjection_eq_self_iff Q xi).2 128 ((mem_commonFixedSubspace_iff Q xi).2 hfixed) 129 · intro b 130 exact commonFixedProjection_comp_map_comp_eq pi 131 (Representation.continuousLinearMap pi).continuous q phi b hq_star 132 (hcompression b) 133 · exact hphi 134 · exact hdense 135 136/-- In an inequivalent irreducible realization, the common fixed projection 137of a flag with a pure cyclic compression state must vanish. -/ 138theorem commonFixedProjection_eq_zero_of_no_unitary 139 {H : Type v} {K : Type w} 140 [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 141 [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 142 [Nontrivial K] 143 (pi : Representation A H) (rho : Representation A K) 144 (q : ℕ → A) (phi : A →L[ℂ] ℂ) (xi : H) 145 (hq_star : ∀ n, star (q n) = q n) 146 (hcompression : ∀ b : A, 147 Tendsto (fun n ↦ q n * b * q n - phi b • q n) atTop (nhds 0)) 148 (hxiState : ∀ b : A, inner ℂ xi (pi b xi) = phi b) 149 (hxiCyclic : DenseRange (StarAlgHom.orbitMap pi xi)) 150 (hrho : StarAlgHom.IsIrreducible rho) 151 (hno : ∀ U : H ≃ₗᵢ[ℂ] K, 152 ¬ StarAlgHom.Intertwines pi rho (U : H →L[ℂ] K)) : 153 commonFixedProjection (fun n ↦ rho (q n)) = 0 := by 154 let Q : ℕ → K →L[ℂ] K := fun n ↦ rho (q n) 155 let P := commonFixedProjection Q 156 by_contra hP 157 have hex : ∃ z : K, P z ≠ 0 := by 158 by_contra h 159 push_neg at h 160 apply hP 161 ext z 162 exact h z 163 obtain ⟨z, hz⟩ := hex 164 let r : ℝ := ‖P z‖ 165 have hr : r ≠ 0 := norm_ne_zero_iff.mpr hz 166 let eta : K := ((r⁻¹ : ℝ) : ℂ) • P z 167 have heta_norm : ‖eta‖ = 1 := by 168 dsimp only [eta] 169 rw [norm_smul, Complex.norm_real, Real.norm_eq_abs, 170 abs_of_nonneg (inv_nonneg.mpr (norm_nonneg _)), inv_mul_cancel₀ hr] 171 have heta_ne : eta ≠ 0 := norm_ne_zero_iff.mp (by rw [heta_norm]; exact one_ne_zero) 172 have heta_fixed (n : ℕ) : rho (q n) eta = eta := by 173 dsimp only [eta] 174 rw [map_smul] 175 exact congrArg (fun y : K ↦ ((r⁻¹ : ℝ) : ℂ) • y) 176 (commonFixedProjection_apply_fixed Q n z) 177 have heta_state (b : A) : inner ℂ eta (rho b eta) = phi b := by 178 have h := inner_map_eq_of_compression_tendsto rho 179 (Representation.continuousLinearMap rho).continuous q phi b eta eta 180 hq_star heta_fixed heta_fixed (hcompression b) 181 have hself : inner ℂ eta eta = 1 := by 182 rw [inner_self_eq_norm_sq_to_K, heta_norm] 183 norm_num 184 calc 185 inner ℂ eta (rho b eta) = phi b * inner ℂ eta eta := h 186 _ = phi b := by rw [hself, mul_one] 187 have hrho' : Representation.IsIrreducible rho := 188 (Representation.isIrreducible_iff_starAlgHom rho).2 hrho 189 have hetaCyclic : DenseRange (StarAlgHom.orbitMap rho eta) := 190 Representation.denseRange_orbitMap_of_isIrreducible rho hrho' heta_ne 191 obtain ⟨U, hU, -⟩ := StarAlgHom.existsUnique_pointedCyclicTransport 192 pi rho xi eta hxiCyclic hetaCyclic (fun b ↦ (hxiState b).trans (heta_state b).symm) 193 exact hno U hU.2.2 194 195/-- If exactly one fiber of an arbitrary atomic sum has a nonzero common fixed 196projection, its atomic common fixed space is the span of the corresponding 197coordinate vector. -/ 198theorem iInf_range_atomicRepresentation_eq_span 199 {I : Type v} {H : I → Type w} 200 [DecidableEq I] 201 [∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℂ (H i)] 202 [∀ i, CompleteSpace (H i)] 203 (pi : ∀ i, Representation A (H i)) 204 (q : ℕ → A) (hq : ∀ n, IsStarProjection (q n)) 205 (i : I) (xi : H i) (hxi : ‖xi‖ = 1) 206 (hsame : commonFixedProjection (fun n ↦ pi i (q n)) = 207 InnerProductSpace.rankOne ℂ xi xi) 208 (hother : ∀ j, j ≠ i → 209 commonFixedProjection (fun n ↦ pi j (q n)) = 0) : 210 (⨅ n, (atomicRepresentation pi (q n)).range) = 211 ℂ ∙ coordinateEmbedding i xi := by 212 let Q (j : I) : ℕ → H j →L[ℂ] H j := fun n ↦ pi j (q n) 213 have hxiCommon : xi ∈ commonFixedSubspace (Q i) := by 214 rw [← commonFixedProjection_eq_self_iff] 215 rw [hsame] 216 simp [InnerProductSpace.rankOne_apply, inner_self_eq_norm_sq_to_K, hxi] 217 have hxiFixed : ∀ n, pi i (q n) xi = xi := 218 (mem_commonFixedSubspace_iff (Q i) xi).1 hxiCommon 219 apply le_antisymm 220 · intro x hx 221 have hfixed (n : ℕ) : atomicRepresentation pi (q n) x = x := by 222 rcases (Submodule.mem_iInf 223 (fun n ↦ (atomicRepresentation pi (q n)).range)).mp hx n with ⟨y, rfl⟩ 224 change atomicRepresentation pi (q n) 225 (atomicRepresentation pi (q n) y) = atomicRepresentation pi (q n) y 226 rw [← ContinuousLinearMap.mul_apply, ← map_mul, 227 (hq n).isIdempotentElem.eq] 228 have hfiberFixed (j : I) : ∀ n, pi j (q n) (x j) = x j := by 229 intro n 230 exact congrArg (fun y : HilbertSum H ↦ y j) (hfixed n) 231 have hfiberProjection (j : I) : commonFixedProjection (Q j) (x j) = x j := 232 (commonFixedProjection_eq_self_iff (Q j) (x j)).2 233 ((mem_commonFixedSubspace_iff (Q j) (x j)).2 (hfiberFixed j)) 234 refine Submodule.mem_span_singleton.mpr ⟨inner ℂ xi (x i), ?_⟩ 235 apply lp.ext 236 funext j 237 by_cases hji : j = i 238 · subst j 239 have hi := hfiberProjection i 240 rw [hsame] at hi 241 simpa [coordinateEmbedding_apply, InnerProductSpace.rankOne_apply] using hi 242 · have hj := hfiberProjection j 243 rw [hother j hji] at hj 244 have hxj : x j = 0 := by simpa using hj.symm 245 simp [coordinateEmbedding_apply, lp.coeFn_single, hji, hxj] 246 · intro x hx 247 obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.mp hx 248 apply (Submodule.mem_iInf 249 (fun n ↦ (atomicRepresentation pi (q n)).range)).mpr 250 intro n 251 refine ⟨c • coordinateEmbedding i xi, ?_⟩ 252 calc 253 atomicRepresentation pi (q n) (c • coordinateEmbedding i xi) = 254 c • atomicRepresentation pi (q n) (coordinateEmbedding i xi) := 255 map_smul _ _ _ 256 _ = c • lp.single 2 i (pi i (q n) xi) := by 257 rw [coordinateEmbedding_apply, atomicRepresentation_single] 258 _ = c • coordinateEmbedding i xi := by 259 rw [hxiFixed n, coordinateEmbedding_apply] 260 261end MathlibAnnex.Analysis.CStarAlgebra