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. The motivating
examples are Killing flows (the stationary β_t flow of a Schwarzschild
exterior, with the Hartle-Hawking state, or the de Sitter static-patch boost,
with the Gibbons-Hawking temperature). Those regions are not diamonds (basis
sets), and no such flow fixes a nonempty diamond, so the axioms as stated place
no constraint on their algebras: the examples motivate the definitions but are
not instances of them. A spatial-symmetry subgroup (e.g. the rotation subgroup
fixing a comoving ball in an FLRW cosmology) is also a stabilizer.
Transport a local algebra along an equality of regions.
Instances For
The stabilizer automorphism Ξ±Μ_Ο of π(B), for an isometry Ο that fixes the region B.
The covariance isomorphisms Ξ±_Ο : π(B) β π(Ο(B)) of Axiom 5 map between different local algebras,
and curved spacetime has no quasilocal algebra on which they could act together. When Ο(B) = B,
however, Ξ±_Ο maps π(B) back to itself, and so is a *-automorphism Ξ±Μ_Ο of the single algebra π(B).
The isometries fixing B form its stabilizer subgroup Stab(B), on which these automorphisms form a
group action (stabAut_one, stabAut_mul). Physically Stab(B) stands in for the global symmetry
group. The motivating examples are Killing flows, such as the stationary flow of a black-hole
exterior or the boost of a de Sitter static patch. Those regions are not diamonds (basis sets), and
no such flow fixes a nonempty diamond, so the axioms as stated place no constraint on their
algebras: the examples motivate the definition but are not instances of it.
Implementation note: Ξ±Μ_Ο is covEquiv Ο B followed by the identification π(Ο β’ B) = π(B) along
the hypothesis h : Ο β’ B = B (algCongr). stabAutHom is the same map indexed by elements of
MulAction.stabilizer M.Isom B.
Blueprint: def:stabilizer-action-in-curved-spacetime
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 g β¦ Ξ±Μ_g, as a function on the stabilizer subgroup Stab(B).
Stab(B) = {Ο : Ο(B) = B} is Mathlib's MulAction.stabilizer M.Isom B, and Ξ±Μ_g is stabAut at the
underlying isometry of g. Indexing by subgroup elements makes the action laws Ξ±Μ_1 = id and
Ξ±Μ_(g'g) = Ξ±Μ_g' β Ξ±Μ_g (stabAutHom_one, stabAutHom_mul) statements without side hypotheses.
The GNS and KMS results use this form.
Blueprint: the action of def:stabilizer-action-in-curved-spacetime, indexed by Stab(B)
Equations
- N.stabAutHom B Ο = N.stabAut βΟ β―
Instances For
The stabilizer action g β¦ Ξ±Μ_g as a group homomorphism from Stab(B) to the group of *-automorphisms of π(B).
This bundles the action laws stabAutHom_one and stabAutHom_mul: Stab(B) acts on the single
algebra π(B) by *-automorphisms. It is the curved counterpart of the Minkowski actionHom,
which acts on the quasilocal algebra; here the action is on one region's algebra only.
Implementation note: the group law of the automorphisms is composition, f * g = g.trans f
(StarAlgEquiv.aut). The structure is a MonoidHom, which for groups is a group homomorphism.
Blueprint: the group action of lmm:stabilizer-action-laws-in-curved-spacetime
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.
GNS covariance along the stabilizer action #
GNS covariance along the stabilizer action (curved spacetime). The stabilizer
automorphism \hatΞ±_g = N.stabAutHom B g is a *-automorphism of the local algebra
π(B), so a cyclic representation of π(B) reproducing the pullback state Ο β \hatΞ±_g
is unitarily equivalent to Ο_Ο β \hatΞ±_g.
Irreducibility is stabilizer invariant (curved spacetime). With the GNS data
above, Οβ is irreducible exactly when Οβ is.
Factoriality is stabilizer invariant (curved spacetime). With the GNS data above,
Οβ(π(B))'' is a factor exactly when Οβ(π(B))'' is. So the superselection type of a
local state is invariant under the stabilizer symmetry of the region β the curved
counterpart of Lorentz invariance of the sector.