Physicslib4.Spacetime.LorentzianSpacetime

Lorentzian spacetime

This file formalises the blueprint declaration def:lorentzian-spacetime (Chapter 10, sections/sec10/spacetime, of the AQFT-in-Lean blueprint; the notion is also discussed expositorily in the Chapter 9 prologue):

A Lorentzian spacetime is a smooth, connected, four-dimensional manifold equipped with a smooth, nowhere-vanishing global vector field tᵃ and associated Lorentzian metric. In addition it is equipped with an associated Hausdorff Alexandrov topology.

Main definitions

• Physicslib4.Spacetime.LorentzianSpacetime: the bundled curved-spacetime object (def:lorentzian-spacetime, Chapter 10).

Modelling notes

The three ingredients of the blueprint definition are already available individually in this development, so the bundle simply records them together:

• the smooth, connected, four-dimensional Hausdorff manifold with its smooth, non-degenerate, symmetric Lorentzian (0,2) metric is the existing Physicslib4.Spacetime structure (def:spacetime);
• the smooth, nowhere-vanishing global timelike vector field tᵃ is a Physicslib4.Spacetime.TimeOrientation on that spacetime (field + nonvanishing + timelike_at + smooth);
• the Hausdorff Alexandrov topology assumption is the field alexandrov_t2, asserting that the Alexandrov topology alexandrovTopology toSpacetime timeOrientation — generated by the diamonds I⁺(p) ∩ I⁻(q) — is T2.

By the blueprint's "Properties of the Alexandrov Topology" theorem the Hausdorff-Alexandrov assumption is equivalent to strong causality and to the agreement of the Alexandrov and manifold topologies; we take the Hausdorff form as the primitive assumption, exactly as the Chapter 9 prologue does.

This bundle is the concrete object that instantiates the abstract Physicslib4.AQFT.HaagKastlerCurved.LorentzianSpacetime interface over which Axioms 1-5 are stated, via LorentzianSpacetime.toAbstractIdentityComponent (Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean).

structure Physicslib4.Spacetime.LorentzianSpacetime : Type 1

A Lorentzian spacetime: a spacetime with a time orientation whose Alexandrov topology is Hausdorff.

