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 of a state ω on a unital C*-algebra A: N(ω) = { n ∈ A : ω (star n * n) = 0 }.

Blueprint reference: the set 𝒩 in 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 orthogonal set of a state ω on a unital C*-algebra A: N₁(ω) = { n ∈ A : ∀ b, ω (star b * n) = 0 }.

Blueprint reference: the set 𝒩₁ in 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 of a state ω, packaged as a Submodule ℂ A.

The linear-subspace content of lmm:lmm2: the carrier equals nullSet ω, and nullSet ω is closed under addition and under scalar multiplication by complex numbers, and contains 0.

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.