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₁).
Basis-set preservation M.IsBasisSet (g · B₁) is supplied by the interface field
M.isBasisSet_smul, as elsewhere in the curved development (e.g.
localVonNeumann_mono). The coherence between the stabilizer action and the
isotony embeddings is not a hypothesis: it is stabAutHom_commIsotony, derived
from Axiom 5 (3), which is stated for the Axiom 2 isotony family.
The reusable conjugation machinery (lieConj, MulEquiv.image_centralizer) is
shared with the Minkowski development.
A stabilizer element of B maps every subregion of B into B:
B₁ ⊆ B and g · B = B give g · B₁ ⊆ B.
The stabilizer action commutes with isotony. For g ∈ Stab(B) and a
subregion B₁ ⊆ B (so g · B₁ ⊆ B, smul_subset_of_mem_stabilizer), the
stabilizer automorphism of 𝔘(B) carries
the image of 𝔘(B₁) onto that of 𝔘(g · B₁), compatibly with the covariance
equivalence. This is Axiom 5 (3) (covEquiv_commIsotony) transported along
g · B = B.
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),
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 geometric datum
(M.isBasisSet_smul _ hB₁) is the curved-spacetime side condition 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.
Conjugation by a unitary implementing a stabilizer element g, as a *-isomorphism R(B₁) ≅ R(g · B₁) of local von Neumann algebras.
Suppose g fixes the basis set B (g ∈ Stab(B), so g · B = B), π is a representation of 𝔘(B), and
U is a unitary on H with U π(a) U⁻¹ = π(α̂_g a) for all a ∈ 𝔘(B), where α̂_g is the stabilizer
automorphism of 𝔘(B); the stabilizer GNS unitaries (exists_gns_unitary_stabilizer) are such
unitaries. For a basis set B₁ ⊆ B, conjugation T ↦ U T U⁻¹ is a *-automorphism of the bounded
operators on H, and by geometric covariance (lieConj_image_localVonNeumann) it maps R(B₁) onto
R(g · B₁). This is its restriction, a *-isomorphism between the two algebras.
Implementation note: the isomorphism is between the underlying *-subalgebras
(VonNeumannAlgebra.toStarSubalgebra).
Blueprint: thrm:von-neumann-covariance-iso-in-curved-spacetime
Equations
- N.localVonNeumannEquiv hB π Uop g hB₁ h₁ hcov = Physicslib4.restrictStarAlgEquiv Uop.conjStarAlgEquiv ⋯ ⋯