Quasilocal Algebra

This file formalises the blueprint declaration def:quasilocal-algebra (section 10.3 of the AQFT-in-Lean blueprint):

Consider the set-theoretic union of all 𝔘(𝐁). As previously proven, this set-theoretic union is a normed -algebra. Also, as previously proven, taking its completion one obtains a C-algebra denoted as 𝔘. This C*-algebra 𝔘 is called the quasilocal algebra.

Main definitions

• Physicslib4.AQFT.HaagKastler.QuasilocalAlgebra: a structure bundling the data of a quasilocal algebra for a given LocalNet: an ambient C*-algebra together with unital *-monomorphisms from each local algebra 𝔘(B) whose images jointly have dense union.

Modelling notes

• Mathlib (as of v4.31.0-rc1) does not yet have a canonical C*-algebraic direct-limit / amalgamated-completion construction for a family of C*-algebras. Consequently we cannot construct the quasilocal algebra of a LocalNet as a definite term; instead we package its characterising data as a structure.

• A QuasilocalAlgebra U consists of:

  • a carrier type carrier,
  • a CStarAlgebra instance on carrier,
  • a family of unital *-homomorphisms ι B : U.algebra B →⋆ₐ[ℂ] carrier, one for each subset B of Minkowski spacetime,
  • injectivity of ι B for every Alexandrov-basis set B (so that each local algebra embeds faithfully), and
  • the density condition that the set-theoretic union of the images ι B '' (U.algebra B), ranging over Alexandrov-basis sets B, is dense in carrier.

• This mirrors exactly the existential content of QuasilocalCompleteness: a LocalNet satisfies that axiom iff it admits some QuasilocalAlgebra. The two are kept separate so the axiom can be stated as a Prop and the underlying datum can be passed around as a structure.

• The CStarAlgebra instance is attribute [instance]-marked so that downstream code finds the C*-structure on Q.carrier automatically (mirroring the pattern in LocalAlgebras.lean).

structure Physicslib4.AQFT.HaagKastler.QuasilocalAlgebra (U : LocalNet) : Type (max 1 u_1)

Quasilocal Algebra (data). For a local net U, a QuasilocalAlgebra U is the data of an ambient unital C*-algebra carrier — the quasilocal algebra 𝔘 — together with a family of unital *-monomorphisms ι B : U.algebra B →⋆ₐ[ℂ] carrier, one for every subset B of Minkowski spacetime, such that

• each ι B is injective when B is an Alexandrov-basis set (so the local algebras embed faithfully), and
• the union of the images Set.range (ι B) over all Alexandrov-basis sets B is dense in carrier.

The density condition encodes the blueprint's "taking the completion of the set-theoretic union of all 𝔘(B) one obtains the C*-algebra 𝔘": every element of carrier is the norm-limit of a sequence of elements coming from the local algebras.

Blueprint reference: def:quasilocal-algebra.

• carrier : Type

  The underlying type of the quasilocal algebra 𝔘.

• instCStarAlgebra : CStarAlgebra self.carrier

  The CStarAlgebra instance on carrier.

• ι (B : Set StandardMinkowskiSpacetime.Carrier) : U.algebra B →⋆ₐ[ℂ] self.carrier

  The family of unital *-homomorphisms ι B : 𝔘(B) →⋆ₐ[ℂ] 𝔘 embedding each local algebra into the quasilocal algebra.

• ι_injective ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ : IsAlexandrovBasisSet B → Function.Injective ⇑(self.ι B)

  Each embedding ι B is injective on Alexandrov-basis sets, i.e. every local algebra 𝔘(B) embeds faithfully into 𝔘.

• dense_range : Dense (⋃ (B : Set StandardMinkowskiSpacetime.Carrier), ⋃ (_ : IsAlexandrovBasisSet B), Set.range ⇑(self.ι B))

  The union of the images of all local algebras, ranging over Alexandrov-basis sets, is dense in the quasilocal algebra. This is the blueprint's "completion of the set-theoretic union".

• inclusion ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ : IsAlexandrovBasisSet B₁ → IsAlexandrovBasisSet B₂ → B₁ ⊆ B₂ → U.algebra B₁ →⋆ₐ[ℂ] U.algebra B₂

  A chosen family of isotony *-monomorphisms inclusion : 𝔘(B₁) →⋆ₐ[ℂ] 𝔘(B₂) for inclusions B₁ ⊆ B₂ of Alexandrov-basis sets.

• ι_inclusion ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂) (a : U.algebra B₁) : (self.ι B₂) ((self.inclusion hB₁ hB₂ h) a) = (self.ι B₁) a

  Isotony coherence: the embeddings respect the chosen isotony arrows, ι B₂ ∘ inclusion = ι B₁. An element of 𝔘(B₁) thus embeds into the quasilocal algebra 𝔘 independently of the basis set used to view it.

theorem Physicslib4.AQFT.HaagKastler.QuasilocalAlgebra.norm_ι {U : LocalNet} (Q : QuasilocalAlgebra U) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) (a : U.algebra B) : ‖(Q.ι B) a‖ = ‖a‖

Each local embedding Q.ι B is norm-preserving on Alexandrov-basis sets: an injective *-homomorphism of complex C*-algebras is isometric, so the local algebra 𝔘(B) sits inside the quasilocal algebra 𝔘 with its norm intact.

theorem Physicslib4.AQFT.HaagKastler.QuasilocalAlgebra.isometry_ι {U : LocalNet} (Q : QuasilocalAlgebra U) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) : Isometry ⇑(Q.ι B)

Each local embedding Q.ι B is an isometry on Alexandrov-basis sets. This is the metric form of QuasilocalAlgebra.norm_ι.