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.)
GNS unitary representation of an invariant automorphism action.
For a unital C*-algebra A, a state ω, and a monoid-indexed family of
*-automorphisms γ g : A ≃⋆ₐ[ℂ] A leaving ω invariant (ω (γ g a) = ω a),
the action is implemented on the GNS space of ω by a unitary representation:
there is a GNS triple (H, π, Ω) and unitaries U g with
U g (π a Ω) = π (γ g a) Ω, U g Ω = Ω, U (g' * g) = U g' ∘ U g, and
U 1 = id.
Bundled GNS unitary representation of an invariant action. The bundled form
of exists_gns_unitary_of_invariant: the action enters as a group homomorphism
γ : G →* (A ≃⋆ₐ[ℂ] A), and the implementing unitaries are returned as a bundled
group homomorphism U : G →* (H ≃ₗᵢ[ℂ] H) — a genuine unitary representation.
The group laws U (g' * g) = U g' * U g and U 1 = 1 are now carried by U
itself (map_mul/map_one), so they no longer appear as separate hypotheses on
γ or clauses on U. What remains are the geometric clauses: the reproducing
formula, the implementation U g (π a Ω) = π (γ g a) Ω, vacuum invariance
U g Ω = Ω, operator covariance, and cyclicity. Both group structures use the
composition convention f * g = g.trans f (StarAlgEquiv.aut,
LinearIsometryEquiv.instGroup).
Strongly continuous GNS unitary representation of an invariant action.
Strengthening of exists_gns_unitary_of_invariant: if, in addition, the index
G carries a topology and the matrix coefficients g ↦ ω(a⋆ · γ g b) are
continuous for all a, b : A (the weak-continuity hypothesis), then the
implementing unitary representation U is strongly continuous:
g ↦ U g ψ is continuous for every vector ψ.
The proof feeds the analytic core strongContinuous_of_weak: the cyclic
vectors π a Ω are dense, and the matrix coefficient g ↦ ⟪π a Ω, U g (π b Ω)⟫
equals g ↦ ω(a⋆ · γ g b) (by the implementation property and the reproducing
formula), which is continuous by hypothesis.
Bundled strongly continuous GNS unitary representation. The bundled form of
exists_gns_unitary_of_invariant_strongContinuous: the action enters as a group
homomorphism γ : G →* (A ≃⋆ₐ[ℂ] A) and the strongly continuous implementing
unitaries are returned as a bundled group homomorphism U : G →* (H ≃ₗᵢ[ℂ] H). The
group laws are carried by U; the strong-continuity clause g ↦ U g ψ continuous
and the geometric clauses remain.