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 a LocalNet M (Axiom 1 data) plus proofs of Isotony, LocalCommutativity, LocalAlgebra, and IsometricCovariance.

Notes

• As in the Minkowski case, joint satisfiability of the axioms is witnessed by the trivial net (every region ↦ ℂ) over a trivial Lorentzian spacetime, giving Nonempty (Σ M, HaagKastlerNet M).

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

A Haag-Kastler net on (the Alexandrov-basis sets of) a Lorentzian spacetime M: the data of Axiom 1 (def:local-algebras-in-curved-spacetime) together with proofs of Axioms 2-5.

Blueprint reference: def:haag-kastler-net-in-curved-spacetime.

• U : LocalNet M

  The underlying assignment B ↦ 𝔘(B) (Axiom 1).

• isotony : Isotony self.U

  Isotony: the chosen functorial family of unital *-monomorphisms implementing inclusions of basis sets (Axiom 2). This is data, carrying the identity and composition laws.

• localCommutativity : LocalCommutativity self.U self.isotony

  Local commutativity: completely-spacelike basis sets commute inside any common containing basis algebra (Axiom 3). This consumes the Axiom 2 family rather than introducing its own: it asserts only the commutation condition.

• localAlgebra : LocalAlgebra self.U

  Local algebra: all observables are local observables (Axiom 4).

• isometricCovariance : IsometricCovariance self.U

  Isometric covariance: the identity-component isometry group acts on the net and commutes with isotony (Axiom 5).

@[reducible, inline]

abbrev Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.algebra {M : LorentzianSpacetime} (N : HaagKastlerNet M) (B : Set M.Carrier) : Type

The local algebra 𝔘(B) assigned by the net to a region B (the Axiom 1 data, via the underlying LocalNet M).

Equations

• N.algebra B = N.U.algebra B

noncomputable def Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.emptyEquivComplex {M : LorentzianSpacetime} (N : HaagKastlerNet M) : N.algebra ∅ ≃⋆ₐ[ℂ] ℂ

Net-level normalisation 𝔘(∅) ≃⋆ₐ[ℂ] ℂ.

Equations

• N.emptyEquivComplex = N.U.emptyEquivComplex

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

The empty-region algebra 𝔘(∅) is commutative.

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

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

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isotony_refl {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} : ∃ (φ : N.algebra B →⋆ₐ[ℂ] N.algebra B), Function.Injective ⇑φ

Isotony, reflexivity. Every Alexandrov-basis set embeds into itself via the identity unital *-monomorphism.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isotony_trans {M : LorentzianSpacetime} (N : HaagKastlerNet M) ⦃B₁ B₂ B₃ : Set M.Carrier⦄ (hB₁ : M.IsBasisSet B₁) (hB₂ : M.IsBasisSet B₂) (hB₃ : M.IsBasisSet B₃) (h₁₂ : B₁ ⊆ B₂) (h₂₃ : B₂ ⊆ B₃) : ∃ (φ : N.algebra B₁ →⋆ₐ[ℂ] N.algebra B₃), Function.Injective ⇑φ

Isotony, transitivity. For inclusions B₁ ⊆ B₂ ⊆ B₃ of Alexandrov-basis sets, the net's isotony embeddings compose to a unital *-monomorphism 𝔘(B₁) ↪ 𝔘(B₃).

noncomputable def Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.covEquiv {M : LorentzianSpacetime} (N : HaagKastlerNet M) (φ : M.Isom) (B : Set M.Carrier) : N.algebra B ≃⋆ₐ[ℂ] N.algebra (φ • B)

The covariance equivalence 𝔘(B) ≃⋆ₐ[ℂ] 𝔘(φ·B) implementing the action of an identity-component isometry φ on the net, chosen from the existence witness provided by Axiom 5 (isometricCovariance).

Equations

• N.covEquiv φ B = Exists.choose ⋯ φ B

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.finrank_algebra_smul {M : LorentzianSpacetime} (N : HaagKastlerNet M) (φ : M.Isom) (B : Set M.Carrier) : Module.finrank ℂ (N.algebra B) = Module.finrank ℂ (N.algebra (φ • B))

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).

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.norm_covEquiv {M : LorentzianSpacetime} (N : HaagKastlerNet M) (φ : M.Isom) {B : Set M.Carrier} (a : N.algebra B) : ‖(N.covEquiv φ B) a‖ = ‖a‖

Isometry invariance of the local norm. The covariance equivalence is a *-isomorphism of C*-algebras, hence isometric: ‖α a‖ = ‖a‖.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.commute_covEquiv_iff {M : LorentzianSpacetime} (N : HaagKastlerNet M) (φ : M.Isom) {B : Set M.Carrier} (a b : N.algebra B) : Commute ((N.covEquiv φ B) a) ((N.covEquiv φ B) b) ↔ Commute a b

