Physicslib4.AQFT.HaagKastlerCurved.LocalAlgebra

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/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).

Supporting lemmas

• localObservables_eq: set-builder characterisation of localObservables, the curved mirror of quasilocalObservables_eq.
• one_mem_localObservables, add_mem_localObservables, smul_mem_localObservables: membership API showing localObservables contains the identity and is closed under addition and scaling.

Modelling notes

• On a generic Lorentzian spacetime there is no quasilocal algebra (see Axiom 3), so — unlike the Minkowski Axiom 4 (ObservableCorrespondence, whose measure lands in the one ambient quasilocal algebra 𝔘) — "all observables are local observables" cannot be phrased through a single 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 u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) (T : H →L[ℂ] H) : Prop

A local observable of a representation π of 𝔘(B): an operator π(a) with a self-adjoint in 𝔘(B).

Fix a region B and a *-representation π of its local algebra 𝔘(B) by bounded operators on a Hilbert space H; the blueprint's case is the GNS representation π_ω of a state ω on 𝔘(B) (gns_construction). A bounded operator T on H is a local observable when T = π(a) for some self-adjoint a ∈ 𝔘(B). Such a T is self-adjoint (IsLocalObservable.isSelfAdjoint), since π preserves the adjoint, so it is an observable in the quantum-mechanical sense, and it is measured in B. Conversely, every self-adjoint operator in the range of π is a local observable (isLocalObservable_iff).

Implementation note: π is any unital *-homomorphism 𝔘(B) → B(H), not only a GNS representation.

Blueprint: 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 u_1} [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 v) (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 in curved spacetime (local completeness): each observable of a local representation is a local observable.

The blueprint's axiom says that all observables are local observables. Curved spacetime has no quasilocal algebra, so there is no single algebra in which "all observables" live; the axiom is read locally instead. For every basis set B, every *-representation π of 𝔘(B) on a Hilbert space H, and every self-adjoint operator T in the range of π, T is a local observable: T = π(a) for a self-adjoint a ∈ 𝔘(B).

Read this way the axiom holds for every local net (localAlgebra_of): if T = π(b) is self-adjoint, then T is also the image of the self-adjoint part (b + b*)/2 of b.

Implementation note: the Hilbert spaces H range over Type v, the universe of the local algebras, which is where gns_construction puts the GNS spaces of their states (as in the Minkowski net). π is any unital *-homomorphism 𝔘(B) → B(H).

Blueprint: 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 u_1} [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 u_1} [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 u_1} [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 u_1} [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 u_1} [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 u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : U.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) : Set (H →L[ℂ] H)

The set of local observables of a representation π of 𝔘(B): the operators π(a) with a self-adjoint.

It equals the set of self-adjoint operators in the range of π (localObservables_eq), contains the identity and is closed under sums and real multiples.

Blueprint: the local observables of def:local-observable

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 u_1} [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 u_1} [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 u_1} [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 u_1} [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.