Directedness of the Alexandrov basis of standard Minkowski spacetime

Any two Alexandrov-basis "diamonds" I⁺(p₁) ∩ I⁻(q₁) and I⁺(p₂) ∩ I⁻(q₂) of standard Minkowski spacetime are contained in a common diamond. This is the geometric prerequisite for showing the union of local images in a quasilocal algebra is directed (and hence a *-subalgebra), needed to lift the covariance action.

Main results

• Physicslib4.Spacetime.minkowskiForwardCone_subset / minkowskiBackwardCone_subset: transitivity (nesting) of the coordinate forward / backward Minkowski cones.
• Physicslib4.Spacetime.exists_common_past / exists_common_future: any two points have a common chronological predecessor / successor.
• Physicslib4.Spacetime.alexandrovBasis_directed: directedness of the Alexandrov basis under inclusion.

theorem Physicslib4.Spacetime.minkowskiForwardCone_subset {p p' : SpacetimeModel} (h : p' ∈ minkowskiForwardCone p) : minkowskiForwardCone p' ⊆ minkowskiForwardCone p

Forward-cone transitivity. If p' ∈ I⁺(p) then I⁺(p') ⊆ I⁺(p).

theorem Physicslib4.Spacetime.minkowskiBackwardCone_subset {q q' : SpacetimeModel} (h : q' ∈ minkowskiBackwardCone q) : minkowskiBackwardCone q' ⊆ minkowskiBackwardCone q

Backward-cone transitivity. If q' ∈ I⁻(q) then I⁻(q') ⊆ I⁻(q).

theorem Physicslib4.Spacetime.exists_common_past (p₁ p₂ : SpacetimeModel) : ∃ (p : SpacetimeModel), p₁ ∈ minkowskiForwardCone p ∧ p₂ ∈ minkowskiForwardCone p

Existence of a common chronological predecessor. Any two points lie in the chronological future of a single point.

theorem Physicslib4.Spacetime.exists_common_future (q₁ q₂ : SpacetimeModel) : ∃ (q : SpacetimeModel), q₁ ∈ minkowskiBackwardCone q ∧ q₂ ∈ minkowskiBackwardCone q

Existence of a common chronological successor. Any two points lie in the chronological past of a single point.

theorem Physicslib4.Spacetime.alexandrovBasis_directed {B₁ B₂ : Set SpacetimeModel} (h₁ : B₁ ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation) (h₂ : B₂ ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation) : ∃ B ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation, B₁ ⊆ B ∧ B₂ ⊆ B

Directedness of the Alexandrov basis. Any two Alexandrov-basis diamonds of standard Minkowski spacetime are contained in a common diamond.

The Alexandrov diamonds form a genuine topological basis on standard Minkowski

theorem Physicslib4.Spacetime.exists_past_between_standardMinkowski {p₁ p₂ x : SpacetimeModel} (h₁ : x ∈ minkowskiForwardCone p₁) (h₂ : x ∈ minkowskiForwardCone p₂) : ∃ a ∈ minkowskiForwardCone p₁, a ∈ minkowskiForwardCone p₂ ∧ x ∈ minkowskiForwardCone a

Past interpolation. If x is in the forward cones of p₁ and p₂, there is a point a in both forward cones with x in the forward cone of a (i.e. p₁, p₂ ≪ a ≪ x). Take a = x - ε • e₀ for small ε > 0: the spatial separation from each pᵢ is unchanged, so the timelike condition survives, and x - a = ε e₀ is future-timelike.

theorem Physicslib4.Spacetime.exists_future_between_standardMinkowski {q₁ q₂ x : SpacetimeModel} (h₁ : x ∈ minkowskiBackwardCone q₁) (h₂ : x ∈ minkowskiBackwardCone q₂) : ∃ b ∈ minkowskiBackwardCone q₁, b ∈ minkowskiBackwardCone q₂ ∧ x ∈ minkowskiBackwardCone b

Future interpolation. If x is in the backward cones of q₁ and q₂, there is a point b in both backward cones with x in the backward cone of b (i.e. x ≪ b ≪ q₁, q₂). Dual to exists_past_between_standardMinkowski, with b = x + ε • e₀.

theorem Physicslib4.Spacetime.alexandrovBasis_exists_subset_inter_standardMinkowski (B₁ : Set SpacetimeModel) (h₁ : B₁ ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation) (B₂ : Set SpacetimeModel) (h₂ : B₂ ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation) (x : SpacetimeModel) (hx : x ∈ B₁ ∩ B₂) : ∃ B₃ ∈ StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation, x ∈ B₃ ∧ B₃ ⊆ B₁ ∩ B₂

Downward intersection property of the diamonds. For two Alexandrov diamonds of standard Minkowski and a point x in their intersection, there is a diamond B₃ with x ∈ B₃ ⊆ B₁ ∩ B₂. Uses past/future interpolation to build B₃ = I⁺(a) ∩ I⁻(b) and cone-nesting for the containment.

theorem Physicslib4.Spacetime.isTopologicalBasis_alexandrovBasis_standardMinkowski : TopologicalSpace.IsTopologicalBasis (StandardMinkowskiSpacetime.alexandrovBasis standardMinkowskiTimeOrientation)

The Alexandrov diamonds are a topological basis on standard Minkowski. Unconditionally: covering holds because every point has a chronological past and future point, and the downward intersection property is alexandrovBasis_exists_subset_inter_standardMinkowski; the generation condition is definitional.