Isometric transport of commutativity. Two local elements commute iff their images under the covariance equivalence commute.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.covEquiv_one {M : LorentzianSpacetime} (N : HaagKastlerNet M) (B : Set M.Carrier) (a : N.algebra B) : (N.covEquiv 1 B) a = ⋯.mp a

Covariance, identity. The action of the identity isometry is the identity automorphism (modulo the canonical identification 𝔘(B) = 𝔘(1·B) from one_smul).

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.covEquiv_mul {M : LorentzianSpacetime} (N : HaagKastlerNet M) (φ φ' : M.Isom) (B : Set M.Carrier) (a : N.algebra B) : (N.covEquiv (φ' * φ) B) a = ⋯.mp ((N.covEquiv φ' (φ • B)) ((N.covEquiv φ B) a))

Covariance, composition. The action is multiplicative in the group element: α (φ'·φ) = α φ' ∘ α φ (modulo the canonical identification 𝔘((φ'·φ)·B) = 𝔘(φ'·(φ·B)) from mul_smul).

noncomputable def Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.commIsotony {M : LorentzianSpacetime} (N : HaagKastlerNet M) ⦃B₁ B₂ : Set M.Carrier⦄ (h₁ : M.IsBasisSet B₁) (h₂ : M.IsBasisSet B₂) (h : B₁ ⊆ B₂) : N.U.algebra B₁ →⋆ₐ[ℂ] N.U.algebra B₂

The isotony embeddings of the net: the chosen family supplied by Axiom 2 (isotony).

Previously this was Classical.choosen from the Axiom 3 existence witness, which is why it carried no composition law and every consumer factoring a three-fold inclusion had to assume coherence separately. It is now literally the Axiom 2 family, so commIsotony_self and commIsotony_comp below hold for every net.

Equations

• N.commIsotony h₁ h₂ h = N.isotony.map h₁ h₂ h

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.commIsotony_injective {M : LorentzianSpacetime} (N : HaagKastlerNet M) ⦃B₁ B₂ : Set M.Carrier⦄ (h₁ : M.IsBasisSet B₁) (h₂ : M.IsBasisSet B₂) (h : B₁ ⊆ B₂) : Function.Injective ⇑(N.commIsotony h₁ h₂ h)

Each chosen isotony embedding is injective.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.commIsotony_self {M : LorentzianSpacetime} (N : HaagKastlerNet M) ⦃B : Set M.Carrier⦄ (h : M.IsBasisSet B) : N.commIsotony h h ⋯ = StarAlgHom.id ℂ (N.U.algebra B)

Identity law for the isotony embeddings, from Axiom 2.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.commIsotony_comp {M : LorentzianSpacetime} (N : HaagKastlerNet M) ⦃B₁ B₂ B₃ : Set M.Carrier⦄ (h₁ : M.IsBasisSet B₁) (h₂ : M.IsBasisSet B₂) (h₃ : M.IsBasisSet B₃) (h₁₂ : B₁ ⊆ B₂) (h₂₃ : B₂ ⊆ B₃) : (N.commIsotony h₂ h₃ h₂₃).comp (N.commIsotony h₁ h₂ h₁₂) = N.commIsotony h₁ h₃ ⋯

Composition law for the isotony embeddings, from Axiom 2: the embedding along B₁ ⊆ B₃ factors through any intermediate B₂.

This is the coherence that was previously carried as an ad hoc hypothesis at every site factoring a three-fold inclusion B₁ ⊆ B₂ ⊆ B; it now holds for every net, including the trivial one.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.commute_of_spacelike {M : LorentzianSpacetime} (N : HaagKastlerNet M) ⦃B₁ B₂ B : Set M.Carrier⦄ (hB₁ : M.IsBasisSet B₁) (hB₂ : M.IsBasisSet B₂) (hB : M.IsBasisSet B) (hs : M.IsCompletelySpacelike B₁ B₂) (h₁ : B₁ ⊆ B) (h₂ : B₂ ⊆ B) (a : N.algebra B₁) (b : N.algebra B₂) : Commute ((N.commIsotony hB₁ hB h₁) a) ((N.commIsotony hB₂ hB h₂) b)

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.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.commute_of_spacelike_symm {M : LorentzianSpacetime} (N : HaagKastlerNet M) ⦃B₁ B₂ B : Set M.Carrier⦄ (hB₁ : M.IsBasisSet B₁) (hB₂ : M.IsBasisSet B₂) (hB : M.IsBasisSet B) (hs : M.IsCompletelySpacelike B₁ B₂) (h₁ : B₁ ⊆ B) (h₂ : B₂ ⊆ B) (a : N.algebra B₁) (b : N.algebra B₂) : Commute ((N.commIsotony hB₂ hB h₂) b) ((N.commIsotony hB₁ hB h₁) a)

Local commutativity is symmetric. Commutation of completely-spacelike local algebras inside a common containing basis algebra holds in either order.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.commute_of_spacelike_mono {M : LorentzianSpacetime} (N : HaagKastlerNet M) (mono : ∀ ⦃O₁ O₁' O₂ O₂' : Set M.Carrier⦄, O₁' ⊆ O₁ → O₂' ⊆ O₂ → M.IsCompletelySpacelike O₁ O₂ → M.IsCompletelySpacelike O₁' O₂') ⦃B₁ B₂ B₁' B₂' B : Set M.Carrier⦄ (hB₁' : M.IsBasisSet B₁') (hB₂' : M.IsBasisSet B₂') (hB : M.IsBasisSet B) (hs : M.IsCompletelySpacelike B₁ B₂) (hsub₁ : B₁' ⊆ B₁) (hsub₂ : B₂' ⊆ B₂) (h₁ : B₁ ⊆ B) (h₂ : B₂ ⊆ B) (a : N.algebra B₁') (b : N.algebra B₂') : Commute ((N.commIsotony hB₁' hB ⋯) a) ((N.commIsotony hB₂' hB ⋯) b)

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.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isLocalObservable_of_isSelfAdjoint {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) (hB : M.IsBasisSet B) (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) (hmem : T ∈ Set.range ⇑π) : IsLocalObservable π T

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.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isLocalObservable_one {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) : IsLocalObservable π 1

The identity operator is a local observable of the net.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isLocalObservable_add {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) {S T : H →L[ℂ] H} (hS : IsLocalObservable π S) (hT : IsLocalObservable π T) : IsLocalObservable π (S + T)

The net's local observables are closed under addition.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isLocalObservable_smul {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) {c : ℂ} {T : H →L[ℂ] H} (hT : IsLocalObservable π T) (hc : IsSelfAdjoint c) : IsLocalObservable π (c • T)

The net's local observables are closed under scaling by a self-adjoint (i.e. real) complex scalar.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isLocalObservable_smul_add_smul {M : LorentzianSpacetime} (N : HaagKastlerNet M) {B : Set M.Carrier} {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) {c d : ℂ} {S T : H →L[ℂ] H} (hc : IsSelfAdjoint c) (hd : IsSelfAdjoint d) (hS : IsLocalObservable π S) (hT : IsLocalObservable π T) : IsLocalObservable π (c • S + d • T)

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.

def Physicslib4.AQFT.HaagKastlerCurved.trivialSpacetime : LorentzianSpacetime

A trivial Lorentzian spacetime used purely to witness joint satisfiability of the axioms: a one-point carrier, every set a basis set, trivial spacelike relation, and the trivial isometry group.

Equations

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

noncomputable def Physicslib4.AQFT.HaagKastlerCurved.trivialLocalNet (M : LorentzianSpacetime) : LocalNet M

The trivial local net over any abstract Lorentzian spacetime: every region is assigned the C*-algebra ℂ, with the empty-region normalisation the identity isomorphism.

Equations

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

def Physicslib4.AQFT.HaagKastlerCurved.trivialLocalNetIsotony (M : LorentzianSpacetime) : Isotony (trivialLocalNet M)

The trivial net's Axiom 2 data: every local algebra is ℂ and every inclusion is implemented by the identity, which is trivially functorial.

Equations

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

theorem Physicslib4.AQFT.HaagKastlerCurved.trivialLocalNet_localCommutativity (M : LorentzianSpacetime) : LocalCommutativity (trivialLocalNet M) (trivialLocalNetIsotony M)

theorem Physicslib4.AQFT.HaagKastlerCurved.trivialLocalNet_localAlgebra (M : LorentzianSpacetime) : LocalAlgebra (trivialLocalNet M)

theorem Physicslib4.AQFT.HaagKastlerCurved.trivialLocalNet_isometricCovariance (M : LorentzianSpacetime) : IsometricCovariance (trivialLocalNet M)

noncomputable def Physicslib4.AQFT.HaagKastlerCurved.trivialHaagKastlerNet (M : LorentzianSpacetime) : HaagKastlerNet M

The trivial net over any abstract Lorentzian spacetime, bundled as a Haag-Kastler net.

Equations

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

theorem Physicslib4.AQFT.HaagKastlerCurved.nonempty_haagKastlerNet (M : LorentzianSpacetime) : Nonempty (HaagKastlerNet M)

The curved-spacetime Haag-Kastler axioms are jointly satisfiable over every Lorentzian spacetime. The trivial net (every region ↦ ℂ) is a Haag-Kastler net.