MathlibAnnex/Analysis/CStarAlgebra/Spectrum/PrimitiveRepresentative.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-/67import MathlibAnnex.Analysis.CStarAlgebra.Spectrum.Primitive89/-!10# Chosen pure-state representatives of primitive-spectrum points1112Each actual primitive point stores the existence of a pure-state GNS kernel.13This module exposes one chosen representative and its exact kernel carrier.14-/1516@[expose] public section1718set_option autoImplicit false19noncomputable section2021open Set22open scoped CStarAlgebra2324namespace MathlibAnnex.Analysis.CStarAlgebra2526universe u2728variable {A : Type u} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]2930namespace PrimitiveSpectrum3132/-- The pure-state GNS representative stored by an actual primitive point. -/33def pureStateRepresentative (P : PrimitiveSpectrum A) : NonUnitalPureState A :=34  P.property.choose3536@[simp]37theorem kernelIdeal_pureStateRepresentative (P : PrimitiveSpectrum A) :38    NonUnitalCStarRepresentation.kernelIdeal P.pureStateRepresentative.gnsRepresentation =39      P.toTwoSidedIdeal := rfl4041@[simp]42theorem coe_kernelIdeal_pureStateRepresentative (P : PrimitiveSpectrum A) :43    (NonUnitalCStarRepresentation.kernelIdeal44      P.pureStateRepresentative.gnsRepresentation : Set A) = P.val := by45  rw [kernelIdeal_pureStateRepresentative, coe_toTwoSidedIdeal]4647end PrimitiveSpectrum4849end MathlibAnnex.Analysis.CStarAlgebra