Axiom 4 (Local Algebra) and local observables, curved spacetime

This file formalises the blueprint declarations def:local-observable and def:local-completeness-in-curved-spacetime (Axiom 4 of the Haag-Kastler axioms on a Lorentzian spacetime, Chapter 10 (sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime) of the AQFT-in-Lean blueprint):

Local Observable. The image π_ω(a) of a self-adjoint member a of a local algebra 𝔘(𝐁) under the GNS *-homomorphism π_ω of a state ω on 𝔘(𝐁) is self-adjoint and corresponds to an observable, called a local observable.

Axiom 4 (Local Algebra). All "observables" are local observables.

Main definitions

• Physicslib4.AQFT.HaagKastlerCurved.IsLocalObservable (def:local-observable).
• Physicslib4.AQFT.HaagKastlerCurved.LocalAlgebra (Axiom 4, def:local-completeness-in-curved-spacetime).

Modelling notes

• On a generic Lorentzian spacetime there is no quasilocal algebra (see Axiom 3), so — unlike the Minkowski Axiom 4 (QuasilocalCompleteness, which collapses to the nonemptiness of a quasilocal algebra) — "all observables are local observables" cannot be phrased through one ambient algebra.

• We therefore relativise the statement to the local GNS representations that the framework actually provides: Axiom 4 asserts that in every GNS representation π of every local algebra 𝔘(B), every self-adjoint operator lying in the range of π is a local observable. This is the faithful curved reading of "all observables are local observables", and (like the Minkowski axioms for the trivial net) it is satisfiable — see localAlgebra_of below, which proves it holds for every net.

def Physicslib4.AQFT.HaagKastlerCurved.IsLocalObservable {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) (T : H →L[ℂ] H) : Prop

Local Observable (blueprint def:local-observable).

Fix a local net U, an Alexandrov-basis set B, and a GNS *-representation π : 𝔘(B) →⋆ₐ[ℂ] (H →L[ℂ] H) of the local algebra 𝔘(B) = U.algebra B on a complex Hilbert space H (in practice obtained from gns_construction applied to a state ω on 𝔘(B)). A bounded operator T : H →L[ℂ] H is a local observable if it is the image T = π a of some self-adjoint element a of the local algebra.

Blueprint reference: def:local-observable.

Equations

• Physicslib4.AQFT.HaagKastlerCurved.IsLocalObservable π T = ∃ (a : U.algebra B), IsSelfAdjoint a ∧ T = π a

theorem Physicslib4.AQFT.HaagKastlerCurved.IsLocalObservable.isSelfAdjoint {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H} {T : H →L[ℂ] H} (hT : IsLocalObservable π T) : IsSelfAdjoint T

Every local observable is self-adjoint: it is the image of a self-adjoint element of the local algebra under a *-homomorphism. This is the self-adjointness clause of def:local-observable.

theorem Physicslib4.AQFT.HaagKastlerCurved.exists_isLocalObservable {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} (ω : GNS.State (U.algebra B)) {a : U.algebra B} (ha : IsSelfAdjoint a) : ∃ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H), IsLocalObservable π (π a) ∧ IsSelfAdjoint (π a)

For any state ω on a local algebra 𝔘(B) and any self-adjoint element a of it, the GNS construction provides a *-representation in which π a is a local observable. This is the existence content of def:local-observable, tying together thrm:gns-construction-theorem and def:state.

def Physicslib4.AQFT.HaagKastlerCurved.LocalAlgebra {M : LorentzianSpacetime} (U : LocalNet M) : Prop

Axiom 4 (Local Algebra), curved spacetime. A local net U on a Lorentzian spacetime M satisfies the local algebra axiom if, in every GNS representation π of every local algebra 𝔘(B), every self-adjoint operator in the range of π is a local observable.

This is the curved reading of "all observables are local observables": the observables of the theory are exactly the images of self-adjoint local elements.

Blueprint reference: def:local-completeness-in-curved-spacetime.

Equations

• One or more equations did not get rendered due to their size.

theorem Physicslib4.AQFT.HaagKastlerCurved.localAlgebra_of {M : LorentzianSpacetime} (U : LocalNet M) : LocalAlgebra U

