Skip to content

GNS construction

2 fully proved

Positive Linear Map

TheoremExistence of a unit cyclic vector in the GNS space#✓fully proved

Let \(A\) be a unital C*-algebra with its standard order and let \(f\) be a positive linear functional on \(A\) with \(f(1) = 1\). Let \(H_f\) be the GNS Hilbert space of \(f\) and \(\pi_f : A \to B(H_f)\) its GNS representation. Then there is a vector \(\xi \in H_f\) with \(\|\xi\| = 1\) such that \(f(a) = \langle \xi, \pi_f(a) \xi \rangle\) for every \(a \in A\), and the linear span of \(\{\pi_f(a) \xi : a \in A\}\) is dense in \(H_f\).

theorem exists_gns_cyclic_vector
    {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
    (f : A →ₚ[ℂ] ℂ) (hf : f (1 : A) = (1 : ℂ)) :
    ∃ (ξ : f.GNS), ‖ξ‖ = 1 ∧
      (∀ a : A, f a = ⟪ξ, (f.gnsStarAlgHom a) ξ⟫_ℂ) ∧
      Dense (↑(Submodule.span ℂ (Set.range fun a : A => (f.gnsStarAlgHom a) ξ)) : Set f.GNS)
Used by 1
Used byGNS cyclic vector of a state

The GNS construction

TheoremGNS cyclic vector of a state#✓fully proved

Let \(A\) be a unital C*-algebra with its standard order and let \(f\) be a positive linear functional on \(A\) with \(f(1) = 1\). Let \(H_f\) be the GNS Hilbert space of \(f\) and \(\pi_f : A \to B(H_f)\) its GNS representation. Then there is a vector \(\xi \in H_f\) with \(\|\xi\| = 1\) such that \(f(a) = \langle \xi, \pi_f(a) \xi \rangle\) for every \(a \in A\), and the linear span of \(\{\pi_f(a) \xi : a \in A\}\) is dense in \(H_f\).

theorem cStarAlgebra_gns_cyclic_vector
    {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
    (f : A →ₚ[ℂ] ℂ) (hf : f (1 : A) = (1 : ℂ)) :
    ∃ (ξ : f.GNS), ‖ξ‖ = 1 ∧
      (∀ a : A, f a = ⟪ξ, (f.gnsStarAlgHom a) ξ⟫_ℂ) ∧
      Dense (↑(Submodule.span ℂ (Set.range fun a : A => (f.gnsStarAlgHom a) ξ)) : Set f.GNS)
Sources
  • GNS construction, Gelfand–Naimark 1943 and I. E. Segal, Ann. of Math. 48 (1947); see Murphy, C*-Algebras; Lean is unital state f 1 = 1 unit cyclic vector with inner-product formula and dense span. It is PositiveLinearMap.exists_gns_cyclic_vector, kept under the source's name.
Uses 1
Proof usesExistence of a unit cyclic vector in the GNS space

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.