GNS unitary representation of an invariant automorphism action #
This file isolates the analytic core behind the GNS implementation of a
covariance action as a standalone, algebra-agnostic result: given any unital
C*-algebra A, a state ω on A, and a family of *-automorphisms
γ : G → (A ≃⋆ₐ[ℂ] A) (indexed by a monoid G) that leaves ω invariant,
the action is implemented on the GNS Hilbert space of ω by a unitary
representation U : G → (H ≃ₗᵢ[ℂ] H).
Main result #
Physicslib4.GNS.exists_gns_unitary_of_invariant: existence of the GNS triple(H, π, Ω)and the unitary representationUwithU g (π a Ω) = π (γ g a) Ω,U g Ω = Ω,U (g' * g) = U g' ∘ U g, andU 1 = id.
Design notes #
This is the local-state analogue of the Minkowski quasilocal GNS unitary
(IsInvariantState.exists_gns_unitary): it depends only on a single C*-algebra
with an invariant automorphism family, not on a global quasilocal algebra. In
particular it applies directly to a local algebra 𝔘(B) of a Haag-Kastler
net (in flat or curved spacetime) whenever the symmetry group acts on 𝔘(B)
by automorphisms (e.g. the stabilizer subgroup of the region B), and the
Minkowski quasilocal version is recovered as the special case A = 𝔘 with
γ = β the quasilocal covariance action.
The construction is the dense extension of the isometry π a Ω ↦ π (γ g a) Ω
(isometric because ω (γ g a)⋆ (γ g b) = ω a⋆ b, a consequence of invariance)
via LinearEquiv.extendOfIsometry. The representation laws follow from the
multiplicativity of γ by dense agreement on the cyclic vectors.
Operator covariance of a GNS implementation. If a family of unitaries
U g implements the action γ on the cyclic vector (U g (π a Ω) = π (γ g a) Ω)
and the vectors π a Ω are dense, then the implementation holds at the operator
level: U g · π(a) · U(g)⁻¹ = π(γ g a) on all of H. (No group structure on the
index G is needed; the inverse is the inverse of the unitary U g.)
A symmetry that leaves a state invariant is implemented by unitaries on its GNS space.
Let γ_g, g ∈ G, be *-automorphisms of A with γ_(g'g) = γ_(g') ∘ γ_g and γ_1 = id, and let ω be an invariant state, ω(γ_g(a)) = ω(a). Then a GNS triple (H, π, Ω) of ω carries unitaries U(g) such that
U(g) π(a)Ω = π(γ_g(a)) Ω, U(g) Ω = Ω, U(g'g) = U(g') U(g), U(1) = 1,
and U(g) π(a) U(g)⁻¹ = π(γ_g(a)) on all of H. This is Wigner's unitary implementation of a symmetry, obtained from the algebra and the state: the invariant state, such as the vacuum, becomes an invariant vector. U(g) is the extension of π(a)Ω ↦ π(γ_g(a))Ω, which preserves inner products because ω is invariant. The result is algebra-agnostic: for a Haag–Kastler net it applies to the quasilocal algebra with the Poincaré action β_L, and to a local algebra with the stabiliser of its region.
Implementation note: G is a monoid, and U g is a linear isometric equivalence of H. Composition
of unitaries is written (U g).trans (U g') for U(g') U(g). The bundled form with group
homomorphisms is exists_gns_unitaryRep_of_invariant.
Blueprint: the general form of thrm:invariant-state-gns-unitary
The unitary implementation of an invariant symmetry, as a homomorphism into the unitary group.
This is exists_gns_unitary_of_invariant with the action given as a monoid homomorphism
γ : G →* (A ≃⋆ₐ[ℂ] A) and the unitaries returned as a monoid homomorphism
U : G →* (H ≃ₗᵢ[ℂ] H): a unitary representation of G on the GNS space. The laws U(g'g) =
U(g') U(g) and U(1) = 1 are part of U; the statement keeps the reproducing formula, the
implementation U(g)π(a)Ω = π(γ_g(a))Ω, the invariance U(g)Ω = Ω, operator covariance and the
cyclicity of Ω.
Implementation note: both groups multiply by composition, f * g = g.trans f
(StarAlgEquiv.aut, LinearIsometryEquiv.instGroup).
Blueprint: the general form of thrm:invariant-state-gns-unitary
The unitary implementation of an invariant symmetry is strongly continuous if ω is.
With the hypotheses of exists_gns_unitary_of_invariant, let G carry a topology and let the
matrix coefficients g ↦ ω(a* γ_g(b)) be continuous for all a, b ∈ A. Then the unitaries can be
chosen with g ↦ U(g)ψ continuous for every ψ ∈ H. Strong continuity is what Stone's theorem
needs to produce self-adjoint generators, such as the Hamiltonian and momentum for spacetime
translations. The proof notes that ⟨π(a)Ω, U(g)π(b)Ω⟩ = ω(a* γ_g(b)) and applies
strongContinuous_of_weak on the dense set of vectors π(a)Ω.
Blueprint: the general form of thrm:invariant-state-gns-unitary-strongly-continuous
A strongly continuous unitary representation implementing an invariant symmetry.
This is exists_gns_unitary_of_invariant_strongContinuous with the action and the unitaries
bundled as monoid homomorphisms, as in exists_gns_unitaryRep_of_invariant. The statement
keeps the reproducing formula, the implementation, the invariance U(g)Ω = Ω, strong continuity
and operator covariance.
Blueprint: the general form of thrm:invariant-state-gns-unitary-strongly-continuous