MathlibAnnex.Analysis.CStarAlgebra.geometricSpectrumToPrimitive_toGeometricSpectrum_pureStateKernel_val
theorem
Identifies a pure-state component intersection with the kernel of its GNS representation.
Statement
Let be a complex C*-algebra, possibly without an identity. A state on is a positive bounded complex-linear functional of norm one. It is pure if it is an extreme point of the state space, regarded as a real convex set. Let be a pure state. Let be the GNS model of its canonical state extension to the forced unitization , and let .
By the extreme-kernel theorem, is the family of kernels of bounded complex-linear functionals that are extreme points, for real convexity, of the entire closed dual unit ball , with closure . The pure-state kernel is one such point, by the pure-state extremality theorem. Let denote its component for the finite-chain relation generated by equal points and nonclosed pairs. Write for the set of these components. For a component , put , and write for the family of all such intersections. The canonical map is
Then, as subsets of the original algebra,
On the left we display the underlying subset of the primitive geometric point.
Assumptions
The given functional is positive, has norm one, and is extreme in the state space for real convexity; carries its compatible C*-order. The GNS action is formed from this very state's canonical extension. The representation is fixed by ; faithfulness is not assumed.
Conclusion
The whole component's intersection is the representation kernel , using this fixed GNS representation. An individual functional kernel need not equal that intersection. Formula (1) is an equality of subsets; it gives neither injectivity of nor a comparison of topologies by itself.
Main citations
- Exact pure-state gamma identity:
geometricSpectrumToPrimitive_toGeometricSpectrum_pureStateKernel_val. - Component intersections, their family and the component-intersection map: the definitions of , and .
- Ryotaro Tanaka, arXiv:2504.05551v1, Lemma 5.10: the component-family and representation-kernel comparison.
Lean source signature (exact)
The declaration prefix below is a contiguous source excerpt, ending before its proof assignment.
theorem geometricSpectrumToPrimitive_toGeometricSpectrum_pureStateKernel_val (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi) : (NormedSpace.geometricSpectrumToPrimitive ℂ A (NormedSpace.toGeometricSpectrum ℂ A (extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩))).val = ((absoluteStateContinuousMap (NonUnitalStateGNS.representation phi hpure.1)).ker : Set A)Back to the reading-guide item
| In the source | Mathematical meaning |
|---|---|
Algebra and ordervariable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]
variable [PartialOrder A] [StarOrderedRing A]Fixed source | The nonzero complex C*-algebra and its compatible order are fixed. |
Given pure state(phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi) :Fixed source | The given is a positive bounded complex-linear functional of norm one, extreme in the state space for real convexity. This same state determines the GNS model. |
Kernel, component and its intersection(NormedSpace.geometricSpectrumToPrimitive ℂ A
(NormedSpace.toGeometricSpectrum ℂ A
(extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩))).val =Fixed source | The innermost input is the geometric point , with its extremality certificate. Sending it to its component gives . Applying and taking the underlying subset gives The nested applications act on this same point in that order. |
The component mapdef toGeometricSpectrum (I : GeometricStructureSpace 𝕜 E) : GeometricSpectrum 𝕜 E :=
(geometricStructureClosure 𝕜 E).toComponentPoint IFixed source | This map sends a point to its entire finite-chain component. In the preceding application, . |
The intersection mapdef geometricSpectrumToPrimitive : GeometricSpectrum 𝕜 E → PrimitiveGeometricSpectrum 𝕜 E :=
ClosureSpace.HullKernel.componentPointToComponentKernelPoint
(geometricStructureFamily 𝕜 E) (univ_notMem_geometricStructureFamily 𝕜 E)Fixed source | This is , sending a component to . Its value is a subset of the algebra, rather than a subset of . |
Kernel of the same GNS representation((absoluteStateContinuousMap (NonUnitalStateGNS.representation phi hpure.1)).ker : Set A) := byFixed source | The right side is . The GNS action is formed from the canonical extension of this same state, and the continuous-linear-map wrapper changes no values. Thus (1) identifies the whole component intersection with the representation kernel, not with the individual functional kernel. |
Operator-valued linear mapprivate def absoluteStateContinuousMap {H : Type v}
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
(pi : NonUnitalCStarRepresentation A H) : A →L[ℂ] (H →L[ℂ] H) :=
LinearMap.mkContinuous
{ toFun := pi, map_add' := map_add pi, map_smul' := map_smul pi }Fixed source | The wrapper has domain and codomain . Its function is the given representation , with the same addition and complex-scalar action. It supplies the operator-valued map whose kernel appears on the right of (1). |
Exact surrounding source context (separate excerpts)
Exact surrounding source:
variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]
Back to the reading-guide itemExact surrounding source:
variable [PartialOrder A] [StarOrderedRing A]
Back to the reading-guide itemThe continuous-map wrapper in the same source is copied separately; its forward function is the given action; the continuous-map constructor receives the existing contractive bound:
private def absoluteStateContinuousMap {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (pi : NonUnitalCStarRepresentation A H) : A →L[ℂ] (H →L[ℂ] H) := LinearMap.mkContinuous { toFun := pi, map_add' := map_add pi, map_smul' := map_smul pi } 1 (fun a => by change ‖pi a‖ ≤ 1 * ‖a‖ simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le pi a)Back to the reading-guide item
Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·