Elementary C*-algebras from singleton spectrum and finite conjugation

MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_compactOperatorModel_iff_singleton_finiteConjugation

theorem

Characterizes a pure-GNS compact model by singleton spectrum and continuous finite conjugation.

Statement

Let be a nonzero complex C*-algebra with its compatible order. Write for its irreducible spectrum, the pure states modulo unitary equivalence of their GNS representations, and for its geometric structure closure space. For , let be its finite-chain component, with the closure induced from . For a complex Hilbert space , let denote the algebra of compact operators on .

The following conditions are equivalent.

There is a pure state of whose GNS representation is faithful and satisfies

\pi_\varphi(A)=\mathcal K(H_\varphi).\tag{1}

The irreducible spectrum is a singleton, and there is a point whose component satisfies the conjugation condition below.

For a closure space , write for its closure operator. For the geometric structure spaces and , abbreviate these operators to and , respectively. Write for the image of a subset under a map . The condition concerns every closure space that is homeomorphic to for some nonzero complex C*-algebra . Here is the same geometric structure construction used for . A homeomorphism is a bijection preserving closure on every subset:

r\bigl(c_B(E)\bigr) =c_X\bigl(r(E)\bigr) \qquad(E\subseteq S(B)).

The algebra may vary; no unit, separability assumption or chosen representation of is part of this condition.

For every such , consider each of its finite-chain components , with the induced closure for , and all bijections

f:D\longrightarrow C_A(I),\qquad g:D\longrightarrow D.

A finite-chain component consists of points joined by a finite chain of linked pairs. Two points are linked if they are equal or their two-point set is not closed. These components are taken in the specified closure space, not as connected components of a topology.

A bijection of closure spaces is a finite homeomorphism if it preserves closure on every finite subset:

r\bigl(c_Y(F)\bigr) =c_Z\bigl(r(F)\bigr) \qquad(F\subseteq Y\text{ finite}).\tag{2}

A map is continuous if

r\bigl(c_Y(E)\bigr) \subseteq c_Z\bigl(r(E)\bigr) \qquad(E\subseteq Y).\tag{3}

The required condition is that whenever and are finite homeomorphisms and are also continuous in the sense of (3), transporting to by gives a homeomorphism. More explicitly, both

\begin{aligned} h&=f\circ g\circ f^{-1},\\ h^{-1}&=f\circ g^{-1}\circ f^{-1} \end{aligned} \qquad:C_A(I)\longrightarrow C_A(I)\tag{4}

must be continuous on arbitrary subsets. This is required for every , every component and every pair described above. Continuity of or on arbitrary subsets is not assumed. The inverses in (4) are those of the same bijections and .

Assumptions

is a nonzero complex C*-algebra with its compatible order. It need not be unital or separable, and no finite-dimensionality assumption is imposed. The geometric condition requires both a singleton irreducible spectrum and the existence of ; neither condition is interpreted vacuously. The source guide records the fixed size bounds for the spaces in the conjugation condition.

Conclusion

The two geometric conditions characterize the existence of a pure state whose faithful GNS representation identifies , as a C*-algebra, with . The Hilbert space and representation in this identification are those of the same state in (1).

Main citations

The compact-model characterization states this equivalence in every Hilbert dimension. Its two directions use the existence of a compact-operator model and the conjugation property of compact-operator models. The conjugation condition specifies the inputs and the two continuous maps in (4); the realization of closure spaces by C*-algebras specifies the spaces . The conjugate and its inverse act by the formulas in (4).

Lean source signature (exact)

The preceding variable declarations supply A and its algebra and order structures; [Nontrivial A] appears explicitly in the theorem. The outer ↔ compares the GNS-model condition with a conjunction ∧: a singleton irreducible spectrum and the existence of a geometric point I with the component condition. The following is the contiguous prefix of the selected declaration, ending before the proof assignment.

theorem exists_pureState_compactOperatorModel_iff_singleton_finiteConjugation
    [Nontrivial A] :
    (∃ phi : NonUnitalPureState A, IsCompactOperatorModel phi.gnsRepresentation) ↔
      (∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q) ∧
      ∃ I : NormedSpace.GeometricStructureSpace ℂ A,
        ((NormedSpace.geometricStructureClosure ℂ A).subspace
          ((NormedSpace.geometricStructureClosure ℂ A).component I)).HasContinuousFiniteConjugation
            (ClosureCat.IsCStarRealizable.{u, max u w})

