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 faithful state's GNS vector is separating. If π is a *-representation and Ω a vector reproducing a faithful state ω (i.e. ω a = ⟪Ω, π a Ω⟫), then π(a) Ω = 0 implies a = 0.

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 GNS triple (H, π, Ω) reproducing ω whose cyclic vector Ω is separating for π(A).