Geometric covariance of the local von Neumann net (curved spacetime) #
This is the curved-spacetime, stabilizer-subgroup analogue of the Minkowski
geometric covariance result. There is no quasilocal algebra in curved spacetime,
so the representation π is of a containing basis algebra 𝔘(B), and the only
genuine symmetries acting on 𝔘(B) are the elements of the stabilizer
Stab(B) = {g : g · B = B} (via stabAut). For g ∈ Stab(B), the implementing
unitary U(g) of the stabilizer GNS representation conjugates the local von
Neumann algebra of a subregion B₁ ⊆ B onto that of g · B₁:
U(g) · R(B₁) · U(g)⁻¹ = R(g · B₁).
Compared with Minkowski, the abstract LorentzianSpacetime interface provides
neither basis-set preservation (M.IsBasisSet (g · B₁)) nor the
covariance-versus-isotony coherence relating the stabilizer action stabAut g to
the chosen isotony embeddings commIsotony. Both therefore enter as explicit
hypotheses (hgB₁, h₁', hcompat), exactly as elsewhere in the curved
development (e.g. localVonNeumann_mono). For a net arising from a concrete
geometric spacetime they are discharged by isBasisSet_smul and the genuine
covariance of the action.
The reusable conjugation machinery (lieConj, MulEquiv.image_centralizer) is
shared with the Minkowski development.
Conjugation carries the local operators of B₁ onto those of g · B₁.
Given operator covariance U π(a) U⁻¹ = π(stabAut g · a) for g ∈ Stab(B) and the
covariance-isotony coherence hcompat, conjugation lieConj U maps the local
observable operators of a subregion B₁ ⊆ B onto those of g · B₁.
Geometric covariance of the local von Neumann net (curved spacetime). For
g ∈ Stab(B), conjugation by the implementing unitary U(g) of the stabilizer
GNS representation carries the local von Neumann algebra of a subregion B₁ ⊆ B
onto that of g · B₁:
U(g) · R(B₁) · U(g)⁻¹ = R(g · B₁).
The operator-covariance hypothesis hcov is the last clause supplied by
exists_gns_unitary_stabilizer; the coherence hcompat and the geometric data
hgB₁, h₁' are the curved-spacetime side conditions discussed in the module
docstring. In particular R(B₁) and R(g · B₁) are unitarily equivalent.
Geometric covariance, bundled (curved spacetime). The set image of the
bundled local VonNeumannAlgebra R(B₁) under conjugation by U(g) is the
bundled R(g · B₁).
Orbit-invariance of factoriality (curved spacetime). If the local von
Neumann algebra R(B₁) of a subregion is a factor, then so is R(g · B₁) for
g ∈ Stab(B). Geometric covariance exhibits R(g · B₁) as the unitary conjugate
U(g) R(B₁) U(g)⁻¹, and conjugation preserves the factor property; so being a
factor is constant along the stabilizer orbit of a subregion.
Geometric covariance as a von Neumann algebra isomorphism (curved spacetime).
For g ∈ Stab(B), conjugation by the implementing unitary U(g) is the
*-isomorphism R(B₁) ≃ R(g · B₁) of local von Neumann algebras: it restricts the
conjugation *-automorphism T ↦ U(g) T U(g)⁻¹ of B(H), whose image of R(B₁)
is exactly R(g · B₁) by geometric covariance.
Equations
- N.localVonNeumannEquiv hB π Uop g hB₁ h₁ hgB₁ h₁' hcov hcompat = Physicslib4.restrictStarAlgEquiv Uop.conjStarAlgEquiv ⋯ ⋯