In the source	Mathematical meaning
Ambient algebra`universe u v w uA uL variable {A : Type u} [NonUnitalCStarAlgebra A] variable [PartialOrder A] [StarOrderedRing A]`Fixed source	The complex C*-algebra with its compatible order; the size parameters are fixed for the selected theorem. No identity is required.
Nonzero algebra and one GNS model`[Nontrivial A] : (∃ phi : NonUnitalPureState A, IsCompactOperatorModel phi.gnsRepresentation) ↔`Fixed source	The nonzero algebra and one pure state whose same GNS representation satisfies (1).
Compact-operator model`def IsCompactOperatorModel [NonUnitalCStarAlgebra A] (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : Prop := Function.Injective e ∧ (∀ a : A, IsCompactOperator (e a)) ∧ ∀ T : H →L[ℂ] H, IsCompactOperator T → ∃ a : A, e a = T`Fixed source	Applied to , this means faithfulness and the two inclusions giving $\pi_\varphi(A)=\mathcal K(H_\varphi).$ Every image operator is compact, and every compact operator is an image of this same representation.
Singleton spectrum`(∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q) ∧`Fixed source	The irreducible spectrum has exactly one point, including its existence. This is conjoined with the component condition that follows.
Point and applied component condition`∃ I : NormedSpace.GeometricStructureSpace ℂ A, ((NormedSpace.geometricStructureClosure ℂ A).subspace ((NormedSpace.geometricStructureClosure ℂ A).component I)).HasContinuousFiniteConjugation (ClosureCat.IsCStarRealizable.{u, max u w}) := by`Fixed source	A point selects its finite-chain component . The ambient closure is restricted to this component, and the resulting closure is the input of the conjugation condition, with precisely the stated class of test spaces.
Geometric points`def GeometricStructureSpace : Type u := {I : Set E // I ∈ geometricStructureFamily 𝕜 E}`Fixed source	A point of is a subset of belonging to the geometric structure family. Thus the quantified is a geometric point, not an arbitrary subset or a normal-part point.
Ambient geometric closure`def geometricStructureClosure : ClosureSpace (GeometricStructureSpace 𝕜 E) := ClosureSpace.HullKernel.space (geometricStructureFamily 𝕜 E) (univ_notMem_geometricStructureFamily 𝕜 E)`Fixed source	The hull–kernel closure on the whole space , rather than the relative closure on a normal part.
Finite-chain component`def component (c : ClosureSpace α) (x : α) : Set α := {y \| c.Related x y}`Fixed source	The points related to by finite chains form . This is not a claim about ordinary topological connectedness.
Induced component closure`def subspace (c : ClosureSpace α) (A : Set α) : ClosureSpace A := c.induced (Subtype.val : A → α)`Fixed source	Restricting the ambient closure along inclusion gives the closure on the component. For , $c_{C_A(I)}(E)=C_A(I)\cap c_A(E).$
Class of test spaces`def IsCStarRealizable.{uA, uX} (X : ClosureCat.{uX}) : Prop := ∃ (A : Type uA) (instA : NonUnitalCStarAlgebra A), letI : NonUnitalCStarAlgebra A := instA Nontrivial A ∧ Nonempty (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A) X.str)`Fixed source	A test space is homeomorphic, for full closure, to for some nonzero complex C*-algebra . The bound algebra in this definition is the realizing , not necessarily the original .
All tests, components and first map`def HasContinuousFiniteConjugation (c : ClosureSpace α) (D : ClosureCat.{s} → Prop) : Prop := ∀ (L : ClosureCat.{s}), D L → ∀ t : L, ∀ f : FiniteHomeomorph (L.str.subspace (L.str.component t)) c, (L.str.subspace (L.str.component t)).Continuous c f.toEquiv →`Fixed source	Apply the closure parameter to and the test class to the preceding realizable spaces. For every such , every chosen point selects a component with induced closure; the map is a finite homeomorphism and is fully continuous in the forward direction.
Second map and the two conclusions`∀ g : FiniteHomeomorph (L.str.subspace (L.str.component t)) (L.str.subspace (L.str.component t)), (L.str.subspace (L.str.component t)).Continuous (L.str.subspace (L.str.component t)) g.toEquiv → c.Continuous c (f.conjugate g).toEquiv ∧ c.Continuous c (f.conjugate g).toEquiv.symm`Fixed source	For every finite homeomorphism with forward full continuity, both the conjugate and its actual inverse are fully continuous on : $\begin{aligned}h&=f\circ g\circ f^{-1},\\h^{-1}&=f\circ g^{-1}\circ f^{-1}.\end{aligned}$ These are the same maps in (4); no full continuity of or is an input.
Finite homeomorphism`structure FiniteHomeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where finitelyContinuous_toFun : c.FinitelyContinuous d toFun finitelyContinuous_invFun : d.FinitelyContinuous c invFun`Fixed source	One bijection with finite continuity for it and its inverse. For and this gives the finite-set equality (2) in their respective induced closure spaces.
Finite continuity`def FinitelyContinuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop := ∀ s : Set α, s.Finite → f '' c.closure s ⊆ d.closure (f '' s)`Fixed source	Closure preservation by inclusion for every finite subset, including the empty subset. Applying this in both directions to the same bijection gives (2).
Full continuity`def Continuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop := ∀ s : Set α, f '' c.closure s ⊆ d.closure (f '' s)`Fixed source	The inclusion (3) for every subset, without a finiteness restriction. In the conclusion the source and target closure are both .
The same conjugation`def FiniteHomeomorph.conjugate (f : FiniteHomeomorph c d) (g : FiniteHomeomorph c c) : FiniteHomeomorph d d := f.symm.trans (g.trans f)`Fixed source	The equivalence obtained by composing the same , then , then . Its forward map is and its inverse is , not an independently chosen inverse.