Physicslib4.GNS.Construction

The GNS Construction Theorem

This file states the GNS Construction Theorem from the AQFT-in-Lean blueprint (section 10.1, label thrm:gns-construction-theorem).

Given a state ω over a unital C*-algebra A, the theorem asserts the existence of a complex Hilbert space H_ω, a *-representation π_ω : A →⋆ₐ[ℂ] (H_ω →L[ℂ] H_ω), and a cyclic vector Ω ∈ H_ω for π_ω such that

• ω a = ⟪Ω, π_ω a Ω⟫ for every a : A, and
• if ω is faithful, then π_ω is injective.

The triple is also unique up to unitary equivalence, which we state as a separate theorem gns_unique because expressing the uniqueness clause as a conjunct inside the existence statement above is awkward (the two Hilbert spaces being compared live in different types).

Main statements

• Physicslib4.GNS.gns_construction: existence of the GNS triple (H, π, Ω), with the cyclicity, reproducing-formula, and faithfulness clauses bundled inside a single existential.
• Physicslib4.GNS.gns_unique: uniqueness of the GNS triple up to a unitary equivalence intertwining the representations and sending the cyclic vector to the cyclic vector.

Notes

The Hilbert space H is existentially quantified in A's universe u (gns_construction.{u}), rather than in a separate Type*, to avoid the usual universe-polymorphism issues that arise when existentially quantifying over a type variable: the GNS Hilbert space is constructed as a completion of a quotient of A, so it lives there.

theorem Physicslib4.GNS.gns_construction {A : Type u} [CStarAlgebra A] (ω : State A) : ∃ (H : Type u) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H), IsCyclicVector π Ω ∧ (∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) ∧ (ω.IsFaithful → Function.Injective ⇑π)

The GNS construction: every state ω is the vector state of a cyclic representation (H, π, Ω).

Given a state ω on a unital C*-algebra A, there are a complex Hilbert space H, a representation π of A by bounded operators on H and a vector Ω ∈ H such that

ω(a) = ⟨Ω, π(a)Ω⟩ for every a ∈ A,

and Ω is cyclic for π. If ω is faithful, π is injective. This is how a Hilbert space enters algebraic quantum field theory: the theory gives the algebra of observables and a state, such as the vacuum, and the GNS construction produces the Hilbert space on which the observables act as operators, with Ω representing the state. The construction completes A/N(ω) for the inner product ⟨[a], [b]⟩ = ω(a* b) (nullSet), with π(a)[b] = [ab] and Ω = [1]. The triple is unique up to unitary equivalence (gns_unique).

Implementation note: H is the space PositiveLinearMap.GNS that Mathlib builds from ω, and π is PositiveLinearMap.gnsStarAlgHom. The statement quantifies H in the universe of A, where that space lives.

Blueprint: thrm:gns-construction-theorem

theorem Physicslib4.GNS.gns_unique {A : Type u_1} [CStarAlgebra A] (ω : State A) {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] (π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁) (hcyc₁ : IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : A), ω a = inner ℂ Ω₁ ((π₁ a) Ω₁)) {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₂ : IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (a : A), ω a = inner ℂ Ω₂ ((π₂ a) Ω₂)) : ∃ (U : H₁ ≃ₗᵢ[ℂ] H₂), U Ω₁ = Ω₂ ∧ ∀ (a : A) (x : H₁), U ((π₁ a) x) = (π₂ a) (U x)

Uniqueness of the GNS triple: two cyclic representations reproducing ω are unitarily equivalent.

Let (H₁, π₁, Ω₁) and (H₂, π₂, Ω₂) be representations of A with cyclic vectors, both reproducing the state ω: ω(a) = ⟨Ω₁, π₁(a)Ω₁⟩ = ⟨Ω₂, π₂(a)Ω₂⟩. Then there is a unitary U : H₁ → H₂ with UΩ₁ = Ω₂ and U π₁(a) = π₂(a) U for all a ∈ A. The map U sends π₁(a)Ω₁ to π₂(a)Ω₂; it preserves inner products, since both equal ω(a* b), and it extends from the dense orbits to the whole spaces. So the representation that a state determines is unique, and "the" GNS representation of ω is well defined up to unitary equivalence.

Implementation note: U is a linear isometric equivalence H₁ ≃ₗᵢ[ℂ] H₂, and the two Hilbert spaces may live in different universes.

Blueprint: thrm:gns-construction-theorem