It bundles a spacetime (toSpacetime), a time orientation t (timeOrientation), and the condition that the Alexandrov topology, generated by the diamonds I⁺(p) ∩ I⁻(q) for t, is Hausdorff (alexandrov_t2). The Hausdorff condition is a causality condition: it is equivalent to strong causality, and to the Alexandrov topology agreeing with the manifold topology (the theorem "Properties of the Alexandrov Topology" of the blueprint's chapter 9, which is context and is not formalised). It holds for Minkowski spacetime (alexandrov_eq_euclidean_standardMinkowski).

The causal notions of Spacetime are restated for the bundled time orientation, for example LorentzianSpacetime.IsBasisSet, LorentzianSpacetime.IsCompletelySpacelike and LorentzianSpacetime.spacelikeComplement. The Haag–Kastler axioms in curved spacetime are stated over an abstract interface, AQFT.HaagKastlerCurved.LorentzianSpacetime, which this structure instantiates through LorentzianSpacetime.toAbstractIdentityComponent.

Blueprint: def:lorentzian-spacetime

• toSpacetime : Spacetime

  The underlying spacetime: a connected four-dimensional manifold with a Lorentzian metric.

• timeOrientation : self.toSpacetime.TimeOrientation

  The time orientation t: a smooth, nowhere-vanishing, everywhere timelike vector field that fixes the future half of each light cone.

• alexandrov_t2 : T2Space self.toSpacetime.Carrier

  The Alexandrov topology for t, generated by the diamonds I⁺(p) ∩ I⁻(q), is Hausdorff.

  This is equivalent to strong causality, and to the Alexandrov topology agreeing with the manifold topology (a standard result, not formalised here).

@[reducible, inline]

abbrev Physicslib4.Spacetime.LorentzianSpacetime.Carrier (M : LorentzianSpacetime) : Type

The points of the Lorentzian spacetime.

Equations

• M.Carrier = M.toSpacetime.Carrier

def Physicslib4.Spacetime.LorentzianSpacetime.IsBasisSet (M : LorentzianSpacetime) (B : Set M.Carrier) : Prop

A region B is a basis set: a chronological diamond I⁺(p) ∩ I⁻(q) of the Lorentzian spacetime, for its time orientation.

These are the regions to which the curved-spacetime Haag–Kastler axioms assign local algebras.

Equations

• M.IsBasisSet B = (B ∈ M.toSpacetime.alexandrovBasis M.timeOrientation)

def Physicslib4.Spacetime.LorentzianSpacetime.IsCompletelySpacelike (M : LorentzianSpacetime) (O₁ O₂ : Set M.Carrier) : Prop

Two regions of a Lorentzian spacetime are completely spacelike, for its time orientation: every point of O₁ is spacelike related to every point of O₂.

This is Spacetime.IsCompletelySpacelike for the bundled time orientation, the separation under which Axiom 3 (local commutativity) makes the local algebras commute.

Equations

• M.IsCompletelySpacelike O₁ O₂ = M.toSpacetime.IsCompletelySpacelike M.timeOrientation O₁ O₂

instance Physicslib4.Spacetime.LorentzianSpacetime.instT2SpaceAlexandrov (M : LorentzianSpacetime) : T2Space M.Carrier

The Alexandrov topology of the Lorentzian spacetime is Hausdorff, re-exposed from the structure field as a T2Space instance on the carrier with the Alexandrov topology.

theorem Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_comm (M : LorentzianSpacetime) {O₁ O₂ : Set M.Carrier} : M.IsCompletelySpacelike O₁ O₂ ↔ M.IsCompletelySpacelike O₂ O₁

Complete spacelike separation of two regions is symmetric.

theorem Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_mono (M : LorentzianSpacetime) {O₁ O₁' O₂ O₂' : Set M.Carrier} (h₁ : O₁' ⊆ O₁) (h₂ : O₂' ⊆ O₂) (h : M.IsCompletelySpacelike O₁ O₂) : M.IsCompletelySpacelike O₁' O₂'

Complete spacelike separation is monotone under shrinking either region.

@[simp]

theorem Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_empty_left (M : LorentzianSpacetime) (O : Set M.Carrier) : M.IsCompletelySpacelike ∅ O

@[simp]

theorem Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_empty_right (M : LorentzianSpacetime) (O : Set M.Carrier) : M.IsCompletelySpacelike O ∅

theorem Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_union_left (M : LorentzianSpacetime) (O₁ O₁' O₂ : Set M.Carrier) : M.IsCompletelySpacelike (O₁ ∪ O₁') O₂ ↔ M.IsCompletelySpacelike O₁ O₂ ∧ M.IsCompletelySpacelike O₁' O₂

A union of regions is completely spacelike to O₂ iff each part is.

theorem Physicslib4.Spacetime.LorentzianSpacetime.isCompletelySpacelike_union_right (M : LorentzianSpacetime) (O₁ O₂ O₂' : Set M.Carrier) : M.IsCompletelySpacelike O₁ (O₂ ∪ O₂') ↔ M.IsCompletelySpacelike O₁ O₂ ∧ M.IsCompletelySpacelike O₁ O₂'

O₁ is completely spacelike to a union iff it is to each part.

theorem Physicslib4.Spacetime.LorentzianSpacetime.isOpen_alexandrov_of_isBasisSet (M : LorentzianSpacetime) {B : Set M.Carrier} (hB : M.IsBasisSet B) : IsOpen B

Every Alexandrov-basis set I⁺(p) ∩ I⁻(q) is open in the Alexandrov topology of the Lorentzian spacetime.

The Alexandrov diamonds as a genuine topological basis

theorem Physicslib4.Spacetime.LorentzianSpacetime.sUnion_alexandrovBasis_eq_univ (M : LorentzianSpacetime) [Nontrivial M.Carrier] : ⋃₀ M.toSpacetime.alexandrovBasis M.timeOrientation = Set.univ

Covering from the Hausdorff assumption. On a Lorentzian spacetime with at least two points, the Alexandrov diamonds cover the whole space: every point lies in some diamond I⁺(p) ∩ I⁻(q). A point in no diamond would have univ as its only Alexandrov-open neighbourhood, contradicting Hausdorffness.

theorem Physicslib4.Spacetime.LorentzianSpacetime.isTopologicalBasis_alexandrovBasis (M : LorentzianSpacetime) [Nontrivial M.Carrier] (hdir : ∀ B₁ ∈ M.toSpacetime.alexandrovBasis M.timeOrientation, ∀ B₂ ∈ M.toSpacetime.alexandrovBasis M.timeOrientation, ∀ x ∈ B₁ ∩ B₂, ∃ B₃ ∈ M.toSpacetime.alexandrovBasis M.timeOrientation, x ∈ B₃ ∧ B₃ ⊆ B₁ ∩ B₂) : TopologicalSpace.IsTopologicalBasis (M.toSpacetime.alexandrovBasis M.timeOrientation)

The Alexandrov diamonds form a topological basis. On a Lorentzian spacetime with at least two points, if the diamonds have the intersection property (hdir: every point of the intersection of two diamonds lies in a diamond inside that intersection), they form a genuine IsTopologicalBasis for the Alexandrov topology. The covering condition is sUnion_alexandrovBasis_eq_univ; the generation condition is definitional.

In the standard theory the intersection property holds in every spacetime, since chronological futures are open in the manifold topology; this is not proved in the library, so it is a hypothesis here. On standard Minkowski spacetime it is proved (alexandrovBasis_exists_subset_inter_standardMinkowski).