PhyslibAlpha.AlgebraicFramework.CStarAlgebra.GNS

The Gelfand─Naimark─Segal (GNS) construction: the cyclic vector

Every state produces a Hilbert space it did not start with. Given a state `ω` on a unital C⋆-algebra `A` — no Hilbert space assumed, no representation assumed, just a positive normalized linear functional (`ω : 𝓢[A]`, `OVERVIEW.md` §13) — the GNS construction recovers both: a Hilbert space `H_ω`, a `⋆`-representation `π_ω : A → B(H_ω)`, and inside `H_ω` a single unit vector `Ω_ω` that reproduces `ω` as a vector state of the representation,

`ω(a) = ⟪Ω_ω, π_ω(a) Ω_ω⟫`.

`Ω_ω` is *cyclic*: applying every `a ∈ A` to it sweeps out a dense subspace of `H_ω`, so nothing in `H_ω` sits outside what `π_ω(A)` can reach starting from `Ω_ω`. This is the converse to §13's vector states `ω_ψ(x) = ⟪ψ, xψ⟫`: every state, not only the ones already handed a Hilbert space to live on, *is* a vector state — of the Hilbert space this construction builds for it out of `ω` alone.

`Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal` already builds `H_ω` (`PositiveLinearMap.GNS`) and `π_ω` (`PositiveLinearMap.gnsStarAlgHom`) from an arbitrary positive linear functional. Its docstring lists the missing cyclic vector as a `TODO`. This file supplies exactly that: `Ω_ω` is the image of `1 : A` inside `H_ω`, the defining identity above, cyclicity of `Ω_ω`, and faithfulness of `π_ω` when `ω` itself is a faithful state.

Main definitions

- `UnitalPositiveLinearMap.GNS`, `UnitalPositiveLinearMap.gnsRep` : `H_ω` and `π_ω`, read directly off a state `ω : 𝓢[A]` rather than through the bare positive functional mathlib works with. - `UnitalPositiveLinearMap.gnsCyclicVector` : `Ω_ω`, the image of `1 : A` in `H_ω`, of unit norm (`norm_gnsCyclicVector`). - `UnitalPositiveLinearMap.inner_gnsCyclicVector_gnsRep_gnsCyclicVector` : the defining identity `ω(a) = ⟪Ω_ω, π_ω(a) Ω_ω⟫`. - `UnitalPositiveLinearMap.denseRange_gnsRep_gnsCyclicVector` : `Ω_ω` is cyclic — `π_ω(A) Ω_ω` is dense in `H_ω`. - `UnitalPositiveLinearMap.IsFaithful`, `UnitalPositiveLinearMap.injective_gnsRep_of_isFaithful` : a faithful state gives an injective (hence genuinely faithful) representation `π_ω`.

9 declarations

abbrev

GNS Hilbert space $H_\omega$

#GNS

Given a unital positive linear map $\omega$ (a state) on a unital $C^*$ -algebra $A$ , the GNS Hilbert space $H_\omega$ is the Hilbert space completion of $A$ with respect to the semi-inner product defined by $\langle x, y \rangle = \omega(x^* y)$ .

abbrev

GNS representation $\pi_\omega: A \to \mathcal{B}(H_\omega)$

#gnsRep

For a state $\omega$ on a unital $C^*$ -algebra $A$ , the GNS representation $\pi_\omega$ is the unital $\star$ -homomorphism from $A$ to the algebra of bounded linear operators $\mathcal{B}(H_\omega)$ on the GNS Hilbert space $H_\omega$ . This map is induced by the left multiplication action of $A$ on itself.

definition

GNS cyclic vector $\Omega_\omega$

#gnsCyclicVector

For a unital positive linear map $\omega$ (a state) on a unital $C^*$ -algebra $A$ , the GNS cyclic vector $\Omega_\omega$ is the element in the GNS Hilbert space $H_\omega$ defined as the image of the identity element $1 \in A$ under the canonical map from the algebra to its GNS representation space.

theorem

$\pi_\omega(a) \Omega_\omega$ is the canonical image of $a$ in $H_\omega$

#gnsRep_gnsCyclicVector

For a state $\omega$ on a unital $C^*$ -algebra $A$ , let $\pi_\omega: A \to \mathcal{B}(H_\omega)$ be the GNS representation and $\Omega_\omega \in H_\omega$ be the GNS cyclic vector. For any element $a \in A$ , the operator $\pi_\omega(a)$ applied to the cyclic vector $\Omega_\omega$ is equal to the canonical image of $a$ in the GNS Hilbert space $H_\omega$ .

theorem

The GNS cyclic vector has unit norm $\|\Omega_\omega\| = 1$

#norm_gnsCyclicVector

For a state $\omega$ on a unital $C^*$ -algebra $A$ (a unital positive linear map), let $\Omega_\omega$ be the associated cyclic vector in the GNS Hilbert space $H_\omega$ . The norm of this cyclic vector is $\|\Omega_\omega\| = 1$ .

