Local von Neumann algebras and spacelike commutation #
In a representation π of the quasilocal algebra, the local von Neumann algebra
of a region B is the bicommutant R(B) = π(𝔘(B))'' of the local observable
operators. 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 regions B₁, B₂, the local algebras commute,
R(B₁) ⊆ R(B₂)'. It is the von Neumann form of Einstein causality
(einstein_causality): elementwise commutation of the local operators, pushed
through the centralizer.
The local observable operators of a region B in a representation π: the
image π(𝔘(B)) of the local algebra.
Equations
- N.localOperators π hB = Set.range fun (a : N.U.algebra B) => π ((N.commAlgebra.ι hB) 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 = (N.localOperators π hB).centralizer.centralizer
Instances For
Microcausality at the von Neumann level. For completely spacelike-separated
basis regions B₁, B₂, the local von Neumann algebras commute:
R(B₁) ⊆ R(B₂)'. This is the von Neumann form of Einstein causality.
Isotony of the net of von Neumann algebras. For basis regions B₁ ⊆ B₂,
the local von Neumann algebras are nested: R(B₁) ⊆ R(B₂). The local observables
of B₁ embed into those of B₂ via the quasilocal isotony coherence
(ι_inclusion), 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.
Statistical independence (Schlieder property), Minkowski spacetime. If Ω
is cyclic for the local observables of B₁ - in Minkowski spacetime this
cyclicity is supplied by the Reeh-Schlieder theorem - 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 cyclicity hypothesis is
the Reeh-Schlieder input (which rests on the spectrum condition); the implication
itself is elementary.
The local observable operators π(𝔘(B)) form a self-adjoint set: π and the
quasilocal embedding ι are *-homomorphisms, so star (π (ι B a)) = π (ι B (star a)).
The local von Neumann algebra R(B) as a genuine VonNeumannAlgebra: the
bicommutant of the self-adjoint set of local observable operators. Its underlying
set is localVonNeumann π B.
Equations
- N.localVonNeumannAlgebra π hB = Physicslib4.GNS.vonNeumannOfSelfAdjoint (N.localOperators π hB) ⋯
Instances For
Microcausality, bundled (Minkowski). For completely spacelike-separated
regions, R(B₁) ≤ R(B₂)' as von Neumann algebras (VonNeumannAlgebra.commutant).
Additive-free locality (Minkowski). A bounded region lying in the spacelike
complement of B has its local algebra inside the commutant of R(B): for basis
sets B' ⊆ B^⊥, R(B') ≤ R(B)'. This repackages microcausality through the
spacelike complement, keeping strictly to bounded (diamond) regions — no algebra is
attached to the unbounded complement.
Isotony, bundled (Minkowski). B₁ ⊆ B₂ ⟹ R(B₁) ≤ R(B₂) as von Neumann
algebras.
Statistical independence, bundled (Minkowski). If Ω is cyclic for the local
observables of B₁ (the Reeh-Schlieder input), then Ω is separating for the bundled
local von Neumann algebra R(B₂) of a spacelike-separated region: any R ∈ R(B₂) with
R Ω = 0 is zero.
The net of von Neumann algebras as an order-preserving map. Packaging
isotony, the assignment B ↦ R(B) is a monotone map from the poset of basis
regions (ordered by inclusion) to the von Neumann algebras of B(H). This is the
statement that the local net is a functor on the inclusion poset: containment of
regions is sent to containment of algebras.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Antitonicity of the commutant. For bundled von Neumann algebras
M₁ ≤ M₂ on H, the commutants reverse the inclusion: M₂' ≤ M₁'.
The relative commutant of a nested pair R(B₁) ⊆ R(B₂): the von Neumann
algebra R(B₁)' ∩ R(B₂), built as the meet of the star-subalgebras of the
commutant of R(B₁) and of R(B₂). Its underlying set is R(B₁)' ∩ R(B₂). This
is the basic object of the theory of local-algebra inclusions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The underlying set of the relative commutant is R(B₁)' ∩ R(B₂).
The relative commutant lies in the larger algebra: R(B₁)' ∩ R(B₂) ≤ R(B₂).
The relative commutant commutes with the smaller algebra: its underlying
set is contained in R(B₁)'.
The relative commutant contains the center of the ambient algebra. For
B₁ ⊆ B₂, the center R(B₂) ∩ R(B₂)' is contained in R(B₁)' ∩ R(B₂). Via
isotony R(B₁) ≤ R(B₂) and antitonicity of the commutant.
The inclusion R(B₁) ⊆ R(B₂) is irreducible when its relative commutant is
trivial: R(B₁)' ∩ R(B₂) = ℂ·1. This is the subfactor-theoretic notion of an
irreducible inclusion.
Equations
- N.IsIrreducibleInclusion π hB₁ hB₂ = (↑(N.relativeCommutant π hB₁ hB₂) = Physicslib4.scalarOperators H)
Instances For
An irreducible inclusion forces the ambient algebra to be a factor. If
B₁ ⊆ B₂ and the inclusion R(B₁) ⊆ R(B₂) is irreducible, then R(B₂) is a factor
(trivial center). The center R(B₂) ∩ R(B₂)' lies inside the relative commutant
(center_le_relativeCommutant), which is the scalars by hypothesis; and the scalars
are always central, giving equality.
Self-inclusion is irreducible iff the algebra is a factor. The trivial
inclusion R(B) ⊆ R(B) is irreducible exactly when R(B) is a factor: the relative
commutant of the self-inclusion is R(B)' ∩ R(B), i.e. the center of R(B) (up to the
order of intersection), which equals the scalars iff R(B) has trivial center. This is
the converse-completing companion to isFactor_of_isIrreducibleInclusion.