Physicslib4.AQFT.HaagKastlerCurved.Concrete

Bridging a concrete spacetime to the abstract Haag-Kastler interface

This file connects the concrete blueprint object Physicslib4.Spacetime.LorentzianSpacetime (def:lorentzian-spacetime) to the abstract interface Physicslib4.AQFT.HaagKastlerCurved.LorentzianSpacetime over which Axioms 1-5 are stated.

Main definitions

• Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent: the abstract interface induced by a concrete Lorentzian spacetime.

Modelling notes

The pieces of the abstract interface are read off the concrete spacetime:

• Carrier is the manifold's point set;
• IsBasisSet is membership in the Alexandrov basis of diamonds I⁺(p) ∩ I⁻(q);
• IsCompletelySpacelike is the spacelike-separation relation of the underlying spacetime, with respect to its chosen time orientation;
• Isom is the oriented identity component Spacetime.Isometry.orientedIdentityComponent (the topological connectedComponentOfOne intersected with future-orientation preservation), which is the blueprint's group of "isometries connected to the identity" in Axiom 5 (see the implementation note on toAbstractIdentityComponent);
• isBasisSet_smul is Spacetime.LorentzianSpacetime.isBasisSet_smul: these isometries carry Alexandrov diamonds to Alexandrov diamonds.

noncomputable def Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent (L : LorentzianSpacetime) : AQFT.HaagKastlerCurved.LorentzianSpacetime

The abstract spacetime interface of a geometric Lorentzian spacetime L, the bridge to the curved axioms.

The pieces of the interface are read off L. The points are those of the manifold. The basis sets are the causal diamonds I⁺(p) ∩ I⁻(q) of the Alexandrov topology for the time orientation of L. Two regions are completely spacelike when every point of the one is spacelike to every point of the other. The isometry group is the group of isometries of L connected to the identity, taken as the oriented identity component: the isometries in the identity component of the isometry group that also preserve the future orientation. These isometries carry diamonds to diamonds (Spacetime.LorentzianSpacetime.isBasisSet_smul), which supplies the one axiom of the interface. Every result proved over the interface, the curved axioms included, then applies to L.

Implementation note: the oriented identity component is the group of isometries connected to the identity named in the blueprint. That an isometry connected to the identity preserves the future orientation needs a Myers–Steenrod-type rigidity theorem that Mathlib does not provide, so orientation preservation is included in the definition of the group rather than proved.

Blueprint: def:abstract-lorentzian-spacetime-interface

Equations

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

@[simp]

theorem Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent_Carrier (L : LorentzianSpacetime) : L.toAbstractIdentityComponent.Carrier = L.Carrier

@[simp]

theorem Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent_IsBasisSet (L : LorentzianSpacetime) : L.toAbstractIdentityComponent.IsBasisSet = L.IsBasisSet

@[simp]

theorem Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent_IsCompletelySpacelike (L : LorentzianSpacetime) : L.toAbstractIdentityComponent.IsCompletelySpacelike = L.IsCompletelySpacelike

@[simp]

theorem Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent_Isom (L : LorentzianSpacetime) : L.toAbstractIdentityComponent.Isom = ↥(Isometry.orientedIdentityComponent L.toSpacetime L.timeOrientation)

The abstract isometry group of the bridge is, definitionally, the oriented identity component. Exposed as a simp lemma so abstract-interface statements can be rewritten to the concrete subgroup.

@[instance_reducible]

noncomputable instance Physicslib4.Spacetime.LorentzianSpacetime.instTopologicalSpaceToAbstractIdentityComponentIsom (L : LorentzianSpacetime) : TopologicalSpace L.toAbstractIdentityComponent.Isom

The topology on the isometry group of the bridge: the subspace topology of the oriented identity component.

The abstract interface carries no topology, so the strongly continuous stabilizer and KMS results take [TopologicalSpace M.Isom] as a hypothesis. Over a geometric spacetime this instance supplies it: the isometry group has the topology induced by φ ↦ (φ, φ⁻¹) into C(M, M) × C(M, M) with the compact-open topology, and the subgroup inherits it.

Equations

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

theorem Physicslib4.Spacetime.LorentzianSpacetime.toAbstractIdentityComponent_isBasisSet_smul (L : LorentzianSpacetime) (φ : L.toAbstractIdentityComponent.Isom) {B : Set L.toAbstractIdentityComponent.Carrier} (hB : L.toAbstractIdentityComponent.IsBasisSet B) : L.toAbstractIdentityComponent.IsBasisSet (φ • B)

Axiom 5 basis-set preservation, stated over the abstract bridge. Every isometry φ of the abstract spacetime carries Alexandrov-basis sets to basis sets: φ(𝐁) = φ • 𝐁 is again a basis set. This is the interface field isBasisSet_smul of the bridge.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.commute_of_spacelike_mono_geometric {L : Spacetime.LorentzianSpacetime} (N : HaagKastlerNet L.toAbstractIdentityComponent) ⦃B₁ B₂ B₁' B₂' B : Set L.toAbstractIdentityComponent.Carrier⦄ (hB₁' : L.toAbstractIdentityComponent.IsBasisSet B₁') (hB₂' : L.toAbstractIdentityComponent.IsBasisSet B₂') (hB : L.toAbstractIdentityComponent.IsBasisSet B) (hs : L.toAbstractIdentityComponent.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 over a concrete spacetime. The geometric specialisation of commute_of_spacelike_mono: for a Haag-Kastler net over the abstract interface induced by a concrete Lorentzian spacetime L, the spacelike-monotonicity hypothesis is discharged automatically by Spacetime.LorentzianSpacetime.isCompletelySpacelike_mono.

theorem Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement_geometric {L : Spacetime.LorentzianSpacetime} (N : HaagKastlerNet L.toAbstractIdentityComponent) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {B : Set L.toAbstractIdentityComponent.Carrier} (hB : L.toAbstractIdentityComponent.IsBasisSet B) (π : N.algebra B →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set L.toAbstractIdentityComponent.Carrier⦄ (hB₁ : L.toAbstractIdentityComponent.IsBasisSet B₁) (hB₂ : L.toAbstractIdentityComponent.IsBasisSet B₂) (hsub : B₁ ⊆ L.spacelikeComplement B₂) (h₁ : B₁ ⊆ B) (h₂ : B₂ ⊆ B) : N.localVonNeumannAlgebra π hB₁ hB h₁ ≤ (N.localVonNeumannAlgebra π hB₂ hB h₂).commutant

Additive-free locality over a concrete spacetime. The geometric specialisation of the curved additive-free locality: for a Haag-Kastler net over a concrete Lorentzian spacetime L, a bounded region B₁ lying in the spacelike complement of B₂ (both inside a common containing basis set B) has its local von Neumann algebra inside the commutant of R(B₂). The Galois bridge subset_spacelikeComplement_iff discharges the spacelike hypothesis; no algebra is attached to the unbounded complement.