Haag-Kastler nets #
This file bundles the data of Axiom 1 (def:local-algebras)
together with the propositional content of Axioms 2-5 into a single
structure HaagKastlerNet, formalising the blueprint declaration
def:haag-kastler-net (section 10.3 of the AQFT-in-Lean blueprint).
Main definitions #
Physicslib4.AQFT.HaagKastler.HaagKastlerNet: a structure consisting of aLocalNet(the Axiom 1 data) plus proofs ofIsotony,LocalCommutativity,QuasilocalCompleteness, andLorentzCovariance.
Notes #
- The structure intentionally does not bundle Axiom 6 (Primitivity) or further axioms; those will be added as separate structure fields in subsequent files when they are formalised.
A Haag-Kastler net on (the Alexandrov-basis sets of) Minkowski
spacetime: the data of Axiom 1 (def:local-algebras) together with
proofs of Axioms 2-5 (def:isotony,
def:local-commutativity, def:quasilocal-completeness,
def:lorentz-covariance).
Blueprint reference: def:haag-kastler-net.
- U : LocalNet
The underlying assignment
B ↦ 𝔘(B)(Axiom 1). Isotony: inclusions of Alexandrov-basis sets induce unital
*-monomorphisms of the corresponding local algebras (Axiom 2).- localCommutativity : LocalCommutativity self.U
Local commutativity: local algebras of completely-spacelike basis sets commute inside the quasilocal algebra (Axiom 3).
- quasilocalCompleteness : QuasilocalCompleteness self.U
Quasilocal completeness: the local algebras' images are dense in the quasilocal algebra; i.e. all observables are quasilocal observables (Axiom 4).
- lorentzCovariance : LorentzCovariance self.U
Lorentz covariance: the inhomogeneous Lorentz group acts on the net and the action commutes with isotony (Axiom 5).
Instances For
The local algebra 𝔘(B) assigned by the net to a region B
(the Axiom 1 data, via the underlying LocalNet).
Instances For
Net-level normalisation 𝔘(∅) ≃⋆ₐ[ℂ] ℂ.
Equations
Instances For
The empty-region algebra 𝔘(∅) is commutative.
The empty-region algebra 𝔘(∅) is one-dimensional over ℂ.
Isotony, reflexivity. Every Alexandrov-basis set embeds into
itself via the identity unital *-monomorphism.
Isotony, transitivity. For inclusions B₁ ⊆ B₂ ⊆ B₃ of
Alexandrov-basis sets, the net's isotony embeddings compose to a unital
*-monomorphism 𝔘(B₁) ↪ 𝔘(B₃).
The canonical quasilocal algebra 𝔘 of the net, chosen from the
existence witness provided by Axiom 4 (quasilocalCompleteness).
Equations
Instances For
Each local algebra 𝔘(B) of an Alexandrov-basis set embeds
norm-preservingly into the canonical quasilocal algebra 𝔘.
Each local embedding 𝔘(B) ↪ 𝔘 into the canonical quasilocal
algebra is an isometry (the metric form of norm_ι).
The covariance equivalence 𝔘(B) ≃⋆ₐ[ℂ] 𝔘(L·B) implementing the
action of a Lorentz transformation L on the net, chosen from the
existence witness provided by Axiom 5 (lorentzCovariance).
Equations
- N.covEquiv L B = Exists.choose ⋯ L B
Instances For
Lorentz invariance of the local dimension. The local algebras of
a region B and of its Lorentz translate L·B have the same
ℂ-dimension: the covariance equivalence is in particular a
ℂ-linear isomorphism 𝔘(B) ≃ₗ[ℂ] 𝔘(L·B).
Lorentz invariance of the local norm. The covariance equivalence is a
*-isomorphism of C*-algebras, hence isometric: ‖α a‖ = ‖a‖.
Lorentz transport of commutativity. Two local elements commute iff their images under the covariance equivalence commute.
Covariance, identity. The action of the identity Lorentz
transformation is the identity automorphism (modulo the canonical
identification 𝔘(B) = 𝔘(1·B) from one_smul).
Covariance, composition. The action is multiplicative in the
group element: α (L'·L) = α L' ∘ α L (modulo the canonical
identification 𝔘((L'·L)·B) = 𝔘(L'·(L·B)) from mul_smul).
The quasilocal algebra witnessing local commutativity (Axiom 3),
chosen from the existence witness in localCommutativity. (This may differ
from the canonical quasilocal of Axiom 4.)
Equations
Instances For
Local commutativity. The images in commAlgebra of two
completely-spacelike basis algebras commute.
Local commutativity is symmetric. Commutation of completely-spacelike local algebras holds in either order.
Characterisation of the net's quasilocal observables. An operator on the
GNS Hilbert space is a quasilocal observable iff it is self-adjoint and lies in
the range of the representation π of the canonical quasilocal algebra.
Every self-adjoint operator in the range of π is a quasilocal observable
of the net.
The identity operator is a quasilocal observable of the net.
The net's quasilocal observables are closed under addition.
The net's quasilocal observables are closed under scaling by a self-adjoint (i.e. real) complex scalar.
Real-linear combinations of the net's quasilocal observables are quasilocal observables.
The trivial net and joint satisfiability of the axioms #
The Haag-Kastler axioms are not vacuous: the trivial net, assigning the
one-dimensional C*-algebra ℂ to every region, satisfies all of Axioms 1-5.
This witnesses Nonempty HaagKastlerNet, i.e. the five axioms are jointly
consistent.
The trivial local net: every region is assigned the C*-algebra ℂ, with
the empty-region normalisation being the identity isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A concrete Alexandrov-basis set of standard Minkowski spacetime
(I⁺(0) ∩ I⁻(0)), used as a witness that basis sets exist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The trivial quasilocal algebra for the trivial net: ambient C*-algebra ℂ,
with every local embedding the identity ℂ →⋆ₐ[ℂ] ℂ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The trivial Haag-Kastler net: the trivial local net (every region ↦ ℂ)
bundled with proofs of Axioms 2-5.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Haag-Kastler axioms are jointly satisfiable. The trivial net (every
region ↦ ℂ) is a Haag-Kastler net, so HaagKastlerNet is nonempty.