Every geometric-spectrum component contains a pure-state kernel

MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_kernel_mem_geometricSpectrum

theorem

Places the kernel of a pure state in every geometric-spectrum component.

Statement

Let be a complex C*-algebra, possibly without an identity. Its geometric structure space consists of kernels of bounded complex-linear functionals that are extreme points, for real convexity, of the entire closed dual unit ball , as stated by the extreme-kernel identification, with closure

c_A(\mathcal T)=\left\{I\in S(A):\bigcap_{J\in\mathcal T}J\subseteq I\right\}.

Two points are linked if they are equal or their pair is not closed. Their finite-chain equivalence classes are the components. A point of the geometric spectrum is one such component subset of .

For every there is a pure state of such that

\ker\varphi\in C. \tag{1}

Here is a point of : the pure-state extremality theorem guarantees that is extreme in the entire closed dual unit ball.

Assumptions

The source fixes a nonzero complex C*-algebra and its compatible order. The component is arbitrary; it need not be presented initially by a functional or representation. A pure state is a positive norm-one bounded complex-linear functional , extreme among positive norm-one functionals for real convexity. The geometric spectrum consists of component sets, so (1) places a functional kernel, rather than a functional, in .

Conclusion

The theorem produces one state together with its purity and the membership of that same state's kernel in the specified component. It does not identify with the intersection of all points of ; that intersection is determined in the component-kernel identity.

Main citations

Exact component representative theorem: exists_pureState_kernel_mem_geometricSpectrum.
Ryotaro Tanaka, arXiv:2504.05551v1, Corollary 5.9: the component representative assertion, read with the type-correct pure-state kernel.

Lean source signature (exact)

The declaration prefix below is a contiguous source excerpt, ending before its proof assignment.

theorem exists_pureState_kernel_mem_geometricSpectrum (C : NormedSpace.GeometricSpectrum ℂ A) :
    ∃ (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi),
      extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩ ∈ C.val

Back to the reading-guide item

In the source	Mathematical meaning
Algebra and order`variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A] variable [PartialOrder A] [StarOrderedRing A]`Fixed source	The nonzero complex C*-algebra and its compatible order support the pure-state and geometric-point constructions.
Specified component`theorem exists_pureState_kernel_mem_geometricSpectrum (C : NormedSpace.GeometricSpectrum ℂ A) :`Fixed source	The input is a component subset of , not an individual functional or representation.
Pure state`∃ (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi),`Fixed source	There is a bounded complex-linear functional which is a pure state: positive, of norm one, and extreme among states for real convexity.
Kernel point in that component`extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩ ∈ C.val := by`Fixed source	The extremality result applied to this same certifies as a point of . The full conclusion is $\ker\varphi\in C.$ The projection of is its component subset, so the membership places the kernel point in the originally specified component.
Components as geometric-spectrum points`def GeometricSpectrum : Type u := {C : Set (GeometricStructureSpace 𝕜 E) // C ∈ geometricSpectrumFamily 𝕜 E}`Fixed source	A geometric-spectrum point is a component subset of with its component membership. Its underlying set is the used in (1).

Exact surrounding source context (separate excerpts)

Exact surrounding source:

variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]

Back to the reading-guide item

Exact surrounding source:

variable [PartialOrder A] [StarOrderedRing A]

Back to the reading-guide item

Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·

Technical documentation