Lifting the covariance action to the quasilocal algebra

The Lorentz action on a Haag-Kastler net is given fiberwise by the covariance equivalences α_L : 𝔘(B) ≃⋆ₐ[ℂ] 𝔘(L·B) (HaagKastlerNet.covEquiv). To obtain a single dynamical system one wants to lift this fiberwise action to a *-automorphism β_L of the quasilocal algebra 𝔘 (the ambient C*-algebra of a QuasilocalAlgebra), intertwining the local embeddings: β_L (ι_B a) = ι_{L·B} (α_L a).

This file isolates the specification of such a lift and proves it is unique. The local embeddings ι_B have dense union in 𝔘, and a *-automorphism of a C*-algebra is continuous; hence a lift is determined by its action on the generators, so at most one lift exists for each L.

Main definitions

• Physicslib4.AQFT.HaagKastler.HaagKastlerNet.QuasilocalLift: a *-automorphism of the quasilocal algebra intertwining the fiberwise action of L.

Main results

• QuasilocalLift.unique: any two lifts of the same L have equal underlying automorphism.
• instSubsingletonQuasilocalLift: consequently the type of lifts is a subsingleton.

Notes

This is the uniqueness half of the lifting problem. Existence - actually constructing β_L by extending the densely-defined intertwiner to the completion - is carried out in QuasilocalIntertwiner.lean (nonempty_quasilocalLift): the union of local images forms a *-subalgebra (directedness of the Alexandrov basis plus the isotony coherence), and the densely-defined intertwiner extends by the uniformly-continuous-extension argument exists_starAlgHom_extend_of_dense.

structure Physicslib4.AQFT.HaagKastler.HaagKastlerNet.QuasilocalLift (N : HaagKastlerNet) (Q : QuasilocalAlgebra N.U) (L : InhomogeneousLorentzGroup) : Type

A lift of the fiberwise covariance action of L to a quasilocal algebra Q: a *-automorphism β of the ambient algebra Q.carrier that intertwines the covariance equivalence α_L with the local embeddings, i.e. β (ι_B a) = ι_{L·B} (α_L a) for every Alexandrov-basis set B.

• β : Q.carrier ≃⋆ₐ[ℂ] Q.carrier

  The *-automorphism of the quasilocal algebra implementing L.

• intertwines ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ : IsAlexandrovBasisSet B → ∀ (a : N.algebra B), self.β ((Q.ι B) a) = (Q.ι (L • B)) ((N.covEquiv L B) a)

  β intertwines the fiberwise action α_L with the local embeddings.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.QuasilocalLift.unique {N : HaagKastlerNet} {Q : QuasilocalAlgebra N.U} {L : InhomogeneousLorentzGroup} (l₁ l₂ : N.QuasilocalLift Q L) : l₁.β = l₂.β

Uniqueness of the lift. Two lifts of the same Lorentz transformation have the same underlying automorphism: they agree on the dense union of the local images, and *-automorphisms of a C*-algebra are continuous.

instance Physicslib4.AQFT.HaagKastler.HaagKastlerNet.instSubsingletonQuasilocalLift {N : HaagKastlerNet} {Q : QuasilocalAlgebra N.U} {L : InhomogeneousLorentzGroup} : Subsingleton (N.QuasilocalLift Q L)

The type of lifts of a fixed L is a subsingleton: a lift is determined by its underlying automorphism (QuasilocalLift.unique), and the intertwining field is a proposition.