Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/CommonFixedSubspace.lean
Pinned GitHub source · Raw UTF-8 source
Back to The atomic common range is one embedded GNS line
1import MathlibAnnex.Analysis.CStarAlgebra.Compression2import MathlibAnnex.Analysis.CStarAlgebra.CyclicTransport3import MathlibAnnex.Analysis.CStarAlgebra.Representation.Adapters4import MathlibAnnex.Analysis.CStarAlgebra.Representation.Atomic5import MathlibAnnex.Analysis.CStarAlgebra.Representation.VectorFunctional6import MathlibAnnex.Analysis.CStarAlgebra.Intertwiner7import MathlibAnnex.Analysis.InnerProductSpace.HilbertSumCoordinates8import MathlibAnnex.Analysis.InnerProductSpace.RankOne9import Mathlib.Analysis.Normed.Module.Normalize1011/-!12# Fixed spaces of represented projection flags1314Compression identifies the common fixed projection in its cyclic fiber and15excludes it in inequivalent irreducible fibers. A coordinate argument then16identifies the common fixed space of an arbitrary dependent atomic sum.17-/1819set_option autoImplicit false2021open Filter Topology22open scoped ENNReal lp InnerProduct2324namespace MathlibAnnex.Analysis.CStarAlgebra2526open MathlibAnnex.Analysis.InnerProductSpace2728universe u v w2930variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]3132/-- For represented star projections, being fixed is equivalent to belonging33to the operator range, so the common fixed subspace is the infimum of the34ranges. -/35theorem commonFixedSubspace_eq_iInf_range36 {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 := by40 ext x41 rw [mem_commonFixedSubspace_iff, Submodule.mem_iInf]42 apply forall_congr'43 intro n44 exact (LinearMap.IsIdempotentElem.mem_range_iff45 (ContinuousLinearMap.IsIdempotentElem.toLinearMap46 ((hq n).map pi).isIdempotentElem)).symm4748/-- A supplied star projection with the represented common-fixed range is49the canonical common fixed projection. -/50theorem starProjection_eq_commonFixedProjection_of_range_iInf51 {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)) := by57 obtain ⟨hProjection, hPeq⟩ :=58 isStarProjection_iff_eq_starProjection_range.mp hP59 have hrange : P.range = commonFixedSubspace (fun n ↦ pi (q n)) :=60 hPrange.trans (commonFixedSubspace_eq_iInf_range pi q hq).symm61 simpa only [commonFixedProjection, hrange] using hPeq6263/-- A projection has to fix a unit vector when its vector state takes value64one on that projection. -/65theorem projection_apply_eq_self_of_vectorFunctional_eq_one66 {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 := by72 have hcomp : IsStarProjection (1 - p) := hp.one_sub73 have hfunctional :74 Representation.vectorFunctional pi xi (star (1 - p) * (1 - p)) = 0 := by75 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 := by78 rw [← Representation.vectorFunctional_star_mul]79 exact hfunctional80 have hzero : pi (1 - p) xi = 0 := inner_self_eq_zero.mp hinner81 have hsub : xi - pi p xi = 0 := by82 simpa [map_sub, map_one] using hzero83 exact (sub_eq_zero.mp hsub).symm8485/-- A unit vector fixed by every member of a compressing self-adjoint flag86has exactly the limiting compression functional as its vector state. -/87theorem vectorFunctional_eq_of_compression_tendsto88 {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 := by97 apply ContinuousLinearMap.ext98 intro b99 have hcoeff := inner_map_eq_of_compression_tendsto pi100 (Representation.continuousLinearMap pi).continuous q phi b eta eta101 hq_star hfixed hfixed (hcompression b)102 have hself : inner ℂ eta eta = 1 := by103 rw [inner_self_eq_norm_sq_to_K, heta]104 norm_num105 change inner ℂ eta (pi b eta) = phi b106 calc107 inner ℂ eta (pi b eta) = phi b * inner ℂ eta eta := hcoeff108 _ = phi b := by rw [hself, mul_one]109110/-- In a cyclic realization of the compression state, the represented common111fixed projection is exactly the projection onto the cyclic vector. -/112theorem commonFixedProjection_eq_rankOne_of_dense_orbit113 {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 := by124 let Q : ℕ → H →L[ℂ] H := fun n ↦ pi (q n)125 let P := commonFixedProjection Q126 apply projection_eq_rankOne_of_dense_orbit pi phi P xi127 · exact (commonFixedProjection_eq_self_iff Q xi).2128 ((mem_commonFixedSubspace_iff Q xi).2 hfixed)129 · intro b130 exact commonFixedProjection_comp_map_comp_eq pi131 (Representation.continuousLinearMap pi).continuous q phi b hq_star132 (hcompression b)133 · exact hphi134 · exact hdense135136/-- In an inequivalent irreducible realization, the common fixed projection137of a flag with a pure cyclic compression state must vanish. -/138theorem commonFixedProjection_eq_zero_of_no_unitary139 {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 := by154 let Q : ℕ → K →L[ℂ] K := fun n ↦ rho (q n)155 let P := commonFixedProjection Q156 by_contra hP157 have hex : ∃ z : K, P z ≠ 0 := by158 by_contra h159 push_neg at h160 apply hP161 ext z162 exact h z163 obtain ⟨z, hz⟩ := hex164 let r : ℝ := ‖P z‖165 have hr : r ≠ 0 := norm_ne_zero_iff.mpr hz166 let eta : K := ((r⁻¹ : ℝ) : ℂ) • P z167 have heta_norm : ‖eta‖ = 1 := by168 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 := by173 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 := by178 have h := inner_map_eq_of_compression_tendsto rho179 (Representation.continuousLinearMap rho).continuous q phi b eta eta180 hq_star heta_fixed heta_fixed (hcompression b)181 have hself : inner ℂ eta eta = 1 := by182 rw [inner_self_eq_norm_sq_to_K, heta_norm]183 norm_num184 calc185 inner ℂ eta (rho b eta) = phi b * inner ℂ eta eta := h186 _ = phi b := by rw [hself, mul_one]187 have hrho' : Representation.IsIrreducible rho :=188 (Representation.isIrreducible_iff_starAlgHom rho).2 hrho189 have hetaCyclic : DenseRange (StarAlgHom.orbitMap rho eta) :=190 Representation.denseRange_orbitMap_of_isIrreducible rho hrho' heta_ne191 obtain ⟨U, hU, -⟩ := StarAlgHom.existsUnique_pointedCyclicTransport192 pi rho xi eta hxiCyclic hetaCyclic (fun b ↦ (hxiState b).trans (heta_state b).symm)193 exact hno U hU.2.2194195/-- If exactly one fiber of an arbitrary atomic sum has a nonzero common fixed196projection, its atomic common fixed space is the span of the corresponding197coordinate vector. -/198theorem iInf_range_atomicRepresentation_eq_span199 {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 := by212 let Q (j : I) : ℕ → H j →L[ℂ] H j := fun n ↦ pi j (q n)213 have hxiCommon : xi ∈ commonFixedSubspace (Q i) := by214 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 hxiCommon219 apply le_antisymm220 · intro x hx221 have hfixed (n : ℕ) : atomicRepresentation pi (q n) x = x := by222 rcases (Submodule.mem_iInf223 (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) y226 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 := by229 intro n230 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)).2233 ((mem_commonFixedSubspace_iff (Q j) (x j)).2 (hfiberFixed j))234 refine Submodule.mem_span_singleton.mpr ⟨inner ℂ xi (x i), ?_⟩235 apply lp.ext236 funext j237 by_cases hji : j = i238 · subst j239 have hi := hfiberProjection i240 rw [hsame] at hi241 simpa [coordinateEmbedding_apply, InnerProductSpace.rankOne_apply] using hi242 · have hj := hfiberProjection j243 rw [hother j hji] at hj244 have hxj : x j = 0 := by simpa using hj.symm245 simp [coordinateEmbedding_apply, lp.coeFn_single, hji, hxj]246 · intro x hx247 obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.mp hx248 apply (Submodule.mem_iInf249 (fun n ↦ (atomicRepresentation pi (q n)).range)).mpr250 intro n251 refine ⟨c • coordinateEmbedding i xi, ?_⟩252 calc253 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) := by257 rw [coordinateEmbedding_apply, atomicRepresentation_single]258 _ = c • coordinateEmbedding i xi := by259 rw [hxiFixed n, coordinateEmbedding_apply]260261end MathlibAnnex.Analysis.CStarAlgebra