Local von Neumann algebras and spacelike commutation (curved spacetime) #
This is the curved-spacetime counterpart of the Minkowski local von Neumann
algebra construction. There is no quasilocal algebra in curved spacetime, so the
relevant representations are of a containing basis algebra 𝔘(B). Given such a
representation π, the local von Neumann algebra of a subregion B' ⊆ B is the
bicommutant R(B') = π(𝔘(B'))'' of the local observable operators (the embedding
𝔘(B') → 𝔘(B) being the isotony witness commIsotony). Mathlib models the
commutant by Set.centralizer, so R(B') is the double centralizer.
The headline result is microcausality at the von Neumann level: for completely
spacelike-separated subregions B₁, B₂ ⊆ B, the local algebras commute,
R(B₁) ⊆ R(B₂)'. It is the von Neumann form of curved Einstein causality
(einstein_causality): elementwise commutation of the local operators, pushed
through the centralizer.
The local observable operators of a subregion B' ⊆ B in a representation π
of the containing algebra 𝔘(B): the image π(𝔘(B')) of the local algebra under
the isotony embedding.
Equations
- N.localOperators π hB' hB h = Set.range fun (a : N.algebra B') => π ((N.commIsotony hB' hB h) a)
Instances For
The local von Neumann algebra R(B') = π(𝔘(B'))'', the bicommutant of the
local observable operators (the commutant being Set.centralizer).
Equations
- N.localVonNeumann π hB' hB h = (N.localOperators π hB' hB h).centralizer.centralizer
Instances For
Microcausality at the von Neumann level (curved spacetime). For completely
spacelike-separated basis subregions B₁, B₂ ⊆ B, the local von Neumann algebras
commute: R(B₁) ⊆ R(B₂)'. This is the von Neumann form of curved Einstein
causality.
Isotony of the net of von Neumann algebras (curved spacetime). For nested
basis subregions B₁ ⊆ B₂ ⊆ B, the local von Neumann algebras are nested:
R(B₁) ⊆ R(B₂). Unlike Minkowski, the curved Axiom 3 isotony embeddings
(commIsotony) are chosen witnesses with no built-in composition law, so the
coherence commIsotony (B₁ ⊆ B) = commIsotony (B₂ ⊆ B) ∘ commIsotony (B₁ ⊆ B₂)
is taken as an explicit hypothesis hcoh (it is automatic whenever the embeddings
are coherent, e.g. for a net whose Axiom 3 witnesses come from a genuine inclusion
family). Given it, the local observables of B₁ embed into those of B₂ and the
double commutant is monotone.
Statistical independence (abstract form). If Ω is cyclic for a set S of
operators (the vectors T Ω, T ∈ S, are dense), then any operator R commuting
with every element of S and annihilating Ω is zero. Equivalently, Ω is
separating for the commutant of S.
Statistical independence (Schlieder property) for spacelike curved regions.
If Ω is cyclic for the local observables of B₁ - the role supplied in
Minkowski spacetime by Reeh-Schlieder - then a nonzero element of the
spacelike-separated local von Neumann algebra R(B₂) cannot annihilate Ω:
R Ω = 0 ⟹ R = 0. So Ω is separating for R(B₂), the operator-algebraic form
of the statistical independence of spacelike-separated local algebras.
The local observable operators π(𝔘(B')) form a self-adjoint set: π and the
isotony embedding commIsotony are *-homomorphisms.
The local von Neumann algebra R(B') as a genuine VonNeumannAlgebra: the
bicommutant of the self-adjoint set of local observable operators inside B(H).
Its underlying set is localVonNeumann π hB' hB h.
Equations
- N.localVonNeumannAlgebra π hB' hB h = Physicslib4.GNS.vonNeumannOfSelfAdjoint (N.localOperators π hB' hB h) ⋯
Instances For
Microcausality, bundled (curved spacetime). For completely spacelike-separated
subregions B₁, B₂ ⊆ B, the bundled local von Neumann algebras commute,
R(B₁) ≤ R(B₂)'.
Isotony, bundled (curved spacetime). B₁ ⊆ B₂ ⊆ B (with the isotony
coherence) gives R(B₁) ≤ R(B₂).
Statistical independence, bundled (curved spacetime). If Ω is cyclic for the
local observables of B₁, then Ω is separating for the bundled local von Neumann
algebra R(B₂) of a spacelike-separated subregion: any R ∈ R(B₂) with R Ω = 0 is
zero.
The chosen Axiom-3 isotony embeddings commIsotony are coherent below B:
for nested basis subregions B₁ ⊆ B₂ ⊆ B, the direct embedding 𝔘(B₁) → 𝔘(B) factors
through 𝔘(B₂).
Unlike Minkowski spacetime — whose QuasilocalAlgebra carries the ι_inclusion coherence
as data, making von Neumann isotony unconditional — the curved Axiom 3 selects its
isotony witnesses via Classical.choose (commIsotony). The composition law below is
therefore not available for free for any net: even the trivial net, whose witness is the
identity, hides it behind Classical.choose (which does not reduce to the witness), and
toAbstract does not touch the net's Axiom-3 data. It must be assumed; it holds for any
net whose Axiom-3 witnesses form a genuine inclusion family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The net of von Neumann algebras as an order-preserving map (curved spacetime).
Fixing a containing basis region B and a representation π of 𝔘(B), and assuming the
isotony embeddings are coherent below B (IsIsotonyCoherentBelow), the assignment
B' ↦ R(B') is a monotone map from the poset of basis subregions of B (ordered by
inclusion) to the von Neumann algebras of B(H). This is the curved counterpart of the
Minkowski vonNeumannNet: the local net restricted to a containing region is a functor on
the inclusion poset, sending containment of regions to containment of algebras.
The coherence enters as a single hypothesis rather than being discharged geometrically:
unlike spacelike-monotonicity (a spacetime fact discharged over toAbstract by
commute_of_spacelike_mono_geometric), it is a property of the net's chosen Axiom-3
embeddings, not of the underlying spacetime. The map is nonetheless unconditional in
that its monotonicity field carries no per-edge side condition.
Equations
- N.vonNeumannNet hB π hcoh = { toFun := fun (B' : { B' : Set M.Carrier // M.IsBasisSet B' ∧ B' ⊆ B }) => N.localVonNeumannAlgebra π ⋯ hB ⋯, monotone' := ⋯ }