Haag-Kastler nets #
This file bundles the data of Axiom 1 (def:local-algebras)
together with the propositional content of Axioms 2, 3 and 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,LocalCommutativityandLorentzCovariance.
Notes #
The structure deliberately does not bundle Axiom 4. What its consumers needed from that axiom was the existence of a quasilocal algebra, and that is now a theorem,
exists_quasilocalAlgebra(thrm:quasilocal-algebra-exists), which builds the algebra from the net alone;HaagKastlerNet.quasilocalis defined from it. Axiom 4 proper (def:quasilocal-completeness) is a bridge principle relating physical observables to the formalism, with no mathematical consumers, and is encoded separately inPhysicslib4/AQFT/HaagKastler/ObservableBridge.lean.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).Written
LocalNet.{u}rather thanLocalNetso that this structure is universe polymorphic. Left implicit, the universe ofLocalNetwould be pinned here, and every net in the development would be forced to have its local algebras in one fixed universe -- the same size restriction thatQuasilocalAlgebra.carrierwas just freed from, reimposed at the bundling level. Isotony: inclusions of Alexandrov-basis sets induce unital
*-monomorphisms of the corresponding local algebras (Axiom 2).- localCommutativity : LocalCommutativity self.U self.isotony
Local commutativity: local algebras of completely-spacelike basis sets commute inside the quasilocal algebra (Axiom 3).
- 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.
This is constructed, not assumed. The witness is exists_quasilocalAlgebra
(thrm:quasilocal-algebra-exists), which builds 𝔘 from the net alone as the
completion of the directed colimit of the local algebras. The net therefore
carries no quasilocal-completeness field: what consumers of the former Axiom 4
actually needed was this existence theorem, not a physical bridge principle.
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 net's Axiom 2 data: every local algebra is ℂ and every inclusion
is implemented by the identity, which is trivially functorial.
This must precede trivialQuasilocalAlgebra, which is now indexed by it.
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 ℂ →⋆ₐ[ℂ] ℂ. It no longer supplies its own
inclusion family; the cocone condition ι_inclusion is stated against the Axiom 2
family trivialLocalNetIsotony.
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.
Stated at universe 0 because the witness is built from ℂ, which lives in
Type. Consistency of the axioms needs only one model, so nothing is lost; a
witness in an arbitrary universe would come from a ULift of this one.