MathlibAnnex.Analysis.CStarAlgebra.primitiveKernelFamily_eq_primitiveGeometricSpectrumFamily
theorem
Identifies primitive representation kernels with intersections of geometric components.
Statement
Let be a complex C*-algebra, possibly without an identity. A pure state is a positive norm-one bounded complex-linear functional on that is extreme in the state space for real convexity. For a pure state , let be the representation of obtained by restricting the GNS representation of its canonical state extension to the forced unitization. The independently defined primitive-kernel family is
Let be the geometric structure space, whose points are kernels of bounded complex-linear functionals that are extreme points, for real convexity, of the entire closed dual unit ball by the extreme-kernel theorem, with the hull–kernel closure . Let be its finite-chain components (chains of equal points or nonclosed pairs), and put . The primitive geometric family is . Then
Here both and are treated as families of subsets of .
Assumptions
The source uses a nonzero complex C*-algebra with its compatible order. The family is constructed from the pure-state GNS representations independently of geometric components. The compared objects are families of subsets of this same algebra; no additional representation or component is an input.
Conclusion
The equality identifies precisely which subsets occur. It does not identify an individual component with its intersection. No injectivity of the representation-kernel map or of is asserted. The primitive-spectrum homeomorphism is a separate construction using this family equality.
Main citations
- Exact family equality:
primitiveKernelFamily_eq_primitiveGeometricSpectrumFamily. - Pure-state component representative and pure-state component intersection: the related representative and same-state intersection statements.
- Independent primitive family and geometric component-intersection family: the definitions compared here.
Lean source signature (exact)
The declaration prefix below is a contiguous source excerpt, ending before its proof assignment.
theorem primitiveKernelFamily_eq_primitiveGeometricSpectrumFamily :
primitiveKernelFamily A = NormedSpace.primitiveGeometricSpectrumFamily ℂ A
| In the source | Mathematical meaning |
|---|---|
Exact declaration(A : Type u) and its nonunital C*-algebra, order and nontriviality instances |
The same nonzero complex C*-algebra underlies both independently defined families. No extra representation is an input to this declaration. |
Exact declarationprimitiveKernelFamily A |
Kernels for pure states , forming the family of subsets of . |
Exact declarationNormedSpace.primitiveGeometricSpectrumFamily ℂ A |
The family of intersections of all GSS points in a component. It is not the family of the component subsets themselves. |
| The complete equalityExact declaration | Every member of either family is a member of the other, as the same subset of . This compares representation kernels with whole-component intersections, not components with individual functional kernels. |
Exact surrounding source context (separate excerpts)
Source lines 27–27:
variable (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
Source lines 28–28:
variable [Nontrivial A]
Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·