theorem

GNS Defining Identity: $\omega(a) = \langle \Omega_\omega, \pi_\omega(a) \Omega_\omega \rangle$

#inner_gnsCyclicVector_gnsRep_gnsCyclicVector

For any element $a$ in a unital $C^*$ -algebra $A$ with a state $\omega$ , the value of the state is given by the inner product $\omega(a) = \langle \Omega_\omega, \pi_\omega(a) \Omega_\omega \rangle$ , where $\pi_\omega$ is the GNS representation and $\Omega_\omega$ is the GNS cyclic vector in the Hilbert space $H_\omega$ .

theorem

The GNS Vector $\Omega_\omega$ is Cyclic ( $\pi_\omega(A) \Omega_\omega$ is Dense in $H_\omega$ )

#denseRange_gnsRep_gnsCyclicVector

Let $A$ be a unital $C^*$ -algebra and $\omega$ be a state (a unital positive linear map) on $A$ . Let $H_\omega$ be the GNS Hilbert space, $\pi_\omega : A \to \mathcal{B}(H_\omega)$ be the GNS representation, and $\Omega_\omega \in H_\omega$ be the GNS cyclic vector (the image of $1 \in A$ ). Then the range of the map $a \mapsto \pi_\omega(a) \Omega_\omega$ is dense in $H_\omega$ . That is, the orbit $\pi_\omega(A) \Omega_\omega = \{ \pi_\omega(a) \Omega_\omega \mid a \in A \}$ is a dense subspace of $H_\omega$ , meaning every vector in $H_\omega$ is a limit of vectors reachable from $\Omega_\omega$ by applying elements of $A$ .

definition

Faithfulness of a state $\omega$ : $\omega(x^* x) = 0 \implies x = 0$

#IsFaithful

A state $\omega$ on a unital $C^*$ -algebra $A$ is **faithful** if for all $x \in A$ , the equality $\omega(x^* x) = 0$ implies $x = 0$ .

theorem

Faithfulness of $\omega$ implies injectivity of the GNS representation $\pi_\omega$

#injective_gnsRep_of_isFaithful

Let $A$ be a unital $C^*$ -algebra and let $\omega$ be a state on $A$ . If $\omega$ is faithful (meaning $\omega(a^* a) = 0$ implies $a = 0$ for all $a \in A$ ), then the associated GNS representation $\pi_\omega : A \to \mathcal{B}(H_\omega)$ is injective.

PhyslibAlpha.AlgebraicFramework.CStarAlgebra.GNS

The Gelfand─Naimark─Segal (GNS) construction: the cyclic vector

Main definitions

GNS Hilbert space HωH_\omegaHω​

GNS representation πω:A→B(Hω)\pi_\omega: A \to \mathcal{B}(H_\omega)πω​:A→B(Hω​)

GNS cyclic vector Ωω\Omega_\omegaΩω​

πω(a)Ωω\pi_\omega(a) \Omega_\omegaπω​(a)Ωω​ is the canonical image of aaa in HωH_\omegaHω​

The GNS cyclic vector has unit norm ∥Ωω∥=1\|\Omega_\omega\| = 1∥Ωω​∥=1

GNS Defining Identity: ω(a)=⟨Ωω,πω(a)Ωω⟩\omega(a) = \langle \Omega_\omega, \pi_\omega(a) \Omega_\omega \rangleω(a)=⟨Ωω​,πω​(a)Ωω​⟩

The GNS Vector Ωω\Omega_\omegaΩω​ is Cyclic (πω(A)Ωω\pi_\omega(A) \Omega_\omegaπω​(A)Ωω​ is Dense in HωH_\omegaHω​)

Faithfulness of a state ω\omegaω: ω(x∗x)=0 ⟹ x=0\omega(x^* x) = 0 \implies x = 0ω(x∗x)=0⟹x=0

Faithfulness of ω\omegaω implies injectivity of the GNS representation πω\pi_\omegaπω​

GNS Hilbert space $H_\omega$

GNS representation $\pi_\omega: A \to \mathcal{B}(H_\omega)$

GNS cyclic vector $\Omega_\omega$

$\pi_\omega(a) \Omega_\omega$ is the canonical image of $a$ in $H_\omega$

The GNS cyclic vector has unit norm $\|\Omega_\omega\| = 1$

GNS Defining Identity: $\omega(a) = \langle \Omega_\omega, \pi_\omega(a) \Omega_\omega \rangle$

The GNS Vector $\Omega_\omega$ is Cyclic ( $\pi_\omega(A) \Omega_\omega$ is Dense in $H_\omega$ )

Faithfulness of a state $\omega$ : $\omega(x^* x) = 0 \implies x = 0$

Faithfulness of $\omega$ implies injectivity of the GNS representation $\pi_\omega$