MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralComparison.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.Spectrum.Primitive7import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.AbsoluteState89/-!10# Independent spectral objects and their geometric comparison maps1112Phi sends the unitary-equivalence class of an actual pure-state GNS action13to the component of that state's functional kernel. Psi retains the actual14primitive-ideal carrier. Their bijectivity is proved from the previously15established component representation and J_C identities. Neither source16spectrum is defined as an alias of, or transported from, a geometric spectrum.17No injectivity of kappa or gamma is assumed.18-/1920set_option autoImplicit false21noncomputable section22open Set2324namespace MathlibAnnex.Analysis.CStarAlgebra2526universe u v27variable (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]28variable [Nontrivial A]29open NonUnitalCStarRepresentation3031namespace NonUnitalPureState32variable {A}3334/-- The functional kernel, as a point of the original general Banach GSS. -/35def geometricPoint (phi : NonUnitalPureState A) : NormedSpace.GeometricStructureSpace ℂ A :=36  extremeKernel ⟨phi.val, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState37    phi.val phi.property⟩3839/-- This point is exactly the canonical GNS vector-coefficient kernel. -/40theorem geometricPoint_eq_matrixCoefficientKernel (phi : NonUnitalPureState A) :41    phi.geometricPoint = matrixCoefficientKernel phi.gnsRepresentation42      phi.isIrreducible_gnsRepresentation phi.gnsVector phi.gnsVector43      phi.gnsVector_ne_zero phi.gnsVector_ne_zero := by44  apply Subtype.ext45  change (phi.val.ker : Set A) =46    ((matrixCoefficient phi.gnsRepresentation phi.gnsVector phi.gnsVector).ker : Set A)47  rw [phi.matrixCoefficient_gnsRepresentation]4849/-- The actual component attached to a pure-state representation. -/50def toGeometricSpectrum (phi : NonUnitalPureState A) : NormedSpace.GeometricSpectrum ℂ A :=51  NormedSpace.toGeometricSpectrum ℂ A phi.geometricPoint5253/-- Paper 5.8, with actual GNS equivalence, makes the comparison well-defined54and injective on the quotient. Functional-kernel equality is not the relation used. -/55theorem toGeometricSpectrum_eq_iff (phi psi : NonUnitalPureState A) :56    phi.toGeometricSpectrum = psi.toGeometricSpectrum ↔57      phi.gnsRepresentation.UnitaryEquivalent psi.gnsRepresentation := by58  change (NormedSpace.geometricStructureClosure ℂ A).toComponentPoint phi.geometricPoint =59    (NormedSpace.geometricStructureClosure ℂ A).toComponentPoint psi.geometricPoint ↔ _60  rw [ClosureSpace.toComponentPoint_eq_iff, phi.geometricPoint_eq_matrixCoefficientKernel,61    psi.geometricPoint_eq_matrixCoefficientKernel]62  exact related_matrixCoefficientKernel_iff_unitaryEquivalent63    phi.gnsRepresentation psi.gnsRepresentation64    phi.isIrreducible_gnsRepresentation psi.isIrreducible_gnsRepresentation65    phi.gnsVector phi.gnsVector psi.gnsVector psi.gnsVector66    phi.gnsVector_ne_zero phi.gnsVector_ne_zero psi.gnsVector_ne_zero psi.gnsVector_ne_zero6768/-- Every component contains a pure-state kernel, by the actual absolute-state construction. -/69theorem toGeometricSpectrum_surjective :70    Function.Surjective (toGeometricSpectrum (A := A)) := by71  intro C72  obtain ⟨rho, rfl⟩ := exists_toGeometricSpectrum_extremeKernel_eq C73  let phi : NonUnitalPureState A :=74    ⟨extremeAbsoluteState rho, isPureNonUnitalState_extremeAbsoluteState rho⟩75  refine ⟨phi, ?_⟩76  apply (ClosureSpace.toComponentPoint_eq_iff _ _ _).277  exact (NormedSpace.geometricStructureClosure ℂ A).related_symm78    (related_extremeKernel_extremeAbsoluteState rho)7980/-- The whole-component theorem, not a one-sided family inclusion, supplies J_C. -/81theorem geometricSpectrumToPrimitive_toGeometricSpectrum_val (phi : NonUnitalPureState A) :82    (NormedSpace.geometricSpectrumToPrimitive ℂ A phi.toGeometricSpectrum).val =83      (kernelIdeal phi.gnsRepresentation : Set A) := by84  rw [coe_kernelIdeal_eq_ker]85  exact geometricSpectrumToPrimitive_toGeometricSpectrum_pureStateKernel_val phi.val phi.property8687end NonUnitalPureState8889namespace IrreducibleSpectrum90variable {A}9192/-- Phi is quotient elimination through the proved GNS-equivalence criterion. -/93def toGeometricSpectrum (q : IrreducibleSpectrum A) : NormedSpace.GeometricSpectrum ℂ A :=94  Quotient.lift NonUnitalPureState.toGeometricSpectrum95    (fun phi psi h => (phi.toGeometricSpectrum_eq_iff psi).2 h) q9697@[simp]98theorem toGeometricSpectrum_ofPureState (phi : NonUnitalPureState A) :99    toGeometricSpectrum (ofPureState phi) = phi.toGeometricSpectrum := rfl100101theorem toGeometricSpectrum_bijective : Function.Bijective (toGeometricSpectrum (A := A)) := by102  constructor103  · intro q r104    refine Quotient.inductionOn₂ q r ?_105    intro phi psi h106    exact Quotient.sound ((phi.toGeometricSpectrum_eq_iff psi).1 h)107  · intro C108    obtain ⟨phi, rfl⟩ := NonUnitalPureState.toGeometricSpectrum_surjective C109    exact ⟨ofPureState phi, rfl⟩110111/-- Phi on an arbitrary represented Hilbert space, with the requested112component formula for every nonzero coefficient pair. -/113theorem toGeometricSpectrum_ofRepresentation114    {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]115    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)116    (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) :117    toGeometricSpectrum (ofRepresentation pi hpi) =118      NormedSpace.toGeometricSpectrum ℂ A (matrixCoefficientKernel pi hpi x y hx hy) := by119  let phi := (exists_pureState_unitaryEquivalent_gnsRepresentation pi hpi).choose120  have hphi : pi.UnitaryEquivalent phi.gnsRepresentation :=121    (exists_pureState_unitaryEquivalent_gnsRepresentation pi hpi).choose_spec122  change NormedSpace.toGeometricSpectrum ℂ A phi.geometricPoint = _123  rw [phi.geometricPoint_eq_matrixCoefficientKernel]124  apply (ClosureSpace.toComponentPoint_eq_iff _ _ _).2125  exact (related_matrixCoefficientKernel_iff_unitaryEquivalent126    phi.gnsRepresentation pi phi.isIrreducible_gnsRepresentation hpi127    phi.gnsVector phi.gnsVector x y128    phi.gnsVector_ne_zero phi.gnsVector_ne_zero hx hy).2 hphi.symm129130/-- The bijection underlying Phi, before any topological conclusion. -/131def equivGeometricSpectrum : IrreducibleSpectrum A ≃ NormedSpace.GeometricSpectrum ℂ A :=132  Equiv.ofBijective toGeometricSpectrum toGeometricSpectrum_bijective133134@[simp]135theorem equivGeometricSpectrum_ofPureState (phi : NonUnitalPureState A) :136    equivGeometricSpectrum (ofPureState phi) = phi.toGeometricSpectrum := rfl137138end IrreducibleSpectrum139140/-- Independently defined primitive kernels and geometric component intersections141are the same family of subsets of the original A. -/142theorem primitiveKernelFamily_eq_primitiveGeometricSpectrumFamily :143    primitiveKernelFamily A = NormedSpace.primitiveGeometricSpectrumFamily ℂ A := by144  ext P145  constructor146  · rintro ⟨phi, rfl⟩147    have h := (NormedSpace.geometricSpectrumToPrimitive ℂ A phi.toGeometricSpectrum).property148    rw [phi.geometricSpectrumToPrimitive_toGeometricSpectrum_val] at h149    exact h150  · intro hP151    let J : NormedSpace.PrimitiveGeometricSpectrum ℂ A := ⟨P, hP⟩152    obtain ⟨C, hC⟩ := NormedSpace.geometricSpectrumToPrimitive_surjective ℂ A J153    obtain ⟨phi, hphi⟩ := NonUnitalPureState.toGeometricSpectrum_surjective C154    refine ⟨phi, ?_⟩155    calc156      (kernelIdeal phi.gnsRepresentation : Set A) =157          (NormedSpace.geometricSpectrumToPrimitive ℂ A phi.toGeometricSpectrum).val :=158        phi.geometricSpectrumToPrimitive_toGeometricSpectrum_val.symm159      _ = P := by rw [hphi, hC]160161/-- Psi retains primitive-ideal carriers, with family membership justified by162an actual theorem rather than a definition of Prim in terms of PS. -/163def primitiveSpectrumEquivGeometric : PrimitiveSpectrum A ≃ NormedSpace.PrimitiveGeometricSpectrum ℂ A where164  toFun P := ⟨P.val, (primitiveKernelFamily_eq_primitiveGeometricSpectrumFamily A) ▸ P.property⟩165  invFun J := ⟨J.val, (primitiveKernelFamily_eq_primitiveGeometricSpectrumFamily A).symm ▸ J.property⟩166  left_inv _ := Subtype.ext rfl167  right_inv _ := Subtype.ext rfl168169@[simp]170theorem primitiveSpectrumEquivGeometric_val (P : PrimitiveSpectrum A) :171    (primitiveSpectrumEquivGeometric A P).val = P.val := rfl172173@[simp]174theorem primitiveSpectrumEquivGeometric_symm_val (J : NormedSpace.PrimitiveGeometricSpectrum ℂ A) :175    ((primitiveSpectrumEquivGeometric A).symm J).val = J.val := rfl176177/-- The requested square, on actual points: Psi(kappa(q)) = gamma(Phi(q)). -/178theorem primitiveSpectrumEquivGeometric_kernel (q : IrreducibleSpectrum A) :179    primitiveSpectrumEquivGeometric A (IrreducibleSpectrum.kernel q) =180      NormedSpace.geometricSpectrumToPrimitive ℂ A (IrreducibleSpectrum.equivGeometricSpectrum q) := by181  refine Quotient.inductionOn q ?_182  intro phi183  apply Subtype.ext184  exact phi.geometricSpectrumToPrimitive_toGeometricSpectrum_val.symm185186/-- Function-level square; neither vertical map is assumed injective. -/187theorem primitiveSpectrumEquivGeometric_comp_kernel :188    primitiveSpectrumEquivGeometric A ∘ IrreducibleSpectrum.kernel =189      NormedSpace.geometricSpectrumToPrimitive ℂ A ∘ IrreducibleSpectrum.equivGeometricSpectrum :=190  funext (primitiveSpectrumEquivGeometric_kernel A)191192/-- The actual carrier relation used in the independent closure comparison. -/193theorem geometricSpectrumKernel_equivGeometricSpectrum (q : IrreducibleSpectrum A) :194    NormedSpace.geometricSpectrumKernel ℂ A (IrreducibleSpectrum.equivGeometricSpectrum q) =195      (IrreducibleSpectrum.kernel q).val :=196  (congrArg Subtype.val (primitiveSpectrumEquivGeometric_kernel A q)).symm197198end MathlibAnnex.Analysis.CStarAlgebra