MathlibAnnex.Analysis.CStarAlgebra.exists_forall_eq_irreducibleSpectrum_iff_exists_faithful_representation
theorem
Characterizes a singleton irreducible spectrum by one faithful representation with a full normal part.
Statement
Let be a nonzero complex -algebra, not necessarily unital, with the compatible order structure used in its pure-state construction. Write for its irreducible spectrum: the space of unitary-equivalence classes of irreducible representations, realized here through pure-state GNS representations. It is not the space of primitive ideals obtained by identifying representations with the same kernel.
For a nonzero irreducible -representation on a complex Hilbert space , write for the geometric structure of its image , whose points are subsets obtained as unions of supporting kernels for maximal proper real faces of the closed unit ball. The established -algebra identification realizes these points as kernels of extreme norm-one functionals. Use the inner product linear in its second variable. For , define the bounded linear functional by . Its normal part consists of these coefficient kernels
The following are equivalent:
(i) The irreducible spectrum has exactly one point.
(ii) There are a complex Hilbert space and a nonzero irreducible -representation such that
The same Hilbert space and representation satisfy all the conditions in (ii).
Assumptions
The algebra is nontrivial. There is no separability, unitality, finite-dimensionality, or prescribed Hilbert space in the input. Irreducibility on the right includes a nonzero action; it is not a convention that permits the zero representation. The order and star-order structures in the ambient source are retained. No full-normal-part or faithfulness assumption is hidden in a newly defined representation object.
Here “fully normal” means exactly the equality of sets of geometric points in (ii). It is not a claim about normal functionals on a von Neumann algebra, nor about the ultraweak continuity of .
Conclusion
A singleton unitary-equivalence spectrum is equivalent to the simultaneous existence of faithfulness and a full normal part for one nonzero irreducible representation. Neither condition alone replaces their conjunction. No elementary-algebra classification is asserted here.
Main citations
The singleton-spectrum representation theorem gives the equivalence of (i) and (ii). The pure-state witness theorem supplies one faithful GNS representation with full normal part; the converse for a given representation applies to the same representation in (ii).
Lean source signature (exact)
The preceding variable declarations supply the nonzero C*-algebra and its order assumptions. On the right of ↔, the nested existentials choose one complex Hilbert space and one representation on it. The norm, inner product and completeness all belong to that same space; the local letI declarations make these structures available together. The three final conjuncts concern that same representation. The following contiguous prefix ends before the proof assignment.
theorem exists_forall_eq_irreducibleSpectrum_iff_exists_faithful_representation : (∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q) ↔ (∃ (H' : Type u) (instN : NormedAddCommGroup H'), letI := instN ∃ instI : InnerProductSpace ℂ H', letI := instI ∃ instC : CompleteSpace H', letI := instC ∃ pi : NonUnitalCStarRepresentation A H', pi.IsIrreducible ∧ Function.Injective pi ∧ normalPart (NonUnitalStarAlgHom.range pi) = Set.univ)Back to the reading-guide item
| In the source | Mathematical meaning |
|---|---|
Nonzero algebra and compatible ordervariable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]
variable [PartialOrder A] [StarOrderedRing A]Fixed source | The input is the nonzero complex C*-algebra . The partial order and star-order structure are those used for positivity and pure states. Unitality and separability are not required. |
A singleton irreducible spectrum(∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q) ↔Fixed source | The left side says that has exactly one point, including existence of that point. Its points are unitary-equivalence classes of irreducible representations; this is not a statement that their kernels alone coincide. |
One Hilbert space and one representation(∃ (H' : Type u) (instN : NormedAddCommGroup H'),
letI := instN
∃ instI : InnerProductSpace ℂ H',
letI := instI
∃ instC : CompleteSpace H',
letI := instC
∃ pi : NonUnitalCStarRepresentation A H',Fixed source | One complex Hilbert space is chosen, with its norm, compatible inner product and completeness. One -representation is then chosen on this same space. All conditions in the next row concern this same . |
Irreducibility, faithfulness, and the full normal partpi.IsIrreducible ∧ Function.Injective pi ∧ normalPart (NonUnitalStarAlgHom.range pi) = Set.univ) := byFixed source | The representation is nonzero and irreducible, is faithful, and has full normal part: The latter equality is with the whole geometric structure space of its image , not with the operator algebra . |
Coefficient kernels in the image algebradef normalPart (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)) :
Set (NormedSpace.GeometricStructureSpace ℂ S) :=
{I | ∃ x y : H, x ≠ 0 ∧ y ≠ 0 ∧
{a : S | inner ℂ y ((a : H →L[ℂ] H) x) = 0} = I.val}Fixed source | Apply the definition to the image algebra . Its normal part consists of the coefficient kernels where is given by , as in (1). The kernel is identified with the underlying subset of the geometric point . |
Exact surrounding source context (separate excerpts)
universe u v variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A] variable [PartialOrder A] [StarOrderedRing A]Back to the reading-guide item
The existential Hilbert space has source level u, the same fixed level as . The separate ambient level v does not enlarge this theorem's model quantifier.
Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·