The causal (spacelike) complement of a region #
The spacelike complement B^⊥ of a region B in a Lorentzian spacetime is the
set of points completely spacelike-separated from all of B:
B^⊥ = { x | {x} is completely spacelike to B }.
This is the geometric substrate of locality and Haag duality in algebraic quantum field theory. We record its order structure:
spacelikeComplement_antitone—B₁ ⊆ B₂ ⇒ B₂^⊥ ⊆ B₁^⊥;subset_spacelikeComplement_spacelikeComplement—B ⊆ B^⊥⊥;spacelikeComplement_spacelikeComplement_spacelikeComplement—B^⊥⊥⊥ = B^⊥;subset_spacelikeComplement_iff— the Galois-type bridgeB₁ ⊆ B₂^⊥ ↔ B₁, B₂ completely spacelike.
The spacelike complement B^⊥ of a region B, with respect to a time
orientation t: the points completely spacelike-separated from all of B.
Equations
- M.spacelikeComplement t B = {x : M.Carrier | M.IsCompletelySpacelike t {x} B}
Instances For
Galois bridge. A region lies in the complement of another exactly when the two are completely spacelike-separated.
The spacelike complement B^⊥ of a region B: the points completely
spacelike-separated from all of B.
Equations
- M.spacelikeComplement B = {x : M.Carrier | M.IsCompletelySpacelike {x} B}
Instances For
Complete spacelike separation of a singleton from a region is pointwise.
The spacelike complement is antitone: enlarging a region shrinks its complement.
A region is contained in its double complement: B ⊆ B^⊥⊥.
The triple complement equals the complement: B^⊥⊥⊥ = B^⊥.
The complement of the empty region is everything.
Galois bridge. A region lies in the complement of another exactly when the two are completely spacelike-separated.
Causally complete regions and the causal closure operator #
The double complement B ↦ B^⊥⊥ is a closure operator on the regions of a
Lorentzian spacetime. Its fixed points — the causally complete regions — are
the natural regions of algebraic QFT, and they form a complete lattice on which
the spacelike complement ^⊥ acts as an order-reversing involution.
A caveat on orthocomplementation: the spacelike-separation relation used here is
irreflexive-causality based (a point is spacelike to itself, since there is no
degenerate closed causal trip), so B ∩ B^⊥ need not be empty and the full
orthocomplement law B ⊓ B^⊥ = ⊥ does not hold at this generality. What does
hold is the complete lattice with an order-reversing involution (a De Morgan
structure).
The causal closure operator B ↦ B^⊥⊥ on the regions of M: monotone,
extensive (B ⊆ B^⊥⊥), and idempotent (B^⊥⊥⊥⊥ = B^⊥⊥).
Equations
- M.causalClosure = ClosureOperator.mk' (fun (B : Set M.Carrier) => M.spacelikeComplement (M.spacelikeComplement B)) ⋯ ⋯ ⋯
Instances For
A region is causally complete if it equals its own double complement,
B^⊥⊥ = B (equivalently, it is a closed element of causalClosure).
Equations
- M.IsCausallyComplete B = (M.spacelikeComplement (M.spacelikeComplement B) = B)
Instances For
The spacelike complement of any region is causally complete: B^⊥⊥⊥ = B^⊥.
The causal closure B^⊥⊥ of any region is causally complete.
On causally complete regions the spacelike complement is an involution:
B^⊥⊥ = B.
The causally complete regions are closed under intersection (the lattice
meet): B₁^⊥⊥ = B₁ and B₂^⊥⊥ = B₂ imply (B₁ ∩ B₂)^⊥⊥ = B₁ ∩ B₂.
Arbitrary intersections of causally complete sets are causally complete.
The causally complete regions, i.e. the closed elements of the causal
closure operator (B^⊥⊥ = B). Ordered by inclusion.
Equations
Instances For
The causally complete regions form a complete lattice (meets are intersections; joins are causal closures of unions), transported from the causal closure operator via its Galois insertion.
The spacelike complement as an order-reversing involution on the complete lattice of causally complete regions (the causal complement).
Equations
- M.causalComplement B = ⟨M.spacelikeComplement ↑B, ⋯⟩
Instances For
Causal complementation is an involution: B^⊥⊥ = B on causally complete
regions.
De Morgan laws for the spacelike complement #
Binary De Morgan (set level). The spacelike complement turns a union into
an intersection: (B₁ ∪ B₂)^⊥ = B₁^⊥ ∩ B₂^⊥.
Infinitary De Morgan (set level). The spacelike complement turns an
indexed union into an intersection: (⋃ i, B i)^⊥ = ⋂ i, (B i)^⊥.
De Morgan laws for the causal complement #
On the complete lattice of causally complete regions the causal complement is an
order-reversing involution, hence satisfies the full De Morgan laws. The lattice
is not linearly ordered, so the equalities below rely on the involution
(causalComplement_causalComplement), not on antitonicity alone.
⊥^⊥ = ⊤: the complement of the least region is the greatest.
⊤^⊥ = ⊥: the complement of the greatest region is the least.
Binary De Morgan (join). (B₁ ⊔ B₂)^⊥ = B₁^⊥ ⊓ B₂^⊥.
Binary De Morgan (meet). (B₁ ⊓ B₂)^⊥ = B₁^⊥ ⊔ B₂^⊥.
Infinitary De Morgan (join). (⨆ i, B i)^⊥ = ⨅ i, (B i)^⊥.
Infinitary De Morgan (meet). (⨅ i, B i)^⊥ = ⨆ i, (B i)^⊥.