Stabilizer action on a curved local algebra and its GNS unitary #
In curved spacetime there is no quasilocal algebra, so the covariance
equivalences covEquiv φ B : 𝔘(B) ≃⋆ₐ[ℂ] 𝔘(φ·B) map between different local
algebras and do not assemble into a single unitary representation of the full
isometry group. They do restrict to a genuine action by automorphisms of a
single local algebra 𝔘(B) on the stabilizer subgroup
Stab(B) = {φ : φ·B = B} of the region B: for such φ, φ·B = B, so
covEquiv φ B : 𝔘(B) ≃⋆ₐ[ℂ] 𝔘(φ·B) = 𝔘(B) is an automorphism of 𝔘(B).
This file builds that automorphism stabAut, proves it is a monoid action
(stabAut_one, stabAut_mul) using the curved covariance coherence
(covEquiv_one, covEquiv_mul), and instantiates the algebra-agnostic GNS
unitary GNS.exists_gns_unitary_of_invariant to produce a unitary
representation of Stab(B) on the GNS space of a Stab(B)-invariant state on
𝔘(B).
Main definitions / results #
HaagKastlerNet.stabAut: forφwithφ·B = B, the covariance automorphism of𝔘(B).HaagKastlerNet.stabAut_one,HaagKastlerNet.stabAut_mul: it is a monoid action ofStab(B).HaagKastlerNet.exists_gns_unitary_stabilizer: the GNS unitary representation ofStab(B)for aStab(B)-invariant state on𝔘(B).
Physical interpretation #
Stab(B) is the curved-spacetime stand-in for the global symmetry group: it is
the subgroup acting on the single algebra one actually has. Concretely it is
typically a Killing flow (e.g. the stationary ∂_t flow of a Schwarzschild
exterior, giving a KMS/Hartle-Hawking state, or the de Sitter static-patch boost
giving the Gibbons-Hawking temperature) or a spatial-symmetry subgroup (e.g. the
rotation subgroup fixing a comoving ball in an FLRW cosmology).
Transport a local algebra along an equality of regions.
Instances For
Stabilizer automorphism. For an isometry φ fixing the region B
(φ·B = B), the covariance equivalence covEquiv φ B lands back in 𝔘(B) and
is therefore an automorphism of the single algebra 𝔘(B).
Instances For
Naturality of covEquiv under an equality of regions.
The stabilizer action is trivial at the identity.
The stabilizer action is multiplicative.
The stabilizer automorphism as a function on the stabilizer subgroup
Stab(B) = {φ : φ·B = B}, packaged so the monoid-action laws are syntactic.
Equations
- N.stabAutHom B φ = N.stabAut ↑φ ⋯
Instances For
The stabilizer action packaged as a group homomorphism from the stabilizer
subgroup Stab(B) to the *-automorphism group of the local algebra 𝔘(B),
g ↦ α̂_g. This bundles stabAutHom_one and stabAutHom_mul; the target's group
law is composition (f * g = g.trans f, StarAlgEquiv.aut). It exhibits the
stabilizer action as a unitary-free representation of Stab(B) by *-automorphisms
of 𝔘(B) — the curved counterpart of the Minkowski actionHom.
Equations
- N.stabAutMonoidHom B = { toFun := N.stabAutHom B, map_one' := ⋯, map_mul' := ⋯ }
Instances For
GNS unitary representation of the stabilizer. For a state ω on the
local algebra 𝔘(B) that is invariant under the stabilizer action of
Stab(B) = {φ : φ·B = B}, the action is implemented on the GNS Hilbert space by
a unitary representation U of Stab(B): there is a GNS triple (H, π, Ω) and
unitaries U g with U g (π a Ω) = π (g · a) Ω, U g Ω = Ω, the group laws,
and U 1 = id.
This is the curved-spacetime instantiation of
GNS.exists_gns_unitary_of_invariant, with the single algebra A = 𝔘(B) and
the stabilizer action γ = stabAutHom.
Strongly continuous GNS unitary representation of the stabilizer.
Strengthening of exists_gns_unitary_stabilizer: if the isometry group M.Isom
carries a topology (passed as an instance argument, since the abstract
LorentzianSpacetime interface provides none) and the matrix coefficients
g ↦ ω(a⋆ · g·b) are continuous on Stab(B), then the unitary representation
U of Stab(B) is strongly continuous: g ↦ U g ψ is continuous for every
GNS vector ψ.
The stabilizer subgroup ↥(MulAction.stabilizer M.Isom B) inherits its topology
as a subspace of M.Isom. This is the curved-spacetime specialization of
GNS.exists_gns_unitary_of_invariant_strongContinuous.
Bundled GNS unitary representation of the stabilizer. The bundled form of
exists_gns_unitary_stabilizer: the implementing unitaries are returned as a
genuine unitary representation U : ↥Stab(B) →* (H ≃ₗᵢ[ℂ] H), feeding the
stabilizer group homomorphism stabAutMonoidHom into the bundled analytic core
GNS.exists_gns_unitaryRep_of_invariant.
Bundled strongly continuous GNS unitary representation of the stabilizer.
The bundled form of exists_gns_unitary_stabilizer_strongContinuous: the strongly
continuous implementing unitaries are returned as a bundled group homomorphism
U : ↥Stab(B) →* (H ≃ₗᵢ[ℂ] H).
Irreducible covariant representation of a pure invariant state (curved
spacetime). A state ω on a local algebra 𝔘(B) that is invariant under the
stabilizer action and pure yields a GNS representation that is simultaneously
covariant - implemented by a unitary representation U of the stabilizer
Stab(B) fixing the cyclic vector Ω, with the operator covariance
U(g) π(a) U(g)⁻¹ = π(g · a) - and irreducible. It is the curved, per-region
analogue (there is no quasilocal algebra), combining exists_gns_unitary_stabilizer
with purity ⟹ irreducibility (isPure_iff_isIrreducible).
As in the Minkowski case this is a precursor to, not, a vacuum: curved spacetime has no global vacuum, and the analogue of the spectrum condition (the Hadamard / microlocal spectrum condition) is a separate requirement not imposed here.
Purity is invariant under the stabilizer action (curved spacetime). A state
ω on a local algebra 𝔘(B) is pure if and only if its pullback ω ∘ \hatα_g
along the stabilizer automorphism is pure, for any g ∈ Stab(B). Specialization of
isPure_precomp_iff.