Basic definitions for the GNS construction

This file formalises some basic notions used in the GNS construction, following the AQFT-in-Lean blueprint, section 10.1.

Main definitions

• Physicslib4.GNS.State: a state on an abstract C*-algebra, defined as a continuous linear functional that is positive (sends star a * a to a non-negative complex number) and normalised (operator norm equal to 1). This corresponds to the blueprint label def:state.
• Physicslib4.GNS.State.IsFaithful: faithfulness of a state, asserting that ω (star a * a) = 0 only when a = 0. Also part of def:state.
• Physicslib4.GNS.IsCyclicVector: a vector Ω of a Hilbert space H is cyclic for a representation π : A →⋆ₐ[ℂ] (H →L[ℂ] H) of an algebra A when the set { π a Ω : a ∈ A } is dense in H. This corresponds to the blueprint label def:cyclic-vector.

Notes

Mathlib does not yet provide a packaged State type for C*-algebras, so we introduce one here. The positivity condition is stated using the canonical partial order on ℂ from Mathlib: 0 ≤ z iff z.re ≥ 0 and z.im = 0.

The blueprint statement of def:cyclic-vector only requires A to be an algebra; here we keep the assumptions general enough to be reusable but require the operator-algebra side H →L[ℂ] H to make sense, so H is a complex Hilbert space.

structure Physicslib4.GNS.State (A : Type u_1) [CStarAlgebra A] extends A →L[ℂ] ℂ : Type u_1

A state on a unital C*-algebra A is a continuous linear functional A →L[ℂ] ℂ that is positive (sends every element of the form star a * a to a non-negative complex number) and normalised (operator norm equal to 1).

Blueprint reference: def:state.

• toFun : A → ℂ
• map_add' (x y : A) : (↑self.toContinuousLinearMap).toFun (x + y) = (↑self.toContinuousLinearMap).toFun x + (↑self.toContinuousLinearMap).toFun y
• map_smul' (m : ℂ) (x : A) : (↑self.toContinuousLinearMap).toFun (m • x) = (RingHom.id ℂ) m • (↑self.toContinuousLinearMap).toFun x
• cont : Continuous (↑self.toContinuousLinearMap).toFun
• isPositive (a : A) : 0 ≤ self.toContinuousLinearMap (star a * a)

  Positivity: ω (a* a) ≥ 0 for every a ∈ A.

• isNormalized : ‖self.toContinuousLinearMap‖ = 1

  Normalisation: the operator norm of ω equals 1.

@[implicit_reducible]

noncomputable instance Physicslib4.GNS.State.instFunLikeComplex {A : Type u_1} [CStarAlgebra A] : FunLike (State A) A ℂ

Equations

• Physicslib4.GNS.State.instFunLikeComplex = { coe := fun (ω : Physicslib4.GNS.State A) => ⇑ω.toContinuousLinearMap, coe_injective := ⋯ }

def Physicslib4.GNS.State.IsFaithful {A : Type u_1} [CStarAlgebra A] (ω : State A) : Prop

A state ω on a C*-algebra A is faithful if ω (star a * a) = 0 implies a = 0. Equivalently, a ≠ 0 implies 0 < ω (star a * a).

Blueprint reference: def:state (faithfulness clause).

Equations

• ω.IsFaithful = ∀ (a : A), a ≠ 0 → 0 < ω (star a * a)

def Physicslib4.GNS.IsCyclicVector {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : A →⋆ₐ[ℂ] H →L[ℂ] H) (Ω : H) : Prop

A vector Ω : H is cyclic for a representation π : A →⋆ₐ[ℂ] (H →L[ℂ] H) of A on the Hilbert space H when the set { π a Ω : a ∈ A } is dense in H.

Blueprint reference: def:cyclic-vector.

Equations

• Physicslib4.GNS.IsCyclicVector π Ω = Dense (Set.range fun (a : A) => (π a) Ω)