Axiom 4 holds for every local net. Given a self-adjoint operator T = π b in the range of a GNS representation, replacing b by its self-adjoint part 2⁻¹ • (b + star b) (which π still sends to T) exhibits T as a local observable. In particular the axiom is satisfiable.

theorem Physicslib4.AQFT.HaagKastlerCurved.isLocalObservable_one {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H} : IsLocalObservable π 1

The identity operator on the GNS Hilbert space is a local observable: it is the image π 1 of the (self-adjoint) unit of the local algebra.

theorem Physicslib4.AQFT.HaagKastlerCurved.IsLocalObservable.add {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H} {S T : H →L[ℂ] H} (hS : IsLocalObservable π S) (hT : IsLocalObservable π T) : IsLocalObservable π (S + T)

Local observables are closed under addition: the sum of the images of two self-adjoint elements is the image of their (self-adjoint) sum.

theorem Physicslib4.AQFT.HaagKastlerCurved.IsLocalObservable.smul {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H} {c : ℂ} {T : H →L[ℂ] H} (hT : IsLocalObservable π T) (hc : IsSelfAdjoint c) : IsLocalObservable π (c • T)

Local observables are closed under scaling by a self-adjoint complex scalar (equivalently, a real scalar): self-adjointness of c • a requires star c = c.

theorem Physicslib4.AQFT.HaagKastlerCurved.IsLocalObservable.smul_add_smul {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H} {c d : ℂ} {S T : H →L[ℂ] H} (hc : IsSelfAdjoint c) (hd : IsSelfAdjoint d) (hS : IsLocalObservable π S) (hT : IsLocalObservable π T) : IsLocalObservable π (c • S + d • T)

Real-linear combinations of local observables are local observables. The scalars are taken self-adjoint in ℂ, i.e. real, which is exactly the condition under which the combination stays self-adjoint.

theorem Physicslib4.AQFT.HaagKastlerCurved.isLocalObservable_iff {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H} {T : H →L[ℂ] H} : IsLocalObservable π T ↔ IsSelfAdjoint T ∧ T ∈ Set.range ⇑π

Characterisation of local observables. An operator T on the GNS Hilbert space is a local observable precisely when it is self-adjoint and lies in the range of the representation π. The forward direction is IsLocalObservable.isSelfAdjoint; the converse holds even when π is not injective, by replacing a preimage b with its self-adjoint part 2⁻¹ • (b + star b), which π still sends to T.

def Physicslib4.AQFT.HaagKastlerCurved.localObservables {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) : Set (H →L[ℂ] H)

The set of local observables on the GNS Hilbert space H for the representation π: all bounded operators of the form π a with a a self-adjoint element of the local algebra.

Equations

• Physicslib4.AQFT.HaagKastlerCurved.localObservables π = {T : H →L[ℂ] H | Physicslib4.AQFT.HaagKastlerCurved.IsLocalObservable π T}

theorem Physicslib4.AQFT.HaagKastlerCurved.localObservables_eq {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) : localObservables π = ↑(selfAdjoint (H →L[ℂ] H)) ∩ Set.range ⇑π

The local observables are exactly the self-adjoint elements lying in the range of the representation π.

theorem Physicslib4.AQFT.HaagKastlerCurved.one_mem_localObservables {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) : 1 ∈ localObservables π

The identity operator is a local observable.

theorem Physicslib4.AQFT.HaagKastlerCurved.add_mem_localObservables {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) {S T : H →L[ℂ] H} (hS : S ∈ localObservables π) (hT : T ∈ localObservables π) : S + T ∈ localObservables π

The local observables are closed under addition.

theorem Physicslib4.AQFT.HaagKastlerCurved.smul_mem_localObservables {M : LorentzianSpacetime} {U : LocalNet M} {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) {c : ℂ} {T : H →L[ℂ] H} (hT : T ∈ localObservables π) (hc : IsSelfAdjoint c) : c • T ∈ localObservables π

The local observables are closed under scaling by a self-adjoint (i.e. real) complex scalar.