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โ).
No coherence hypothesis is needed. The step this rests on is that the embedding
๐(Bโ) โ ๐(B) factors through ๐(Bโ), and that is now the composition law of
Axiom 2, available as commIsotony_comp. Formerly the embeddings in play were the
witnesses chosen inside Axiom 3, which carried no composition law, so this
factorisation had to be assumed as a separate hypothesis hcoh at every site.
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 gives
R(Bโ) โค R(Bโ), with no coherence side condition.
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โ).
This was formerly an assumption. The curved Axiom 3 used to select its own isotony
witnesses via Classical.choose, so the composition law was unavailable even for the
trivial net, whose witness is the identity but hidden behind a Classical.choose that
does not reduce. Axiom 2 now owns the isotony family and carries the composition law
as one of its fields, and Axiom 3 consumes that family, so this property holds for every
net โ see isIsotonyCoherentBelow immediately below. The definition is retained as a
name for the condition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every net is isotony-coherent below every region. Immediate from the composition
law of Axiom 2 (commIsotony_comp), read pointwise. This is what makes the former
hcoh hypotheses throughout this file redundant.
The net of von Neumann algebras as an order-preserving map (curved spacetime).
Fixing a containing basis region B and a representation ฯ of ๐(B), 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.
Monotonicity carries no coherence hypothesis. The factorisation it rests on is the
composition law of Axiom 2, discharged for every net by isIsotonyCoherentBelow.
Equations
- N.vonNeumannNet hB ฯ = { toFun := fun (B' : { B' : Set M.Carrier // M.IsBasisSet B' โง B' โ B }) => N.localVonNeumannAlgebra ฯ โฏ hB โฏ, monotone' := โฏ }
Instances For
The relative commutant of a nested pair R(Bโ) โ R(Bโ) of subregions of a
containing region B, in a representation ฯ of ๐(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โ). Curved counterpart
of the Minkowski relative commutant; the basic object of local-algebra inclusion
theory.
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 nested
basis subregions Bโ โ 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. No
coherence hypothesis is needed: the factorisation curved isotony requires is the
composition law of Axiom 2.
The inclusion R(Bโ) โ R(Bโ) of subregions of B is irreducible when its
relative commutant is trivial: R(Bโ)' โฉ R(Bโ) = โยท1. Curved counterpart of the
subfactor-theoretic notion of an irreducible inclusion.
Equations
- N.IsIrreducibleInclusion hB ฯ hBโ hBโ hโ hโ = (โ(N.relativeCommutant hB ฯ hBโ hBโ hโ hโ) = Physicslib4.scalarOperators H)
Instances For
An irreducible inclusion forces the ambient algebra to be a factor (curved
spacetime). For nested basis subregions Bโ โ Bโ โ B, if the inclusion
R(Bโ) โ R(Bโ) is irreducible then R(Bโ) is a factor. The
center R(Bโ) โฉ R(Bโ)' lies in the relative commutant (center_le_relativeCommutant),
which is the scalars by hypothesis; the scalars are always central, giving equality. No
coherence hypothesis is needed, by the composition law of Axiom 2.
Self-inclusion is irreducible iff the algebra is a factor (curved spacetime).
For a basis subregion B' โ B in a representation of ๐(B), the trivial self-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.
The center of a local von Neumann algebra is abelian (curved spacetime). For a
subregion B' โ B in a representation of ๐(B), the center R(B') โฉ R(B')' is abelian.
A thin specialization of the general vonNeumannCenter_isAbelian to the curved local
algebra R(B').
A local von Neumann algebra that is a factor is abelian iff it is the scalars
(curved spacetime). For a subregion B' โ B, if R(B') is a factor then it is abelian
exactly when R(B') = โยท1. A thin specialization of isAbelian_iff_eq_scalars_of_isFactor
to the curved local algebra.
A local von Neumann algebra shares its center with its commutant (curved spacetime).
Z(R(B')) = Z(R(B')'). A thin specialization of the general vonNeumannCenter_eq_commutant
to the curved local algebra.
A local von Neumann algebra is a factor iff its center is the scalars (curved
spacetime). A thin specialization of the general isFactor_iff_center_eq_scalars to the
curved local algebra R(B').