Haag-Kastler nets in curved spacetime #
This file bundles the data of Axiom 1
(def:local-algebras-in-curved-spacetime) together with the
propositional content of Axioms 2-5 into a single structure
HaagKastlerNet, formalising the blueprint declaration
def:haag-kastler-net-in-curved-spacetime (Chapter 10,
sections/sec10/haag-kastler-axioms-in-curved-spacetime, of the
AQFT-in-Lean blueprint).
Main definitions #
Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet: a structure consisting of aLocalNet M(Axiom 1 data) plus proofs ofIsotony,LocalCommutativity,LocalAlgebra, andIsometricCovariance.
Supporting lemmas #
commIsotony_injective: restatesIsotony.injectivethrough the net's chosencommIsotony.commute_of_spacelike_symm: the symmetric restatement ofcommute_of_spacelike, the curved mirror ofcommute_ι_of_spacelike_symm.isLocalObservable_of_isSelfAdjoint,isLocalObservable_add,isLocalObservable_smul,isLocalObservable_smul_add_smul: membership and closure API for the net's local observables, the curved mirrors of the quasilocal-observable API inPhysicslib4.AQFT.HaagKastler.Net.trivialSpacetime: the trivial Lorentzian spacetime underlying the joint satisfiability witness mentioned above.
Notes #
- As in the Minkowski case, joint satisfiability of the axioms is
witnessed by the trivial net (every region ↦
ℂ) over a trivial Lorentzian spacetime, givingNonempty (Σ M, HaagKastlerNet M).
A Haag–Kastler net on a curved spacetime M: a net of local algebras satisfying Axioms 1 to 5.
The structure bundles the local algebras B ↦ 𝔘(B) of Axiom 1, the isotony family of Axiom 2, and
proofs of local commutativity (Axiom 3), local completeness (Axiom 4) and isometric covariance
(Axiom 5). Theorems about a theory on M take a HaagKastlerNet M as hypothesis and use each axiom
as a field. Unlike the Minkowski net, there is no quasilocal algebra: results are stated in the
algebra 𝔘(B) of a basis set B containing the regions involved, or in a representation of it.
Axiom 4, read locally, is a field here and holds for every net (localAlgebra_of).
nonempty_haagKastlerNet shows that the axioms are consistent over every spacetime.
Implementation note: HaagKastlerNet.{u, v} M has its spacetime M in universe u and its local
algebras in universe v, independent of u.
Blueprint: def:haag-kastler-net-in-curved-spacetime
- U : LocalNet M
The local algebras B ↦ 𝔘(B) (Axiom 1).
Implementation note: the universe is named, as
LocalNet.{u, v}, so thatHaagKastlerNettakes the universe v of the algebras as a parameter, as in the Minkowski net. The isotony embeddings i(B₁, B₂) : 𝔘(B₁) → 𝔘(B₂), with their identity and composition laws (Axiom 2).
- localCommutativity : LocalCommutativity self.U self.isotony
Local commutativity (Axiom 3): for completely spacelike basis sets B₁, B₂ and every basis set B ⊇ B₁ ∪ B₂, the images of 𝔘(B₁) and 𝔘(B₂) in 𝔘(B) under the embeddings of
isotonycommute. - localAlgebra : LocalAlgebra self.U
Local completeness (Axiom 4): in every representation of a local algebra 𝔘(B), every self-adjoint operator in its range is a local observable.
- isometricCovariance : IsometricCovariance self.U self.isotony
Isometric covariance (Axiom 5): the isometries connected to the identity act on the net, compatibly with
isotony.
Instances For
The local algebra 𝔘(B) assigned by the net to a region B
(the Axiom 1 data, via the underlying LocalNet M).
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 *-isomorphism α_φ : 𝔘(B) → 𝔘(φ(B)) by which an isometry φ acts on the net.
Axiom 5 (isometricCovariance) asserts that such a family exists; this definition chooses one.
covEquiv_one, covEquiv_mul and covEquiv_commIsotony restate the three conditions of
Axiom 5 for it.
Blueprint: the maps α_φ of def:isometric-covariance-in-curved-spacetime
Equations
- N.covEquiv φ B = Exists.choose ⋯ φ B
Instances For
Isometry invariance of the local dimension. The local algebras
of a region B and of its isometric image φ·B have the same
ℂ-dimension: the covariance equivalence is in particular a ℂ-linear
isomorphism 𝔘(B) ≃ₗ[ℂ] 𝔘(φ·B).
Isometry invariance of the local norm. The covariance equivalence is a
*-isomorphism of C*-algebras, hence isometric: ‖α a‖ = ‖a‖.
Isometric transport of commutativity. Two local elements commute iff their images under the covariance equivalence commute.
Covariance, identity. The action of the identity isometry is the
identity automorphism (modulo the canonical identification
𝔘(B) = 𝔘(1·B) from one_smul).
Covariance, composition. The action is multiplicative in the
group element: α (φ'·φ) = α φ' ∘ α φ (modulo the canonical
identification 𝔘((φ'·φ)·B) = 𝔘(φ'·(φ·B)) from mul_smul).
The isotony embedding i(B₁, B₂) : 𝔘(B₁) → 𝔘(B₂) of the net, for basis sets B₁ ⊆ B₂.
This is the Axiom 2 family itself (isotony.map), so it is injective and satisfies the identity
and composition laws for every net (commIsotony_injective, commIsotony_self,
commIsotony_comp). Results about nested regions B₁ ⊆ B₂ ⊆ B compare algebras through these
embeddings into a common 𝔘(B).
Blueprint: the maps i of def:isotony-in-curved-spacetime
Equations
- N.commIsotony h₁ h₂ h = N.isotony.map h₁ h₂ h
Instances For
Each chosen isotony embedding is injective.
Identity law for the isotony embeddings, from Axiom 2.
Composition law for the isotony embeddings, from Axiom 2: the embedding
along B₁ ⊆ B₃ factors through any intermediate B₂.
This coherence holds for every net, including the trivial one, so no site
factoring a three-fold inclusion B₁ ⊆ B₂ ⊆ B needs it as a hypothesis.
Covariance commutes with isotony (Axiom 5 (3)): the covariance
equivalences intertwine the Axiom 2 isotony embeddings,
α_φ ∘ i_{B₁B₂} = i_{φB₁ φB₂} ∘ α_φ.
Transporting an isotony embedding along an equality of target regions.
Local commutativity. If basis sets B₁, B₂ are completely spacelike
and both contained in a common basis set B, their images in 𝔘(B) under the
isotony embeddings commute.
Local commutativity is symmetric. Commutation of completely-spacelike local algebras inside a common containing basis algebra holds in either order.
Monotonicity of local commutativity. Commutation of completely-spacelike
basis algebras is inherited by sub-basis-sets: if B₁, B₂ are completely
spacelike and contained in a common basis set B, and B₁' ⊆ B₁, B₂' ⊆ B₂
are basis sets, then the images of 𝔘(B₁') and 𝔘(B₂') in 𝔘(B) commute.
The first argument mono is the monotonicity of the spacelike-separation
relation. On the abstract LorentzianSpacetime interface this is a hypothesis;
for a net over a geometric spacetime it is discharged by
Spacetime.LorentzianSpacetime.isCompletelySpacelike_mono.
Net-level Axiom 4 (Local Algebra). In every GNS representation π
of a local algebra 𝔘(B) of the net (over an Alexandrov-basis set B),
every self-adjoint operator in the range of π is a local observable.
This applies the net's localAlgebra field.
The identity operator is a local observable of the net.
The net's local observables are closed under addition.
The net's local observables are closed under scaling by a self-adjoint (i.e. real) complex scalar.
Real-linear combinations of the net's local observables are local observables.
The trivial net and joint satisfiability of the axioms #
The curved-spacetime Haag-Kastler axioms are not vacuous: over a
trivial Lorentzian spacetime, the trivial net assigning ℂ to
every region satisfies all of Axioms 1-5.
A one-point instance of the abstract spacetime interface, with the trivial isometry group.
Every set is a basis set and every two sets are completely spacelike. This shows that the interface asks for no geometry: in a geometric spacetime no point is spacelike to itself, so completely spacelike regions are disjoint, but the interface imposes no such condition. This spacetime is a test case for the interface, not a model of a physical spacetime.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The trivial local net over any spacetime M: the algebra ℂ for every region.
The normalisation 𝔘(∅) = ℂ·1 is the identity of ℂ. Together with the identity maps for isotony
and covariance it satisfies all five axioms (trivialHaagKastlerNet).
Implementation note: its algebras live in universe 0, because ℂ : Type.
Blueprint: the trivial net of thrm:haag-kastler-net-in-curved-spacetime-nonempty
Equations
- One or more equations did not get rendered due to their size.
Instances For
The isotony family of the trivial net: the identity map ℂ → ℂ for every inclusion.
The identity is injective and the identity and composition laws hold by definition.
Blueprint: the trivial net of thrm:haag-kastler-net-in-curved-spacetime-nonempty
Equations
- One or more equations did not get rendered due to their size.
Instances For
The trivial Haag–Kastler net over any spacetime M: ℂ for every region, identity maps throughout.
Each axiom holds for a simple reason. Isotony holds because the identity is functorial; local
commutativity because ℂ is commutative; local completeness because it holds for every net
(localAlgebra_of); and isometric covariance because every α_φ is the identity of ℂ, so its
three conditions hold by definition.
Implementation note: its algebras live in universe 0, because ℂ : Type.
Blueprint: the trivial net of thrm:haag-kastler-net-in-curved-spacetime-nonempty
Equations
- One or more equations did not get rendered due to their size.
Instances For
The curved-spacetime Haag–Kastler axioms are consistent: every spacetime carries a net.
The witness is the trivial net (trivialHaagKastlerNet), which assigns ℂ to every region. The
statement is for an arbitrary instance M of the abstract interface;
Spacetime.LorentzianSpacetime.nonempty_haagKastlerNet_identityComponent specialises it to a
geometric spacetime.
Implementation note: the net has its algebras in universe 0 because the witness is built from ℂ,
which lives in Type. Consistency of the axioms needs only one model, so nothing is lost; the
library gives no witness in other universes. The Minkowski
HaagKastler.nonempty_haagKastlerNet makes the same choice.
Blueprint: the abstract form of thrm:haag-kastler-net-in-curved-spacetime-nonempty