Axiom 1 (Local Algebras), curved spacetime

This file formalises the blueprint declaration def:local-algebras-in-curved-spacetime (Axiom 1 of the Haag-Kastler axioms on a Lorentzian spacetime, Chapter 10 (sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime) of the AQFT-in-Lean blueprint):

For any basis element 𝐁 of the Alexandrov topology on a Lorentzian spacetime M, i.e. any set of the form I⁺(p) ∩ I⁻(q), there is a corresponding abstract C*-algebra 𝔘(𝐁), and when 𝐁 is the empty set, 𝔘(∅) = ℂ · 1.

Main definitions

• Physicslib4.AQFT.HaagKastlerCurved.LocalNet: a structure bundling the data of Axiom 1 over an abstract LorentzianSpacetime M.

Modelling notes

The shape is identical to the Minkowski LocalNet (def:local-algebras), but with the fixed Minkowski carrier and Alexandrov-basis predicate replaced by the abstract interface M : LorentzianSpacetime. The empty-region normalisation 𝔘(∅) = ℂ · 1 is encoded by a StarAlgEquiv between the fiber over ∅ and ℂ.

structure Physicslib4.AQFT.HaagKastlerCurved.LocalNet (M : LorentzianSpacetime) : Type (max 1 u_1)

Axiom 1 (Local Algebras), curved spacetime. The data of a Haag-Kastler local net on a Lorentzian spacetime M: an assignment, for every subset B of M (thought of as an Alexandrov-basis set, with the empty set covering the normalisation 𝔘(∅) = ℂ · 1), of a unital C*-algebra algebra B.

The 𝔘(∅) = ℂ normalisation is captured by the field emptyEquivComplex exhibiting a StarAlgEquiv between algebra ∅ and ℂ.

Blueprint reference: def:local-algebras-in-curved-spacetime.

• algebra : Set M.Carrier → Type

  The C*-algebra 𝔘(B) assigned to a (would-be Alexandrov-basis) region B.

• instCStarAlgebra (B : Set M.Carrier) : CStarAlgebra (self.algebra B)

  The CStarAlgebra instance on each fiber 𝔘(B).

• emptyEquivComplex : self.algebra ∅ ≃⋆ₐ[ℂ] ℂ

  Normalisation: 𝔘(∅) = ℂ · 1, encoded as a *-algebra isomorphism algebra ∅ ≃⋆ₐ[ℂ] ℂ.

theorem Physicslib4.AQFT.HaagKastlerCurved.LocalNet.mul_comm_algebra_empty {M : LorentzianSpacetime} (U : LocalNet M) (a b : U.algebra ∅) : a * b = b * a

The empty-region algebra 𝔘(∅) is commutative: it is *-isomorphic to ℂ via emptyEquivComplex, so its multiplication inherits commutativity from ℂ.

theorem Physicslib4.AQFT.HaagKastlerCurved.LocalNet.finrank_algebra_empty {M : LorentzianSpacetime} (U : LocalNet M) : Module.finrank ℂ (U.algebra ∅) = 1

The empty-region algebra 𝔘(∅) is one-dimensional over ℂ.