Physicslib4.GNS.NullSpace

The null space of a state on a unital C*-algebra

This file formalises the statements of lemmas lmm:lmm1 and lmm:lmm2 from section 10.1 of the AQFT-in-Lean blueprint.

Given a state ω on a unital C*-algebra A, the null space of ω is the set N(ω) := { n ∈ A : ω (n* n) = 0 }, and the orthogonal set is N₁(ω) := { n ∈ A : ∀ b, ω (b* n) = 0 }.

Main statements

• Physicslib4.GNS.nullSet: the set N(ω).
• Physicslib4.GNS.orthSet: the set N₁(ω).
• Physicslib4.GNS.lmm1: nullSet ω = orthSet ω (blueprint lmm:lmm1).
• Physicslib4.GNS.nullSubmodule: the null space packaged as a Submodule ℂ A (carrier equal to nullSet ω), giving the linear-subspace content of lmm:lmm2.
• Physicslib4.GNS.lmm2: nullSet ω underlies a closed Submodule ℂ A (blueprint lmm:lmm2). The primary entry point is lmm2; the helper nullSubmodule_isClosed records closedness separately for convenience.

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

The null set N(ω) = { n ∈ A : ω(n* n) = 0 } of a state ω.

The GNS construction starts from the form ⟨a, b⟩ = ω(a* b) on A. It is positive semi-definite but not an inner product when ω is not faithful, because ⟨n, n⟩ = 0 for every n ∈ N(ω). The set N(ω) equals { n : ω(b* n) = 0 for all b } (lmm1), so it is a closed linear subspace (lmm2), and the form descends to a genuine inner product on A/N(ω). The GNS Hilbert space is the completion of A/N(ω). (The blueprint also uses that N(ω) is a left ideal, so that π(a)[b] = [ab] is well defined; the library does not state this.) A faithful state has N(ω) = {0}.

Implementation note: gns_construction builds the GNS space with Mathlib's PositiveLinearMap.GNS, the completion of A with the seminorm a ↦ ω(a* a)^(1/2); the quotient by N(ω) happens inside that completion, so this file records the blueprint's lemmas about N(ω) and is not used by the construction.

Blueprint: the set 𝒩 of lmm:lmm1 and lmm:lmm2

Equations

• Physicslib4.GNS.nullSet ω = {n : A | ω (star n * n) = 0}

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

The set N₁(ω) = { n ∈ A : ω(b* n) = 0 for all b ∈ A } of a state ω.

These are the elements orthogonal to all of A for the form ⟨b, n⟩ = ω(b* n). By the Cauchy–Schwarz inequality |ω(b* n)|² ≤ ω(b* b) ω(n* n), the set equals the null set N(ω) (lmm1).

Blueprint: the set 𝒩₁ of lmm:lmm1

Equations

• Physicslib4.GNS.orthSet ω = {n : A | ∀ (b : A), ω (star b * n) = 0}

theorem Physicslib4.GNS.lmm1 {A : Type u_1} [CStarAlgebra A] (ω : State A) : nullSet ω = orthSet ω

Equality of the null set and the orthogonal set (lmm:lmm1).

Let ω be a state over a unital C*-algebra A. Then nullSet ω = orthSet ω, i.e. { n : ω (n* n) = 0 } = { n : ∀ b, ω (b* n) = 0 }.

def Physicslib4.GNS.nullSubmodule {A : Type u_1} [CStarAlgebra A] (ω : State A) : Submodule ℂ A

The null set N(ω) of a state ω as a complex linear subspace of A.

Closure under sums and scalar multiples follows from N(ω) = N₁(ω) (lmm1), since N₁(ω) is plainly linear. The subspace is closed (nullSubmodule_isClosed), so the quotient A/N(ω) is a normed space.

Implementation note: the carrier is nullSet ω by definition (nullSubmodule_coe).

Blueprint: the subspace 𝒩 of lmm:lmm2

Equations

• Physicslib4.GNS.nullSubmodule ω = { carrier := Physicslib4.GNS.nullSet ω, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Physicslib4.GNS.nullSubmodule_coe {A : Type u_1} [CStarAlgebra A] (ω : State A) : ↑(nullSubmodule ω) = nullSet ω

theorem Physicslib4.GNS.nullSubmodule_isClosed {A : Type u_1} [CStarAlgebra A] (ω : State A) : IsClosed ↑(nullSubmodule ω)

Closedness of the null submodule (lmm:lmm2, closedness part).

The underlying set of nullSubmodule ω is closed in A.

theorem Physicslib4.GNS.lmm2 {A : Type u_1} [CStarAlgebra A] (ω : State A) : ∃ (S : Submodule ℂ A), ↑S = nullSet ω ∧ IsClosed ↑S

The null space is a closed linear subspace (lmm:lmm2, primary entry point).

Let ω be a state over a unital C*-algebra A. Then there exists a Submodule ℂ A whose underlying set is nullSet ω and which is closed in the topology of A. Concretely, nullSubmodule ω witnesses the existential.