Exact source: MathlibAnnex/Analysis/CStarAlgebra/NonUnital/CompactExclusion.lean
Pinned GitHub source · Raw UTF-8 source
Back to A singleton model is faithful and exactly compact-valued · Back to Every operator in a singleton image is compact
1import Mathlib.RingTheory.TwoSidedIdeal.Operations2import MathlibAnnex.Analysis.CStarAlgebra.ClosedIdealCharacter3import MathlibAnnex.Analysis.CStarAlgebra.CompactPreimage4import MathlibAnnex.Analysis.CStarAlgebra.MaximalAbelianContaining5import MathlibAnnex.Analysis.CStarAlgebra.NonUnital.CompactRange6import MathlibAnnex.Analysis.InnerProductSpace.RankOne78/-!9# Excluding noncompact elements from a non-unital singleton model1011If a represented self-adjoint element were noncompact, put it in a maximal12abelian subalgebra of the unitization. The compact-preimage ideal in that13subalgebra is closed. A character separating the element from this ideal is14non-scalar, hence is realized by a unit eigenvector. The corresponding15rank-one projection is already in the range of the original algebra. Its16operator commutes with the maximal abelian subalgebra, so faithfulness puts17the projection itself in that subalgebra. The separating character must18then take both values zero and one on it, a contradiction.19-/2021set_option autoImplicit false2223open Set24open scoped ComplexOrder ComplexStarModule InnerProduct IsMulCommutative2526namespace MathlibAnnex.Analysis.CStarAlgebra2728universe u v2930variable {A : Type u} [NonUnitalCStarAlgebra A]31 [PartialOrder A] [StarOrderedRing A]32variable {H : Type v}33variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]3435namespace NonUnitalCStarRepresentation3637/-- If an operator-valued complex-linear map sends both real and imaginary38parts of an element to compact operators, it sends the element itself to a39compact operator. -/40private theorem isCompactOperator_of_realPart_of_imaginaryPart41 (pi : NonUnitalCStarRepresentation A H) (a : A)42 (hre : IsCompactOperator (pi (ℜ a : A)))43 (him : IsCompactOperator (pi (ℑ a : A))) :44 IsCompactOperator (pi a) := by45 have hsum : IsCompactOperator46 (pi (ℜ a : A) + Complex.I • pi (ℑ a : A)) :=47 hre.add (him.smul Complex.I)48 have hop : pi a = pi (ℜ a : A) + Complex.I • pi (ℑ a : A) := by49 calc50 pi a = pi ((ℜ a : A) + Complex.I • (ℑ a : A)) := by51 rw [realPart_add_I_smul_imaginaryPart]52 _ = pi (ℜ a : A) + Complex.I • pi (ℑ a : A) := by simp53 rw [hop]54 exact hsum5556/-- A noncompact represented element has a self-adjoint part whose image is57still noncompact. -/58private theorem exists_selfAdjoint_not_isCompactOperator59 (pi : NonUnitalCStarRepresentation A H) {a : A}60 (ha : ¬ IsCompactOperator (pi a)) :61 ∃ b : A, IsSelfAdjoint b ∧ ¬ IsCompactOperator (pi b) := by62 by_cases hre : IsCompactOperator (pi (ℜ a : A))63 · refine ⟨(ℑ a : A), (ℑ a).property, ?_⟩64 intro him65 exact ha (isCompactOperator_of_realPart_of_imaginaryPart pi a hre him)66 · exact ⟨(ℜ a : A), (ℜ a).property, hre⟩6768/-- In a genuinely non-unital separable singleton irreducible model every69represented operator is compact. No simplicity assumption is used. -/70theorem isCompactOperator_map_of_singleton [Nontrivial A]71 [TopologicalSpace.SeparableSpace H]72 (pi : NonUnitalCStarRepresentation A H)73 (hsingle : IsSingletonIrreducibleModel.{u, v, u} pi) :74 ∀ a : A, IsCompactOperator (pi a) := by75 intro a76 by_contra ha77 obtain ⟨b, hbself, hbcompact⟩ :=78 exists_selfAdjoint_not_isCompactOperator pi ha79 have hbinrself : IsSelfAdjoint (b : Unitization ℂ A) := hbself.inr ℂ80 obtain ⟨D, hD, hbD⟩ :=81 exists_maximalAbelian_containing_isSelfAdjoint82 (b : Unitization ℂ A) hbinrself83 letI : IsClosed (D : Set (Unitization ℂ A)) := hD.isClosed84 letI : IsMulCommutative D := hD.185 letI : CommCStarAlgebra D := {}86 let rhoD : Representation D H := pi.unitization.comp D.subtype87 let Jtwo : TwoSidedIdeal D :=88 MathlibAnnex.CStarAlgebra.compactPreimageIdeal89 rhoD.toNonUnitalStarAlgHom90 let J : Ideal D := Jtwo.asIdeal91 have hJclosed : IsClosed (J : Set D) := by92 change IsClosed (Jtwo : Set D)93 exact MathlibAnnex.CStarAlgebra.isClosed_compactPreimageIdeal94 rhoD.toNonUnitalStarAlgHom95 let d : D := ⟨(b : Unitization ℂ A), hbD⟩96 have hdnot : d ∉ J := by97 intro hd98 have hdTwo : d ∈ Jtwo := hd99 have hcompact : IsCompactOperator (rhoD d) :=100 (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal101 rhoD.toNonUnitalStarAlgHom d).1 hdTwo102 apply hbcompact103 simpa [rhoD, d] using hcompact104 obtain ⟨chi, hchiJ, hchid⟩ :=105 exists_character_annihilating_closedIdeal_of_not_mem J hJclosed hdnot106 have hchiInf : chi ≠ infinityCharacterOn (A := A) D := by107 intro heq108 apply hchid109 rw [heq]110 simp [d]111 obtain ⟨eta, heta, heigen⟩ :=112 exists_unit_eigenvector_of_character_ne_infinity113 pi hsingle D chi hchiInf114 obtain ⟨q, hq⟩ :=115 exists_preimage_rankOne_of_singleton pi hsingle eta eta116 have hinj : Function.Injective pi := injective_of_singleton pi hsingle117 have heta_ne : eta ≠ 0 := by118 intro hzero119 simp [hzero] at heta120 have hcommute (x : D) :121 (q : Unitization ℂ A) * (x : Unitization ℂ A) =122 (x : Unitization ℂ A) * (q : Unitization ℂ A) := by123 have hadj : ContinuousLinearMap.adjoint (rhoD x) eta =124 star (chi x) • eta := by125 have hadjmap : ContinuousLinearMap.adjoint (rhoD x) = rhoD (star x) := by126 rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star]127 rw [hadjmap]128 exact heigen (star x) |>.trans (by rw [map_star])129 have hoperator :130 rhoD x * InnerProductSpace.rankOne ℂ eta eta =131 InnerProductSpace.rankOne ℂ eta eta * rhoD x :=132 MathlibAnnex.Analysis.InnerProductSpace.commute_rankOne_self_of_apply_eq_smul_of_adjoint_apply_eq_star_smul133 (rhoD x) eta (chi x) (heigen x) hadj134 have hrhoD : rhoD x =135 (x : Unitization ℂ A).fst • (1 : H →L[ℂ] H) +136 pi (x : Unitization ℂ A).snd := by137 change pi.unitization (x : Unitization ℂ A) = _138 induction (x : Unitization ℂ A) using Unitization.ind with139 | inl_add_inr c y => simp [unitization, Algebra.algebraMap_eq_smul_one]140 have hpiComm :141 pi (x : Unitization ℂ A).snd *142 InnerProductSpace.rankOne ℂ eta eta =143 InnerProductSpace.rankOne ℂ eta eta *144 pi (x : Unitization ℂ A).snd := by145 apply add_left_cancel (a :=146 (x : Unitization ℂ A).fst •147 InnerProductSpace.rankOne ℂ eta eta)148 simpa [hrhoD, add_mul, mul_add, smul_mul_assoc, mul_smul_comm] using149 hoperator150 have hqCommA : q * (x : Unitization ℂ A).snd =151 (x : Unitization ℂ A).snd * q := by152 apply hinj153 simpa [map_mul, hq] using hpiComm.symm154 apply Unitization.ext155 · simp156 · simpa [hqCommA]157 have hqDmem : (q : Unitization ℂ A) ∈ D :=158 hD.mem_of_commute hcommute159 let r : D := ⟨(q : Unitization ℂ A), hqDmem⟩160 have hrJ : r ∈ J := by161 have hcompactr : IsCompactOperator (rhoD r) := by162 rw [show rhoD r = pi q by simp [rhoD, r], hq]163 exact isCompactOperator_rankOne eta eta164 have hrTwo : r ∈ Jtwo :=165 (MathlibAnnex.CStarAlgebra.mem_compactPreimageIdeal166 rhoD.toNonUnitalStarAlgHom r).2 hcompactr167 exact hrTwo168 have hchirZero : chi r = 0 := hchiJ r hrJ169 have hmapr : rhoD r = InnerProductSpace.rankOne ℂ eta eta := by170 simpa [rhoD, r] using hq171 have hprojectionEta :172 InnerProductSpace.rankOne ℂ eta eta eta = eta := by173 simp [InnerProductSpace.rankOne_apply,174 inner_self_eq_norm_sq_to_K, heta]175 have hchirOne : chi r = 1 := by176 apply smul_left_injective ℂ heta_ne177 calc178 chi r • eta = rhoD r eta := (heigen r).symm179 _ = InnerProductSpace.rankOne ℂ eta eta eta := by rw [hmapr]180 _ = eta := hprojectionEta181 _ = (1 : ℂ) • eta := (one_smul ℂ eta).symm182 exact one_ne_zero (hchirOne ▸ hchirZero)183184end NonUnitalCStarRepresentation185186end MathlibAnnex.Analysis.CStarAlgebra