Exact source: MathlibAnnex/Analysis/CStarAlgebra/Representation/RankOneProjection.lean
Pinned GitHub source · Raw UTF-8 source
Back to A unital singleton model acts in finite dimension
1import MathlibAnnex.Analysis.CStarAlgebra.CompactModel2import MathlibAnnex.Analysis.CStarAlgebra.Representation.Adapters3import MathlibAnnex.Analysis.CStarAlgebra.Representation.MinimalProjection4import MathlibAnnex.Analysis.InnerProductSpace.RankOne56/-!7# Scalar corners act as rank-one projections89In an irreducible representation, a nonzero projection whose algebraic corner10is one-dimensional is represented by a rank-one orthogonal projection. The11argument uses only density of the orbit of a nonzero vector in the range of the12projection and closedness of a one-dimensional subspace.13-/1415set_option autoImplicit false1617open Set1819namespace MathlibAnnex.Analysis.CStarAlgebra2021universe u v2223variable {A : Type u} [CStarAlgebra A]24variable {H : Type v}25variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2627namespace Representation2829/-- A nonzero scalar corner is represented by a rank-one projection in an30irreducible representation. -/31theorem exists_unitVector_map_eq_rankOne_of_scalar_corner32 (pi : Representation A H) (hirr : pi.IsIrreducible)33 {p : A} (hp : IsStarProjection p) (hpmap : pi p ≠ 0)34 (hcorner : ∀ a : A, ∃ c : ℂ, p * a * p = c • p) :35 ∃ e : H, ‖e‖ = 1 ∧36 pi p = InnerProductSpace.rankOne ℂ e e := by37 classical38 let P : H →L[ℂ] H := pi p39 have hPstar : IsStarProjection P := hp.map pi40 obtain ⟨xi, hxi⟩ : ∃ xi : H, P xi ≠ 0 := by41 by_contra h42 push_neg at h43 apply hpmap44 apply ContinuousLinearMap.ext45 intro x46 simpa [P] using h x47 let v : H := P xi48 have hv : v ≠ 0 := hxi49 have horbit : DenseRange (StarAlgHom.orbitMap pi v) :=50 denseRange_orbitMap_of_isIrreducible pi hirr hv51 have hPrange : P.range = ℂ ∙ v := by52 apply le_antisymm53 · rintro y ⟨x, rfl⟩54 have hx : x ∈ closure (Set.range (StarAlgHom.orbitMap pi v)) := by55 rw [horbit.closure_range]56 trivial57 apply (Set.MapsTo.closure_left (f := P)58 (s := Set.range (StarAlgHom.orbitMap pi v))59 (t := (ℂ ∙ v : Submodule ℂ H)) ?_60 P.continuous (Submodule.closed_of_finiteDimensional (ℂ ∙ v))) hx61 rintro _ ⟨a, rfl⟩62 obtain ⟨c, hc⟩ := hcorner a63 have hcalc : P (pi a v) = c • v := by64 calc65 P (pi a v) = (P * pi a * P) xi := rfl66 _ = pi (p * a * p) xi := by simp [P]67 _ = pi (c • p) xi := by rw [hc]68 _ = c • v := by simp [P, v]69 change P (pi a v) ∈ (ℂ ∙ v : Submodule ℂ H)70 rw [hcalc]71 exact Submodule.smul_mem _ c (Submodule.mem_span_singleton_self v)72 · rw [Submodule.span_singleton_le_iff_mem]73 exact ⟨xi, rfl⟩74 let e : H := ((‖v‖⁻¹ : ℝ) : ℂ) • v75 have hvnorm : ‖v‖ ≠ 0 := norm_ne_zero_iff.mpr hv76 have he : ‖e‖ = 1 := by77 simp [e, norm_smul, hvnorm]78 have hspan : ℂ ∙ v = ℂ ∙ e := by79 apply le_antisymm80 · rw [Submodule.span_singleton_le_iff_mem]81 apply Submodule.mem_span_singleton.mpr82 refine ⟨((‖v‖ : ℝ) : ℂ), ?_⟩83 simp [e, hvnorm]84 · rw [Submodule.span_singleton_le_iff_mem]85 exact Submodule.smul_mem _ _ (Submodule.mem_span_singleton_self v)86 letI : P.range.HasOrthogonalProjection :=87 Classical.choose (isStarProjection_iff_eq_starProjection_range.mp hPstar)88 have hPeq : P = P.range.starProjection :=89 Classical.choose_spec (isStarProjection_iff_eq_starProjection_range.mp hPstar)90 refine ⟨e, he, ?_⟩91 change P = InnerProductSpace.rankOne ℂ e e92 calc93 P = P.range.starProjection := hPeq94 _ = InnerProductSpace.rankOne ℂ e e :=95 MathlibAnnex.Analysis.InnerProductSpace.starProjection_eq_rankOne_of_eq_span96 P.range e he (hPrange.trans hspan)9798/-- A nonzero scalar corner has compact image in an irreducible99representation. -/100theorem isCompactOperator_map_of_scalar_corner101 (pi : Representation A H) (hirr : pi.IsIrreducible)102 {p : A} (hp : IsStarProjection p) (hpmap : pi p ≠ 0)103 (hcorner : ∀ a : A, ∃ c : ℂ, p * a * p = c • p) :104 IsCompactOperator (pi p) := by105 obtain ⟨e, _he, hmap⟩ :=106 exists_unitVector_map_eq_rankOne_of_scalar_corner pi hirr hp hpmap hcorner107 rw [hmap]108 exact isCompactOperator_rankOne e e109110end Representation111112end MathlibAnnex.Analysis.CStarAlgebra