MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectrumSingleton.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.NormalPartComponentClosed7import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.SpectralHomeomorph8import MathlibAnnex.Analysis.Normed.GeometricStructure.Separation910/-!11# Singleton irreducible spectra and faithful images with full normal part1213Singleton means `∃ q, ∀ r, r = q`, so existence is not lost. The spectrum14is the independently defined pure-state GNS quotient, not the primitive15kernel quotient. Its proved homeomorphism with GS is used on actual points.1617Faithfulness is DERIVED from the intersection of all GSS points being zero18and the whole-component identity J_C = ker(pi). In the converse direction19faithfulness gives density, while full normality gives closedness. Neither20condition alone is substituted for the other. No elementary-algebra claim21or result about the zero algebra is made here.22-/2324set_option autoImplicit false25noncomputable section26open Set27open scoped CStarAlgebra2829namespace MathlibAnnex.Analysis.CStarAlgebra3031universe u v32variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]33variable [PartialOrder A] [StarOrderedRing A]34variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]3536attribute [local instance] HomKernelQuotient.imageCStarAlgebra HomKernelQuotient.isClosed_image3738attribute [local instance] geometricSpectrumTopology3940open NonUnitalCStarRepresentation4142private def singletonContinuousMap (pi : NonUnitalCStarRepresentation A H) :43    A →L[ℂ] (H →L[ℂ] H) :=44  LinearMap.mkContinuous45    { toFun := pi, map_add' := map_add pi, map_smul' := map_smul pi }46    1 (fun a => by47      change ‖pi a‖ ≤ 1 * ‖a‖48      simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le pi a)4950/-- An entire coefficient component fills S(A) precisely when its representation51is faithful and its ACTUAL image GSS is all normal. -/52theorem component_matrixCoefficientKernel_eq_univ_iff53    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)54    (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) :55    (NormedSpace.geometricStructureClosure ℂ A).component56      (matrixCoefficientKernel pi hpi x y hx hy) = Set.univ ↔57      Function.Injective pi ∧ normalPart (NonUnitalStarAlgHom.range pi) = Set.univ := by58  let c := NormedSpace.geometricStructureClosure ℂ A59  let I := matrixCoefficientKernel pi hpi x y hx hy60  have hkernel : ClosureSpace.HullKernel.kernel (NormedSpace.geometricStructureFamily ℂ A)61      (c.component I) = ((singletonContinuousMap pi).ker : Set A) :=62    geometricSpectrumKernel_toGeometricSpectrum_matrixCoefficientKernel pi hpi x y hx hy63  constructor64  · intro hC65    have hk : ((singletonContinuousMap pi).ker : Set A) = ({0} : Set A) := by66      rw [← hkernel, hC]67      exact NormedSpace.kernel_geometricStructureFamily_univ ℂ A68    have hfaith : Function.Injective pi := by69      intro a b hab70      have hz : a - b ∈ ((singletonContinuousMap pi).ker : Set A) := by71        change pi (a - b) = 072        rw [map_sub, hab, sub_self]73      rw [hk] at hz74      exact sub_eq_zero.mp (Set.mem_singleton_iff.mp hz)75    refine ⟨hfaith, ?_⟩76    apply (isClosed_component_matrixCoefficientKernel_iff_normalPart_eq_univ77      pi hpi x y hx hy).178    rw [hC]79    exact c.isClosed_univ80  · rintro ⟨hfaith, hnormal⟩81    have hk : ((singletonContinuousMap pi).ker : Set A) = ({0} : Set A) := by82      ext a83      change pi a = 0 ↔ a = 084      exact ⟨fun ha => hfaith (ha.trans (map_zero pi).symm),85        fun ha => ha ▸ map_zero pi⟩86    have hdense : c.closure (c.component I) = Set.univ :=87      (NormedSpace.geometricStructureClosure_eq_univ_iff_kernel_eq_singleton_zero88        ℂ A (c.component I)).2 (hkernel.trans hk)89    have hc : c.IsClosed (c.component I) :=90      (isClosed_component_matrixCoefficientKernel_iff_normalPart_eq_univ91        pi hpi x y hx hy).2 hnormal92    exact ((c.isClosed_iff _).1 hc).symm.trans hdense9394/-- Specialization to the actual GNS of a pure state. -/95theorem component_geometricPoint_eq_univ_iff (phi : NonUnitalPureState A) :96    (NormedSpace.geometricStructureClosure ℂ A).component phi.geometricPoint = Set.univ ↔97      Function.Injective phi.gnsRepresentation ∧98        normalPart (NonUnitalStarAlgHom.range phi.gnsRepresentation) = Set.univ := by99  rw [phi.geometricPoint_eq_matrixCoefficientKernel]100  exact component_matrixCoefficientKernel_eq_univ_iff101    phi.gnsRepresentation phi.isIrreducible_gnsRepresentation102    phi.gnsVector phi.gnsVector phi.gnsVector_ne_zero phi.gnsVector_ne_zero103104/-- The independently defined spectrum is a singleton exactly when one actual105component fills the original GSS. The proved ordinary spectral homeomorphism106supplies the equivalence, with its point formula unchanged. -/107theorem exists_forall_eq_irreducibleSpectrum_iff_exists_component_eq_univ :108    (∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q) ↔109      ∃ I : NormedSpace.GeometricStructureSpace ℂ A,110        (NormedSpace.geometricStructureClosure ℂ A).component I = Set.univ := by111  let c := NormedSpace.geometricStructureClosure ℂ A112  let e := (irreducibleSpectrumHomeomorph A).toEquiv113  constructor114  · rintro ⟨q, hq⟩115    obtain ⟨I, hI⟩ := NormedSpace.toGeometricSpectrum_surjective ℂ A (e q)116    refine ⟨I, Set.eq_univ_iff_forall.mpr (fun J => ?_)⟩117    have heJ := e.apply_symm_apply (NormedSpace.toGeometricSpectrum ℂ A J)118    have hIJ : NormedSpace.toGeometricSpectrum ℂ A I =119        NormedSpace.toGeometricSpectrum ℂ A J :=120      hI.trans ((congrArg e (hq (e.symm (NormedSpace.toGeometricSpectrum ℂ A J)))).symm.trans heJ)121    exact (c.toComponentPoint_eq_iff I J).1 hIJ122  · rintro ⟨I, hI⟩123    let q := e.symm (NormedSpace.toGeometricSpectrum ℂ A I)124    refine ⟨q, fun r => e.injective ?_⟩125    obtain ⟨J, hJ⟩ := NormedSpace.toGeometricSpectrum_surjective ℂ A (e r)126    have hrel : c.Related I J := by127      change J ∈ c.component I128      rw [hI]129      trivial130    have hIJ := (c.toComponentPoint_eq_iff I J).2 hrel131    exact hJ.symm.trans (hIJ.symm.trans132      (e.apply_symm_apply (NormedSpace.toGeometricSpectrum ℂ A I)).symm)133134/-- Corollary 7.3 with a small, genuine GNS witness. Faithfulness in the135forward implication is proved from the total intersection, not assumed. -/136theorem exists_forall_eq_irreducibleSpectrum_iff_exists_faithful_pureState :137    (∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q) ↔138      ∃ phi : NonUnitalPureState A, Function.Injective phi.gnsRepresentation ∧139        normalPart (NonUnitalStarAlgHom.range phi.gnsRepresentation) = Set.univ := by140  rw [exists_forall_eq_irreducibleSpectrum_iff_exists_component_eq_univ]141  constructor142  · rintro ⟨I, hI⟩143    obtain ⟨phi, hphi⟩ := NonUnitalPureState.toGeometricSpectrum_surjective144      (NormedSpace.toGeometricSpectrum ℂ A I)145    have hcomp : (NormedSpace.geometricStructureClosure ℂ A).component phi.geometricPoint =146        (NormedSpace.geometricStructureClosure ℂ A).component I := congrArg Subtype.val hphi147    exact ⟨phi, (component_geometricPoint_eq_univ_iff phi).1 (hcomp.trans hI)⟩148  · rintro ⟨phi, hfaith, hnormal⟩149    exact ⟨phi.geometricPoint, (component_geometricPoint_eq_univ_iff phi).2 ⟨hfaith, hnormal⟩⟩150151/-- A faithful nonzero irreducible action in ANY Hilbert universe with full152normal part forces a singleton of the independent small spectrum. -/153theorem exists_forall_eq_irreducibleSpectrum_of_faithful_representation154    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)155    (hfaith : Function.Injective pi) (hnormal : normalPart (NonUnitalStarAlgHom.range pi) = Set.univ) :156    ∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q := by157  letI : Nontrivial H := nontrivial_of_isNonzero pi hpi.1158  obtain ⟨x, hx⟩ := exists_ne (0 : H)159  apply exists_forall_eq_irreducibleSpectrum_iff_exists_component_eq_univ.2160  exact ⟨matrixCoefficientKernel pi hpi x x hx hx,161    (component_matrixCoefficientKernel_eq_univ_iff pi hpi x x hx hx).2 ⟨hfaith, hnormal⟩⟩162163/-- In a singleton spectrum, EVERY nonzero irreducible representation is164faithful and has full normal part. This includes arbitrary Hilbert universes. -/165theorem faithful_and_normalPart_eq_univ_of_singleton_irreducibleSpectrum166    (hsingle : ∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q)167    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) :168    Function.Injective pi ∧ normalPart (NonUnitalStarAlgHom.range pi) = Set.univ := by169  obtain ⟨q, hq⟩ := hsingle170  letI : Nontrivial H := nontrivial_of_isNonzero pi hpi.1171  obtain ⟨x, hx⟩ := exists_ne (0 : H)172  let c := NormedSpace.geometricStructureClosure ℂ A173  let I := matrixCoefficientKernel pi hpi x x hx hx174  apply (component_matrixCoefficientKernel_eq_univ_iff pi hpi x x hx hx).1175  apply Set.eq_univ_iff_forall.mpr176  intro J177  let e := (irreducibleSpectrumHomeomorph A).toEquiv178  have heq : e.symm (NormedSpace.toGeometricSpectrum ℂ A I) =179      e.symm (NormedSpace.toGeometricSpectrum ℂ A J) :=180    (hq _).trans (hq _).symm181  have hIJ : NormedSpace.toGeometricSpectrum ℂ A I =182      NormedSpace.toGeometricSpectrum ℂ A J := e.symm.injective heq183  exact (c.toComponentPoint_eq_iff I J).1 hIJ184185/-- The literal existence-of-faithful-representation formulation of 7.3.186The witness lives in the universe of A because the actual GNS construction187does. The previous two theorems handle every separately specified universe.188The local structures are actual structures, not certificates containing189faithfulness, normality, or the desired singleton conclusion. -/190theorem exists_forall_eq_irreducibleSpectrum_iff_exists_faithful_representation :191    (∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q) ↔192    (∃ (H' : Type u) (instN : NormedAddCommGroup H'),193      letI := instN194      ∃ instI : InnerProductSpace ℂ H',195        letI := instI196        ∃ instC : CompleteSpace H',197          letI := instC198          ∃ pi : NonUnitalCStarRepresentation A H',199            pi.IsIrreducible ∧ Function.Injective pi ∧ normalPart (NonUnitalStarAlgHom.range pi) = Set.univ) := by200  constructor201  · intro hsingle202    obtain ⟨phi, hfaith, hnormal⟩ :=203      exists_forall_eq_irreducibleSpectrum_iff_exists_faithful_pureState.1 hsingle204    exact ⟨phi.GNS, inferInstance, inferInstance, inferInstance, phi.gnsRepresentation,205      phi.isIrreducible_gnsRepresentation, hfaith, hnormal⟩206  · rintro ⟨H', instN, h⟩207    letI := instN208    obtain ⟨instI, h⟩ := h209    letI := instI210    obtain ⟨instC, h⟩ := h211    letI := instC212    obtain ⟨pi, hpi, hfaith, hnormal⟩ := h213    exact exists_forall_eq_irreducibleSpectrum_of_faithful_representation pi hpi hfaith hnormal214215end MathlibAnnex.Analysis.CStarAlgebra