Physicslib4.GNS.Basic

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 has no packaged State type for C*-algebras, so one is introduced 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, but IsCyclicVector is declared under this file's ambient variable (A : Type*) [CStarAlgebra A], so in Lean A is a unital C*-algebra (matching every call site in the project). The generality kept here is on the H side: H is required only to be a complex Hilbert space, not fixed to the GNS space of a particular state.

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

A state on a unital C*-algebra A: a positive, normalised continuous linear functional ω : A → ℂ.

The number ω(a) is the expectation value of the observable a in the state ω. Positivity asks that ω(a* a) ≥ 0 for every a ∈ A, that is, ω(a* a) is real and non-negative. Normalisation asks that the operator norm ‖ω‖ is 1; for a positive functional on a nonzero algebra the norm is Re ω(1) (norm_eq_re_apply_one_of_positive), so this is the familiar ω(1) = 1. A density matrix ρ gives the state a ↦ tr(ρa) of the algebra of bounded operators on a Hilbert space, but the definition needs no Hilbert space: the GNS construction (gns_construction) produces one from ω.

Implementation note: the structure extends A →L[ℂ] ℂ, and a FunLike instance lets one write ω a. Positivity uses Mathlib's partial order on ℂ (ComplexOrder), in which 0 ≤ z means that z is real and non-negative.

Blueprint: 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) is real and non-negative for every a ∈ A.

• isNormalized : ‖self.toContinuousLinearMap‖ = 1

  Normalisation: the operator norm ‖ω‖ equals 1.

@[instance_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 faithful state: ω(a* a) > 0 for every nonzero a ∈ A.

Since ω(a* a) ≥ 0 always, this says that ω(a* a) = 0 only for a = 0: no nonzero observable has vanishing expectation of a* a. A faithful state has an injective GNS representation (gns_construction), and its cyclic vector is separating (separating_of_faithful). On a matrix algebra the Gibbs state a ↦ tr(e^(−βH) a)/Z is faithful, while a vector state a ↦ ⟨ψ, aψ⟩ is not: it vanishes on a* a whenever a annihilates the unit vector ψ.

Blueprint: def:state

Equations

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

noncomputable def Physicslib4.GNS.State.toPositiveLinearMap {A : Type u_1} [CStarAlgebra A] (ω : State A) [PartialOrder A] [StarOrderedRing A] : A →ₚ[ℂ] ℂ

Repackaging of a state as a Mathlib PositiveLinearMap, using the canonical spectral order on the C*-algebra A, so that Mathlib's GNS infrastructure applies.

Equations

• ω.toPositiveLinearMap = { toFun := ⇑ω.toContinuousLinearMap, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }

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 cyclic vector Ω for a representation π of A on H: the vectors π(a)Ω, a ∈ A, are dense in H.

Every vector of H is then a limit of vectors obtained by acting on Ω with the represented algebra, as every state of a Fock space is obtained from the vacuum by acting with creation operators. The GNS representation of a state always has a cyclic vector (gns_construction), and a cyclic representation reproducing a state is determined by the state up to unitary equivalence (gns_unique).

Implementation note: a representation is a unital -homomorphism π : A →⋆ₐ[ℂ] (H →L[ℂ] H) into the bounded operators on a complex Hilbert space H. The blueprint allows any algebra A; here A is a unital C-algebra, the case used throughout the project.

Blueprint: def:cyclic-vector

Equations

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