Lorentzian spacetime

This file formalises the blueprint declaration def:lorentzian-spacetime (Chapter 10, sections/sec10/10-2_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 intended to instantiate the abstract Physicslib4.AQFT.HaagKastlerCurved.LorentzianSpacetime interface over which Axioms 1-5 are stated. The remaining ingredient for that bridge is the identity-component isometry group of the spacetime (used by Axiom 5), which is developed separately.

structure Physicslib4.Spacetime.LorentzianSpacetime : Type 1

Lorentzian spacetime (blueprint def:lorentzian-spacetime).

A smooth, connected, four-dimensional Hausdorff manifold with a smooth non-degenerate symmetric Lorentzian metric (toSpacetime), equipped with a smooth nowhere-vanishing global timelike vector field (timeOrientation) and an associated Hausdorff Alexandrov topology (alexandrov_t2).

This is the geometric bundle; LorentzianSpacetime.toAbstract exposes it as the axiom-facing interface Physicslib4.AQFT.HaagKastlerCurved.LorentzianSpacetime over which the curved Haag-Kastler axioms are stated.

Blueprint reference: def:lorentzian-spacetime.

• toSpacetime : Spacetime

  The underlying spacetime: a 4D connected smooth Hausdorff manifold with a smooth non-degenerate symmetric Lorentzian metric (def:spacetime).

• timeOrientation : self.toSpacetime.TimeOrientation

  The smooth, nowhere-vanishing, everywhere-timelike global vector field tᵃ orienting time.

• alexandrov_t2 : T2Space self.toSpacetime.Carrier

  The associated Alexandrov topology (generated by the diamonds I⁺(p) ∩ I⁻(q)) is Hausdorff. By the Alexandrov-topology theorem this is equivalent to strong causality and to the Alexandrov topology agreeing with the manifold topology.

@[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

The Alexandrov-basis sets I⁺(p) ∩ I⁻(q) of the Lorentzian spacetime, as a predicate on subsets of the carrier.

Equations

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

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

Complete spacelike separation of two regions, with respect to the spacetime's time orientation (used by Axiom 3).

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 are downward-directed (the intersection property), they form a genuine IsTopologicalBasis for the Alexandrov topology. The covering condition is sUnion_alexandrovBasis_eq_univ; the generation condition is definitional.