Towards the intertwiner on the generated subalgebra #
This file begins assembling the densely-defined intertwiner used to lift the
fiberwise covariance action to the quasilocal algebra (QuasilocalLift). Two
ingredients are established here:
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 remaining step - defining the intertwiner ι_B a ↦ ι_{L·B}(α_L a) on this
generated subalgebra and checking it is a well-defined *-homomorphism - will
use StarAlgebra.adjoin_induction together with the isotony-coherence field
QuasilocalAlgebra.ι_inclusion and basis directedness.
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), ⋃ (_ : Physicslib4.AQFT.HaagKastler.IsAlexandrovBasisSet B), Set.range ⇑(Q.ι B)
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
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 hcompat 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_ι, valid once Q is covariance-compatible.
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.
A quasilocal algebra is covariant if its embeddings are covariance-
compatible for every Lorentz transformation (so the lift exists for all
L).
Equations
Instances For
The chosen extended intertwiner Φ_L : 𝔘 →⋆ₐ[ℂ] 𝔘 for a covariant
quasilocal algebra.
Equations
Instances For
Φ_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 a covariance-compatible quasilocal
algebra, 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 trivial quasilocal algebra is covariance-compatible. Every local
algebra is ℂ, every ℂ-algebra *-automorphism of ℂ is the identity, and
the embeddings/inclusions are the identity, so the compatibility holds.
The quasilocal lift exists unconditionally for the trivial net.
Equations
Instances For
A covariant quasilocal algebra: a Haag-Kastler net together with a
quasilocal algebra whose embeddings are covariance-compatible for every Lorentz
transformation. On such data the Lorentz action lifts to a *-automorphism of
the quasilocal algebra for every L.
- net : HaagKastlerNet
The underlying Haag-Kastler net.
- quasilocal : QuasilocalAlgebra self.net.U
A quasilocal algebra of the net.
- covariant : IsCovariant self.net self.quasilocal
Covariance-compatibility of the embeddings, for every Lorentz transformation.
Instances For
The lift of the Lorentz action of L to a *-automorphism of the
quasilocal algebra, packaged as a QuasilocalLift.
Equations
Instances For
The covariance *-automorphism β_L of the 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 it is a
fixed point of the dual covariance action: ω(β_L a) = ω(a) for every Lorentz
transformation L and every observable a. This is the invariance part of the
vacuum conditions; the spectrum condition is imposed separately.
Equations
- C.IsInvariantState ω = ∀ (L : Physicslib4.AQFT.HaagKastler.InhomogeneousLorentzGroup) (a : C.quasilocal.carrier), ω ((C.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 C.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).
This is a necessary precursor to, but not yet, a vacuum representation: a genuine vacuum would additionally require the spectrum condition (positivity of the energy- momentum spectrum), which is not available here.
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 = C.action L.
Specialization of isPure_precomp_iff.
The trivial net with its trivial quasilocal algebra is a covariant quasilocal algebra, so the structure is inhabited.
Equations
- One or more equations did not get rendered due to their size.