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) has no canonical C*-algebraic direct-limit / amalgamated-completion construction for a family of C*-algebras: Mathlib.Algebra.Colimit.DirectLimit is purely algebraic (it puts no norm or topology on the colimit) and there is no C*-completion anywhere in Mathlib.Analysis.CStarAlgebra. This structure therefore packages the characterising data of a quasilocal algebra rather than naming a canonical one, which is what lets Axioms 3-5 be stated against it.

  Note this is an interface, not a claim that no such algebra can be built. The blueprint does construct one, from the net alone, by taking the algebraic colimit, equipping it with the norm ‖mk a‖ = ‖a‖ (well defined because the isotony maps are injective and hence isometric), and completing. See the chain from def:completion-standing-hypotheses to lmm:quasilocal-completion-cstar. The route realising the algebra inside an ambient C*-algebra is deliberately not used: it would have to assume such an ambient algebra, and there is no physical justification for one.

• 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.

• Every LocalNet satisfying Axiom 2 admits such a structure: that is exists_quasilocalAlgebra (thrm:quasilocal-algebra-exists), which builds one as the completion of the directed colimit of the local algebras. So this is an interface onto a canonical object, not a hypothesis a net might fail to satisfy.

• 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) (i : Isotony U) : Type (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 u

  The underlying type of the quasilocal algebra 𝔘, in the same universe as the net's local algebras.

  It must not be pinned to Type 0. LocalNet.algebra is universe polymorphic, so a Type 0 carrier would make this structure uninhabitable for a net whose local algebras live in a higher universe: no Type 0 type can hold injective copies of them, and the existence claim would fail on size grounds alone. This is the twin of the over-quantification defect recorded on ι below.

  The carrier is tied to the net's universe rather than given a free one. That costs no generality: dense_range forces 𝔘 to be the closure of the union of the images of the local algebras, so any quasilocal algebra is already of their size, and a free universe would only add copies of the same algebra higher up. It does buy something important -- a free universe is constrained by no field, so it could not be inferred, and LocalCommutativity would become a family of Props indexed by a universe, making the content of Axiom 3 depend on that index.

• instCStarAlgebra : CStarAlgebra self.carrier

  The CStarAlgebra instance on carrier.

• ι ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ : IsAlexandrovBasisSet B → U.algebra B →⋆ₐ[ℂ] self.carrier

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

  The family is indexed by Alexandrov-basis sets only, matching Isotony.map. It must not be total over all subsets: LocalNet.algebra assigns a type to every subset, including non-basis ones, so a total ι would demand an embedding of those junk fibres into 𝔘 as well. Since dense_range below constrains 𝔘 using the basis sets alone, a net carrying a large algebra on a non-basis subset would then make this structure uninhabitable — density would force 𝔘 small while a unital *-homomorphism out of a simple algebra is automatically injective and would force it large.

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

  Each embedding ι hB is injective, i.e. every local algebra 𝔘(B) embeds faithfully into 𝔘.

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

  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⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂) (a : U.algebra B₁) : (self.ι hB₂) ((i.map hB₁ hB₂ h) a) = (self.ι hB₁) a

  Isotony coherence (the cocone condition): the embeddings into 𝔘 respect the Axiom 2 isotony family, ι B₂ ∘ i.map = ι B₁. An element of 𝔘(B₁) thus embeds into the quasilocal algebra 𝔘 independently of the basis set used to view it, which is exactly what makes ι well defined on the colimit.

  This structure formerly carried its own inclusion family here, duplicating Axiom 2's. It is now parametrised by the Axiom 2 datum i and consumes i.map instead, so there is a single isotony family in the development and the cocone condition relates ι to that family.

theorem Physicslib4.AQFT.HaagKastler.QuasilocalAlgebra.norm_ι {U : LocalNet} {i : Isotony U} (Q : QuasilocalAlgebra U i) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) (a : U.algebra B) : ‖(Q.ι hB) 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} {i : Isotony U} (Q : QuasilocalAlgebra U i) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) : Isometry ⇑(Q.ι hB)

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