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.
Supporting lemmas #
isCausallyComplete_causalClosure— the causal closure of any region is causally complete, an immediate corollary ofisCausallyComplete_spacelikeComplement.spacelikeComplement_spacelikeComplement_of_isCausallyComplete— restatesIsCausallyCompleteas an involution equation,B^⊥⊥ = B.
The spacelike complement B⊥ of a region B, for a time orientation t: the points spacelike related to every point of B.
A point x lies in B⊥ when {x} and B are completely spacelike, that is, when no causal trip joins
x to any point of B in either direction. Since no point is spacelike related to itself,
B ∩ B⊥ = ∅ (disjoint_spacelikeComplement); B⊥ is causally convex
(spacelikeComplement_isCausallyConvex). The same construction on a Lorentzian spacetime, with
its own time orientation, is LorentzianSpacetime.spacelikeComplement, which carries the
lattice theory.
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 is causally convex. If p and r are spacelike to
all of B and p ≺ q ≺ r, then q is spacelike to all of B, by transitivity of
causal precedence.
A region and its spacelike complement are disjoint, B ∩ B^⊥ = ∅, since no point
is spacelike to itself (isSpacelikeRelated_irrefl).
The spacelike complement B⊥ of a region B of a Lorentzian spacetime: the points spacelike related to every point of B.
By Einstein causality, observables localised in B⊥ commute with those localised in B: B⊥ is the
geometric side of locality and of Haag duality. Complementation is antitone
(spacelikeComplement_antitone), B ⊆ B⊥⊥ (subset_spacelikeComplement_spacelikeComplement),
B⊥⊥⊥ = B⊥ (spacelikeComplement_spacelikeComplement_spacelikeComplement) and B ∩ B⊥ = ∅
(disjoint_spacelikeComplement). Moreover B₁ ⊆ B₂⊥ exactly when B₁ and B₂ are completely
spacelike (subset_spacelikeComplement_iff), so complementation is the Galois connection of the
relation "spacelike related". The spacelike complement of the whole spacetime is empty
(spacelikeComplement_univ), and that of the empty set is the whole spacetime.
Blueprint: def:spacelike-complement
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.
A region and its spacelike complement are disjoint, B ∩ B^⊥ = ∅, since no point
is spacelike to itself.
The complement of the whole spacetime is empty, since no point is spacelike to itself.
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.
Causal precedence is reflexive, so no point is spacelike to itself and
B ∩ B^⊥ = ∅ (disjoint_spacelikeComplement). The causal complement is therefore an
orthocomplementation: besides being an order-reversing involution, it satisfies
B ⊓ B^⊥ = ⊥ and B ⊔ B^⊥ = ⊤ (inf_causalComplement, sup_causalComplement).
The causal closure B ↦ B⊥⊥ of a region: its double spacelike complement, as a closure operator.
The causal closure is monotone, extensive (B ⊆ B⊥⊥) and idempotent (B⊥⊥⊥⊥ = B⊥⊥). Physically, B⊥⊥ is the largest region whose physics is determined by B through causality. In Minkowski spacetime, for example, the causal closure of a ball in a time slice is the double cone over the ball (a standard fact, not formalised here).
Implementation note: Mathlib's ClosureOperator bundles the three laws as fields, so they are
proved in constructing this term, from spacelikeComplement_antitone,
subset_spacelikeComplement_spacelikeComplement and
spacelikeComplement_spacelikeComplement_spacelikeComplement; causalClosure_apply unfolds it
to B⊥⊥.
Blueprint: def:causal-closure
Equations
- M.causalClosure = ClosureOperator.mk' (fun (B : Set M.Carrier) => M.spacelikeComplement (M.spacelikeComplement B)) ⋯ ⋯ ⋯
Instances For
A region B is causally complete: it equals its causal closure, B⊥⊥ = B.
The causally complete regions are the fixed points of causalClosure
(isCausallyComplete_iff_isClosed). Every spacelike complement B⊥ is causally complete
(isCausallyComplete_spacelikeComplement), causally complete regions are closed under
intersections and are causally convex (isCausallyConvex_of_isCausallyComplete). They are a
common choice of index set for the local algebras of algebraic quantum field theory; the
Haag–Kastler net of the library is indexed by diamonds instead.
Blueprint: def:causally-complete-region
Equations
- M.IsCausallyComplete B = (M.spacelikeComplement (M.spacelikeComplement B) = B)
Instances For
A region is causally complete iff it is a closed element of the causalClosure
closure operator.
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 type of causally complete regions of a Lorentzian spacetime, ordered by inclusion.
They form a complete lattice: the meet is the intersection, and the join of a family is the
causal closure of its union. The causal complement B ↦ B⊥ (causalComplement) is an
orthocomplementation of this lattice: an order-reversing involution with B ⊓ B⊥ = ⊥ and
B ⊔ B⊥ = ⊤ (inf_causalComplement, sup_causalComplement), so the De Morgan laws hold
(causalComplement_sup, causalComplement_iSup, ...).
Implementation note: the type is Mathlib's ClosureOperator.Closeds of causalClosure, so an
element is a pair of a set B and a proof that B⊥⊥ = B. The CompleteLattice instance is
transported from the closure operator along its Galois insertion
(ClosureOperator.gi) and is anonymous.
Blueprint: thrm:causally-complete-lattice
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 causal complement of a causally complete region B: its spacelike complement B⊥, again causally complete.
On the lattice CausallyCompleteRegion it is an order-reversing involution, (B⊥)⊥ = B
(causalComplement_causalComplement, causalComplement_antitone), and an orthocomplement:
B ⊓ B⊥ = ⊥ and B ⊔ B⊥ = ⊤ (inf_causalComplement, sup_causalComplement). The underlying set is
spacelikeComplement (causalComplement_coe).
Blueprint: thrm:causally-complete-lattice
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 causal complement is antitone: a larger causally complete region has a smaller (or equal) causal complement.
⊥^⊥ = ⊤: 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)^⊥.
Orthocomplementation #
Non-contradiction. A causally complete region meets its causal complement only in
the least region: B ⊓ B^⊥ = ⊥.
Excluded middle. A causally complete region and its causal complement join to the
greatest region: B ⊔ B^⊥ = ⊤.
Causally complete regions are causally convex #
A causally complete region is causally convex. Since B = B^⊥⊥ is a spacelike
complement (of B^⊥), it inherits causal convexity from
spacelikeComplement_isCausallyConvex.
Every element of the causally-complete-region lattice is causally convex.