The quasilocal lift of the covariance action #
This file defines the densely-defined intertwiner ι_B a ↦ ι_{L·B}(α_L a) on the
dense local *-subalgebra, extends it to the quasilocal algebra (quasilocalLift,
HaagKastlerNet.action), and studies invariant states and their covariant GNS
representations. Along the way:
IsAlexandrovBasisSet.directed: the Haag-Kastler-level restatement ofSpacetime.alexandrovBasis_directed(any two basis sets lie in a common basis set).dense_adjoin_iUnion_range_ι: the*-subalgebra of𝔘generated by the union of the local imagesι_B(𝔘(B))is dense - so it is a valid domain for the dense-extension lemmaexists_starAlgHom_extend_of_dense.- The intertwiner on this generated subalgebra, defined using
StarAlgebra.adjoin_inductiontogether with the isotony-coherence fieldQuasilocalAlgebra.ι_inclusionand basis directedness, extends to the whole quasilocal algebra by density.
Haag-Kastler directedness of the Alexandrov basis. Any two Alexandrov-basis sets are contained in a common Alexandrov-basis set.
The *-subalgebra of the quasilocal algebra generated by the union of all
local images is dense: it contains the (already dense) union of the images
ι_B(𝔘(B)).
The union of all local images ι_B(𝔘(B)) over Alexandrov-basis sets B.
Equations
- Q.localImages = ⋃ (B : Set Physicslib4.StandardMinkowskiSpacetime.Carrier), ⋃ (hB : Physicslib4.AQFT.HaagKastler.IsAlexandrovBasisSet B), Set.range ⇑(Q.ι hB)
Instances For
Directedness of the local images. Any two elements of the union of
local images are images, from a common basis set C, of elements of
𝔘(C) - using basis directedness and the isotony-coherence ι_inclusion.
The union of local images is a *-subalgebra of the quasilocal algebra.
Closure under multiplication and addition uses directedness (exists_common_image)
to route both arguments through a single embedding ι_C; closure under star,
1, 0, and scalars is pointwise.
Equations
- Q.localStarSubalgebra = { carrier := Q.localImages, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯, star_mem' := ⋯ }
Instances For
The local *-subalgebra is dense in the quasilocal algebra.
Naturality of the embeddings under set equality. If B₁ = B₂ then the
embedding of a and of its transport agree in 𝔘. Used to reconcile the
cross-fiber casts coming from covEquiv_one / covEquiv_mul.
Covariance-compatible embeddings. A quasilocal algebra Q of the net
N is covariant-compatible for a Lorentz transformation L if its local
embeddings intertwine the covariance action with the chosen isotony inclusions:
ι_{L·B}(α_L a) = ι_{L·C}(α_L (incl_{B,C} a)) for B ⊆ C. This is the
honest content carried by the embeddings of a genuinely covariant 𝔘.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every quasilocal algebra is covariance-compatible. Axiom 5 (3) is stated
for the Axiom 2 isotony family, so α_L intertwines the isotony embeddings, and
the cocone condition ι_inclusion then gives IsCovariantQuasilocal for every
quasilocal algebra and every Lorentz transformation.
Well-definedness of the intertwiner. If two local elements ι_B a and
ι_{B'} a' agree in 𝔘, then their intended images
ι_{L·B}(α_L a) and ι_{L·B'}(α_L a') agree. The proof routes both through a
common basis set C (directedness), uses ι_inclusion + injectivity to
identify the inclusions, and isCovariantQuasilocal to push through the action.
The intertwiner on the quasilocal algebra: on a local element ι_B a
it returns ι_{L·B}(α_L a) (and 0 off the local images). Its characterising
equation is intertwiner_ι.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Defining equation of the intertwiner. On ι_B a it returns
ι_{L·B}(α_L a), well-definedly.
Additivity of the intertwiner. On the local images it preserves
addition - both arguments are routed through a common basis algebra ι_C.
Multiplicativity of the intertwiner. On the local images it preserves multiplication - both arguments are routed through a common basis algebra.
The intertwiner preserves 0.
The intertwiner preserves 1.
The intertwiner preserves star on the local images.
The intertwiner is ℂ-linear on the local images.
The intertwiner as a *-homomorphism on the local subalgebra. Bundles
the homomorphism laws of intertwiner into a StarAlgHom from the dense local
*-subalgebra of 𝔘 into 𝔘.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The intertwiner is norm-preserving on the local images. It maps
ι_B a ↦ ι_{L·B}(α_L a); both embeddings are isometric (norm_ι, using that
L·B is again a basis set) and α_L is isometric (norm_covEquiv).
The bundled intertwiner is an isometry on the local *-subalgebra.
Existence of the extended intertwiner. The norm-preserving (hence
uniformly continuous) *-homomorphism on the dense local *-subalgebra extends
to a *-homomorphism F : 𝔘 →⋆ₐ[ℂ] 𝔘 agreeing with the intertwiner on the
local images.
The chosen extended intertwiner Φ_L : 𝔘 →⋆ₐ[ℂ] 𝔘 of a quasilocal
algebra.
Equations
Instances For
The extended intertwiner Φ_L is continuous.
Φ_L implements the fiberwise action on the generators:
Φ_L (ι_B a) = ι_{L·B}(α_L a).
Two *-homomorphisms of 𝔘 that are continuous and agree on the local
images are equal (the images are dense).
Φ is multiplicative in the group element: Φ_{L'·L} = Φ_{L'} ∘ Φ_L.
Φ_1 = id.
Existence of the quasilocal lift. For every quasilocal algebra (all are
covariance-compatible, isCovariantQuasilocal), the fiberwise Lorentz action
lifts to a *-automorphism of 𝔘, inhabiting QuasilocalLift.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The quasilocal lift exists for every Lorentz transformation.
The quasilocal lift exists unconditionally for the trivial net.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The quasilocal lift exists unconditionally for the trivial net.
The lift of the Lorentz action of L to a *-automorphism of the
quasilocal algebra, packaged as a QuasilocalLift.
Equations
Instances For
The automorphism β_L of the quasilocal algebra 𝔘 by which a Poincaré transformation L acts.
Axiom 5 gives *-isomorphisms α_L : 𝔘(B) → 𝔘(LB) between local algebras. They fit together into a
single *-automorphism β_L of 𝔘 with β_L(ι_B a) = ι_(LB)(α_L a) (action_ι): β_L is defined by
this formula on the union of the local images, which is a dense *-subalgebra since the diamonds
are directed, and extended by continuity. It is unique
(QuasilocalLift.unique), and L ↦ β_L is a group homomorphism (action_one, action_mul,
actionHom).
Blueprint: def:covariant-quasilocal-algebra
Instances For
The action implements the fiberwise covariance on the local images:
β_L (ι_B a) = ι_{L·B}(α_L a).
The action agrees with the underlying extended *-homomorphism.
The action is trivial at the identity: β_1 = id.
The action is multiplicative in the group element:
β_{L'·L} = β_{L'} ∘ β_L.
The covariance action sends the identity to the identity automorphism.
The covariance action is multiplicative: β_{L'·L} = β_L followed by
β_{L'}.
The covariance action packaged as a group homomorphism from the
inhomogeneous Lorentz group to the *-automorphism group of the quasilocal
algebra, L ↦ β_L. This bundles action_one and action_mul; the target's group
law is composition (f * g = g.trans f, StarAlgEquiv.aut), which is exactly the
form of action_mul. It exhibits the covariance action as a genuine unitary-free
representation of the Poincaré group by *-automorphisms of 𝔘.
Instances For
A state ω on the quasilocal algebra is Poincaré invariant if ω(β_L a) = ω(a) for all L and a.
Here β_L is the automorphism HaagKastlerNet.action by which L acts on 𝔘. Invariance is the first
of the two conditions on a vacuum state (HaagKastlerNet.IsVacuumState); the second is the
spectrum condition. In the GNS representation of an invariant state the action is implemented by
unitaries U(L) that fix the cyclic vector (IsInvariantState.exists_gns_unitary).
Blueprint: def:invariant-state
Equations
- N.IsInvariantState ω = ∀ (L : Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup) (a : N.quasilocal.carrier), ω ((N.action L) a) = ω a
Instances For
Invariance of the GNS inner product. For an invariant state, the
sesquilinear form (a, b) ↦ ω(a^* b) - which is the GNS inner product of the
cyclic vectors π(a)Ω, π(b)Ω - is preserved by the action. This is the
algebraic input that makes the implementing operator on the GNS space an
isometry, hence (Step 2) a unitary.
Step 2: GNS unitary implementation of an invariant state. For an
invariant state ω, the fiberwise covariance action is implemented on the GNS
Hilbert space by a family of unitaries U L with U L (π a Ω) = π (β_L a) Ω and
U L Ω = Ω. The unitaries are the dense-extension of the isometry
π a Ω ↦ π (β_L a) Ω (isometric by inner_invariant), via
LinearEquiv.extendOfIsometry.
Strongly continuous GNS unitary representation of an invariant state.
Strengthening of IsInvariantState.exists_gns_unitary: if the quasilocal matrix
coefficients L ↦ ω(a⋆ · β_L b) are continuous in the Lorentz transformation
L (with respect to the topology on InhomogeneousLorentzGroup), then the
implementing unitary representation U is strongly continuous - L ↦ U L ψ is
continuous for every GNS vector ψ.
This is the quasilocal-state form of the weak-continuity hypothesis; it is the
direct specialization of the algebra-agnostic
GNS.exists_gns_unitary_of_invariant_strongContinuous.
Bundled GNS unitary representation of an invariant state. The bundled form
of IsInvariantState.exists_gns_unitary: the implementing unitaries are returned
as a genuine unitary representation U : InhomogeneousLorentzGroup →* (H ≃ₗᵢ[ℂ] H)
(a bundled group homomorphism), rather than a bare family with separate group-law
clauses. It feeds the covariance group homomorphism N.actionHom into the bundled
analytic core GNS.exists_gns_unitaryRep_of_invariant.
Bundled strongly continuous GNS unitary representation of an invariant state.
The bundled form of IsInvariantState.exists_gns_unitary_strongContinuous: the
strongly continuous implementing unitaries are returned as a bundled group
homomorphism U : InhomogeneousLorentzGroup →* (H ≃ₗᵢ[ℂ] H).
Irreducible covariant representation of a pure invariant state (Minkowski).
A state ω on the quasilocal algebra that is both invariant under the covariance
action and pure yields a GNS representation that is simultaneously covariant -
implemented by a unitary representation U of the inhomogeneous Lorentz group
fixing the cyclic vector Ω, with the operator covariance
U(L) π(a) U(L)⁻¹ = π(β_L a) - and irreducible. It combines
IsInvariantState.exists_gns_unitary (a covariant GNS triple with invariant cyclic
Ω) with purity ⟹ irreducibility (isPure_iff_isIrreducible).
A vacuum representation additionally requires the spectrum condition
(positivity of the energy-momentum spectrum); see HaagKastlerNet.IsVacuumState.
Purity is covariance-invariant (Minkowski). A state ω on the quasilocal
algebra is pure if and only if its pullback ω ∘ β_L along the covariance
automorphism is pure: purity is preserved by the *-automorphism β_L = N.action L.
Specialization of isPure_precomp_iff.
GNS covariance along the quasilocal action #
GNS covariance along the quasilocal action. The lifted covariance automorphism
β_L = N.action L is a *-automorphism of the quasilocal algebra 𝔘, so a cyclic
representation of 𝔘 reproducing the pullback state ω ∘ β_L is unitarily equivalent
to π_ω ∘ β_L.
Irreducibility is Lorentz invariant on the quasilocal algebra. With the GNS data
above, π₁ is irreducible exactly when π₂ is.
Factoriality is Lorentz invariant on the quasilocal algebra. With the GNS data
above, π₁(𝔘)'' is a factor exactly when π₂(𝔘)'' is. So the superselection type of a
global state is a Lorentz invariant.