MathlibAnnex/Analysis/CStarAlgebra/Spectrum/Primitive.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.Representatives78/-!9# The primitive spectrum as a family of actual representation kernels1011A point is an actual subset of A occurring as a pure-state GNS kernel. The12arbitrary-universe coverage theorem shows this is exactly the family of all13nonzero irreducible representation kernels. `toTwoSidedIdeal` proves and14exposes the algebraic ideal, rather than storing unproved ideal properties.15This definition is independent of the geometric primitive spectrum.16-/1718set_option autoImplicit false19noncomputable section20open Set2122namespace MathlibAnnex.Analysis.CStarAlgebra2324universe u v25variable (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]26open NonUnitalCStarRepresentation2728/-- A small list of the actual irreducible representation-kernel carriers. -/29def primitiveKernelFamily : Set (Set A) :=30  Set.range fun phi : NonUnitalPureState A => (kernelIdeal phi.gnsRepresentation : Set A)3132/-- Actual primitive ideal carriers, not geometric primitive-spectrum points. -/33def PrimitiveSpectrum := {P : Set A // P ∈ primitiveKernelFamily A}3435namespace PrimitiveSpectrum36variable {A}3738/-- The primitive kernel of the actual GNS representation of a pure state. -/39def ofPureState (phi : NonUnitalPureState A) : PrimitiveSpectrum A :=40  ⟨(kernelIdeal phi.gnsRepresentation : Set A), phi, rfl⟩4142theorem ofPureState_surjective : Function.Surjective (ofPureState (A := A)) := by43  rintro ⟨P, phi, hphi⟩44  exact ⟨phi, Subtype.ext hphi⟩4546/-- An actual ideal underlying a primitive point; the subsequent carrier47identity makes this independent of the selected GNS witness. -/48def toTwoSidedIdeal (P : PrimitiveSpectrum A) : TwoSidedIdeal A :=49  kernelIdeal P.property.choose.gnsRepresentation5051@[simp]52theorem coe_toTwoSidedIdeal (P : PrimitiveSpectrum A) :53    (P.toTwoSidedIdeal : Set A) = P.val := P.property.choose_spec5455@[simp]56theorem mem_toTwoSidedIdeal (P : PrimitiveSpectrum A) (a : A) :57    a ∈ P.toTwoSidedIdeal ↔ a ∈ P.val := by58  rw [← P.coe_toTwoSidedIdeal]59  rfl6061theorem toTwoSidedIdeal_ofPureState (phi : NonUnitalPureState A) :62    (ofPureState phi).toTwoSidedIdeal = kernelIdeal phi.gnsRepresentation := by63  apply SetLike.coe_injective64  exact coe_toTwoSidedIdeal (ofPureState phi)6566theorem toTwoSidedIdeal_ne_top (P : PrimitiveSpectrum A) : P.toTwoSidedIdeal ≠ ⊤ :=67  kernelIdeal_ne_top _ P.property.choose.isIrreducible_gnsRepresentation.16869theorem val_ne_univ (P : PrimitiveSpectrum A) : P.val ≠ Set.univ := by70  intro h71  apply P.toTwoSidedIdeal_ne_top72  apply SetLike.coe_injective73  rw [P.coe_toTwoSidedIdeal, h, TwoSidedIdeal.coe_top]7475theorem isClosed_val (P : PrimitiveSpectrum A) : IsClosed P.val := by76  rw [← P.coe_toTwoSidedIdeal]77  exact isClosed_kernelIdeal _7879theorem star_mem_val_iff (P : PrimitiveSpectrum A) (a : A) :80    star a ∈ P.val ↔ a ∈ P.val := by81  rw [← P.coe_toTwoSidedIdeal]82  exact star_mem_kernelIdeal_iff _ a8384theorem smul_mem_val (P : PrimitiveSpectrum A) (c : ℂ) {a : A} (ha : a ∈ P.val) :85    c • a ∈ P.val := by86  rw [← P.coe_toTwoSidedIdeal] at ha ⊢87  exact smul_mem_kernelIdeal _ c ha8889/-- Meet-primality is proved, not a field in the primitive-point definition. -/90theorem inf_le_toTwoSidedIdeal_iff (P : PrimitiveSpectrum A) (I J : TwoSidedIdeal A) :91    I ⊓ J ≤ P.toTwoSidedIdeal ↔ I ≤ P.toTwoSidedIdeal ∨ J ≤ P.toTwoSidedIdeal :=92  inf_le_kernelIdeal_iff _ P.property.choose.isIrreducible_gnsRepresentation I J9394/-- Any arbitrary-Hilbert-universe nonzero irreducible representation gives95an actual point of this primitive spectrum. -/96def ofRepresentation {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H]97    [CompleteSpace H] (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) :98    PrimitiveSpectrum A := by99  refine ⟨(kernelIdeal pi : Set A), ?_⟩100  obtain ⟨phi, hphi⟩ := exists_pureState_kernelIdeal_eq pi hpi101  exact ⟨phi, congrArg SetLike.coe hphi.symm⟩102103@[simp]104theorem ofRepresentation_val {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H]105    [CompleteSpace H] (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) :106    (ofRepresentation pi hpi).val = (kernelIdeal pi : Set A) := rfl107108end PrimitiveSpectrum109110/-- No primitive ideal is the whole original algebra, including in the empty case. -/111theorem univ_notMem_primitiveKernelFamily : Set.univ ∉ primitiveKernelFamily A := by112  intro h113  exact (PrimitiveSpectrum.val_ne_univ (⟨Set.univ, h⟩ : PrimitiveSpectrum A)) rfl114115namespace IrreducibleSpectrum116variable {A}117118/-- The representation-kernel map kappa. Equivalent GNS models have equal119kernels, but its converse and injectivity are neither used nor asserted. -/120def kernel (q : IrreducibleSpectrum A) : PrimitiveSpectrum A :=121  Quotient.lift PrimitiveSpectrum.ofPureState122    (fun phi psi h => Subtype.ext (congrArg (fun I : TwoSidedIdeal A => (I : Set A))123      (NonUnitalCStarRepresentation.UnitaryEquivalent.kernelIdeal_eq h))) q124125@[simp]126theorem kernel_ofPureState (phi : NonUnitalPureState A) :127    kernel (ofPureState phi) = PrimitiveSpectrum.ofPureState phi := rfl128129/-- The abstract kernel map agrees with the concrete arbitrary-universe action. -/130theorem kernel_ofRepresentation {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H]131    [CompleteSpace H] (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) :132    kernel (ofRepresentation pi hpi) = PrimitiveSpectrum.ofRepresentation pi hpi := by133  apply Subtype.ext134  exact congrArg (fun I : TwoSidedIdeal A => (I : Set A))135    (exists_pureState_unitaryEquivalent_gnsRepresentation pi hpi).choose_spec.kernelIdeal_eq.symm136137theorem kernel_surjective : Function.Surjective (kernel (A := A)) := by138  intro P139  obtain ⟨phi, rfl⟩ := PrimitiveSpectrum.ofPureState_surjective P140  exact ⟨ofPureState phi, rfl⟩141142end IrreducibleSpectrum143end MathlibAnnex.Analysis.CStarAlgebra