Physicslib4.GNS.Separating

The GNS vector of a faithful state is separating

For a faithful state ω the cyclic GNS vector Ω is separating for the representation: π(a) Ω = 0 forces a = 0. The argument is the standard GNS computation ‖π(a) Ω‖² = ⟪Ω, π(a⋆ a) Ω⟫ = ω(a⋆ a), so a null vector means ω(a⋆ a) = 0, and faithfulness gives a = 0.

This is the companion to the injectivity clause of gns_construction and the starting point for any modular (Tomita-Takesaki) development, where a cyclic and separating vector is the basic datum.

Main results

• Physicslib4.GNS.separating_of_faithful: in any representation reproducing a faithful state, the cyclic vector is separating.
• Physicslib4.GNS.exists_gns_separating: the GNS specialization.

theorem Physicslib4.GNS.separating_of_faithful {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {ω : State A} (hω : ω.IsFaithful) (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) (hrep : ∀ (a : A), ω a = inner ℂ Ω ((π a) Ω)) {a : A} (ha : (π a) Ω = 0) : a = 0

A vector reproducing a faithful state is separating: π(a)Ω = 0 forces a = 0.

Let π be a representation of A on H and Ω a vector with ω(a) = ⟨Ω, π(a)Ω⟩ for a faithful state ω. If π(a)Ω = 0 then ω(a* a) = ‖π(a)Ω‖² = 0, and faithfulness gives a = 0. So distinct observables act differently on Ω. A vector that is both cyclic and separating is the starting datum of Tomita–Takesaki modular theory; in quantum field theory the Reeh–Schlieder theorem gives the vacuum this property for the algebras of bounded regions.

Implementation note: "separating" is stated for the elements of A (π(a)Ω = 0 implies a = 0), not for the generated von Neumann algebra π(A)''. The result holds in any representation reproducing ω, not only the GNS one.

Blueprint: thrm:separating-faithful

theorem Physicslib4.GNS.exists_gns_separating {A : Type u} [CStarAlgebra A] (ω : State A) (hω : ω.IsFaithful) : ∃ (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) Ω)) ∧ ∀ (a : A), (π a) Ω = 0 → a = 0

The GNS vector of a faithful state is cyclic and separating.

For a faithful state ω there is a representation (H, π, Ω) of A with Ω cyclic, ω(a) = ⟨Ω, π(a)Ω⟩ for all a, and π(a)Ω = 0 only for a = 0. It is the GNS triple of gns_construction together with separating_of_faithful.

Implementation note: as in gns_construction, H lives in the universe of A.

Blueprint: thrm:separating-faithful