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 operators of a basis set B' โ B in a representation ฯ of ๐(B): the image ฯ(i(B', B)(๐(B'))).
Curved spacetime has no quasilocal algebra, so ฯ is a *-representation of the local algebra ๐(B) of a basis set B containing B', on a Hilbert space H, and the isotony embedding i(B', B) of Axiom 2 carries ๐(B') into ๐(B). The result is a set of bounded operators on H, written ฯ(๐(B')) for short.
Blueprint: def:local-von-neumann-in-curved-spacetime
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'))'' of a basis set B' โ B, as a set of operators.
The commutant S' of a set S of bounded operators is the set of bounded operators commuting with
every element of S, and the bicommutant S'' is the commutant of S'. By the bicommutant theorem of
von Neumann, ฯ(๐(B'))'' is the weak operator closure of the unital *-algebra ฯ(๐(B')), which it
generally contains strictly. Everything is relative to the representation ฯ of the containing
algebra ๐(B).
localVonNeumannAlgebra is the same set as a bundled von Neumann algebra.
Implementation note: the commutant is Mathlib's Set.centralizer in the bounded operators on H.
Blueprint: def:local-von-neumann-in-curved-spacetime
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 embedding ๐(Bโ) โ ๐(B) factors through
๐(Bโ) by the composition law of Axiom 2, commIsotony_comp.
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') = ฯ(๐(B'))'' of a basis set B' โ B, as a von Neumann algebra.
The local operators ฯ(๐(B')) form a self-adjoint set, since ฯ and the isotony embedding preserve
the adjoint, and the bicommutant of a self-adjoint set is a von Neumann algebra
(Physicslib4.GNS.vonNeumannOfSelfAdjoint). This is that algebra, an element of Mathlib's
VonNeumannAlgebra; its underlying set is localVonNeumann (coe_localVonNeumannAlgebra).
Microcausality and isotony are stated for it with the order โค and VonNeumannAlgebra.commutant.
Blueprint: def:local-von-neumann-algebra-in-curved-spacetime
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 net of local von Neumann algebras B' โฆ R(B') inside a basis set B, as a monotone map.
Fix a basis set B and a representation ฯ of ๐(B). The map sends each basis set B' โ B to
R(B') = ฯ(๐(B'))'' and is monotone: Bโ โ Bโ implies R(Bโ) โค R(Bโ) (localVonNeumannAlgebra_mono).
This is the curved counterpart of the Minkowski vonNeumannNet, with the net restricted to the
basis subsets of one containing region because there is no quasilocal algebra.
Monotonicity needs no extra hypothesis. It rests on the embedding of ๐(Bโ) in ๐(B) factoring
through ๐(Bโ), which is the composition law of Axiom 2 (commIsotony_comp) and so holds for every
net.
Blueprint: def:von-neumann-net-in-curved-spacetime
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 R(Bโ)' โฉ R(Bโ) of two basis sets Bโ, Bโ โ B, as a von Neumann algebra.
It consists of the operators of R(Bโ) that commute with all of R(Bโ). For a nested pair
Bโ โ Bโ it is the basic object of the theory of inclusions R(Bโ) โ R(Bโ) of local algebras: the
inclusion is irreducible when it contains only the scalars (IsIrreducibleInclusion), and it
always contains the centre of R(Bโ) (center_le_relativeCommutant). As for the other local von
Neumann algebras, everything is relative to a representation ฯ of a containing algebra ๐(B).
Implementation note: the definition does not require Bโ โ Bโ. Mathlib's VonNeumannAlgebra has
no meet, so the algebra is built by hand as the meet of the *-subalgebras R(Bโ)' and R(Bโ); it is
closed under taking the bicommutant because it is the commutant of R(Bโ) โช R(Bโ)'. Its underlying
set is R(Bโ)' โฉ R(Bโ) (coe_relativeCommutant).
Blueprint: def:relative-commutant-in-curved-spacetime
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โ) is irreducible: its relative commutant R(Bโ)' โฉ R(Bโ) is โยท1.
This is the notion of an irreducible inclusion from subfactor theory: no operator of R(Bโ) other
than a scalar commutes with all of R(Bโ). For nested basis sets Bโ โ Bโ โ B it forces R(Bโ) to be a
factor (isFactor_of_isIrreducibleInclusion), and the inclusion of R(Bโ) in itself is irreducible
exactly when R(Bโ) is a factor (isIrreducibleInclusion_self_iff_isFactor).
Implementation note: โยท1 is scalarOperators H, and the definition does not require Bโ โ Bโ.
Blueprint: def:irreducible-inclusion-in-curved-spacetime
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').