Physicslib4.AQFT.HaagKastlerCurved.LocalCommutativity

Axiom 3 (Local Commutativity), curved spacetime

This file formalises the blueprint declaration def:local-commutativity-in-curved-spacetime (Axiom 3 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):

Let 𝐁₁, 𝐁₂ be Alexandrov-basis sets. If 𝐁₁ and 𝐁₂ are completely spacelike, then for any basis element 𝐁 with 𝐁₁, 𝐁₂ ⊆ 𝐁 the algebras 𝔘(𝐁₁) and 𝔘(𝐁₂) commute inside 𝔘(𝐁), i.e. i(a₁) i(a₂) - i(a₂) i(a₁) = 0, where i is the isotony *-monomorphism (Axiom 2). If no such 𝐁 exists, no condition is imposed.

Main definitions

• Physicslib4.AQFT.HaagKastlerCurved.LocalCommutativity: a Prop-valued predicate on a LocalNet M asserting Axiom 3.

Modelling notes

• This is the point where the curved axioms genuinely diverge from the Minkowski ones: there is no global quasilocal algebra on a generic Lorentzian spacetime, so commutativity cannot be phrased inside one ambient C*-algebra. Instead we quantify over a common containing basis set B (when one exists) and assert commutativity inside the local algebra 𝔘(B), transported there by the isotony embeddings i : 𝔘(Bᵢ) ↪ 𝔘(B).

• The isotony embeddings used are exactly those of Axiom 2: the predicate takes the Isotony family as a parameter and requires the images of its embeddings to commute; it introduces no family of its own. When no common containing basis set B exists, the universally quantified condition is vacuously satisfied, matching the blueprint's "if no such 𝐁 exists, it doesn't make sense to ask whether they commute".

def Physicslib4.AQFT.HaagKastlerCurved.LocalCommutativity {M : LorentzianSpacetime} (U : LocalNet M) (i : Isotony U) : Prop

Axiom 3 in curved spacetime (local commutativity): observables of completely spacelike basis sets commute in every basis set containing both.

Let B₁ and B₂ be completely spacelike basis sets. To multiply an element of 𝔘(B₁) by one of 𝔘(B₂), both must lie in one algebra. As in Minkowski spacetime, the axiom takes any basis set B containing both, and asks that for all a₁ ∈ 𝔘(B₁) and a₂ ∈ 𝔘(B₂) the equation

i(B₁, B)(a₁) i(B₂, B)(a₂) = i(B₂, B)(a₂) i(B₁, B)(a₁)

holds in 𝔘(B), where i is the isotony family of Axiom 2. The difference from Minkowski spacetime is that such a B need not exist, and there is no quasilocal algebra to fall back on. When no common containing basis set exists the condition is vacuous: the two algebras do not lie in a common algebra, so their commutation is not a meaningful question.

The axiom asserts only the commutation. The embeddings, their injectivity and their identity and composition laws belong to Axiom 2, whose family is a parameter here, so results that factor a three-fold inclusion B₁ ⊆ B₂ ⊆ B need no separate coherence hypothesis.

Blueprint: def:local-commutativity-in-curved-spacetime

Equations

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