This chapter describes how the library states the Haag–Kastler axioms on Minkowski spacetime and
what it proves from them. It corresponds to Section 10.6 of the
blueprint.
The physics is introduced in chapter 1 of the tutorial, and the Lean
needed to read the declarations in chapter 2; this chapter assumes
both.
6.1. Overview🔗
As you will recall, a theory in the Haag–Kastler framework is a net of C*-algebras: to each
bounded region \mathbf{B} of spacetime it assigns an algebra \mathfrak{U}(\mathbf{B}) of
the observables measurable in \mathbf{B}, and the axioms say how these algebras relate. The
library states the axioms in the sharpened form of the blueprint, which fixes the points the 1964
paper leaves open. Five declarations carry them:
-
LocalNet, Axiom 1: a unital C*-algebra \mathfrak{U}(\mathbf{B}) for every causal diamond
\mathbf{B} = I^+(p) \cap I^-(q), with \mathfrak{U}(\emptyset) = \mathbb{C}\mathbf{1};
-
Isotony, Axiom 2: a coherent family of unital *-monomorphisms
i_{\mathbf{B}_1\mathbf{B}_2} : \mathfrak{U}(\mathbf{B}_1) \to \mathfrak{U}(\mathbf{B}_2) for
\mathbf{B}_1 \subseteq \mathbf{B}_2;
-
LocalCommutativity, Axiom 3: the images of the algebras of two completely spacelike diamonds
commute in the algebra of any diamond containing both;
-
LorentzCovariance, Axiom 5: the identity component of the Poincaré group acts on the net by
*-isomorphisms \alpha_L : \mathfrak{U}(\mathbf{B}) \to \mathfrak{U}(L\mathbf{B}) that respect
isotony;
-
HaagKastlerNet, which bundles the four.
Axiom 4, that every physical observable is a quasilocal observable, is a statement about the world,
and is the separate structure ObservableCorrespondence. The quasilocal algebra \mathfrak{U},
which the 1964 axioms take for granted, is constructed: every net satisfying Axiom 2 has one, the
completion of the directed colimit of its local algebras. Primitivity, the sixth axiom of 1964, is
not adopted.
From the axioms the library proves:
-
the consistency of the axioms, by a model, the trivial net;
-
local commutativity in the quasilocal algebra, and its equivalence with Axiom 3;
-
Einstein causality: in every representation of \mathfrak{U}, observables of completely
spacelike diamonds commute as operators on the Hilbert space;
-
the basic properties of the local von Neumann algebras
R(\mathbf{B}) = \pi(\mathfrak{U}(\mathbf{B}))'': isotony, microcausality, and the Schlieder
property;
-
the von Neumann density theorem, by which no finite set of measurements distinguishes an element
of \pi(\mathfrak{U})'', to any given accuracy, from an element of \pi(\mathfrak{U});
-
the extension of the Poincaré action to automorphisms of \mathfrak{U}, and the unitary
implementation of the action in the GNS representation of an invariant state.
It also defines vacuum states, by invariance and the spectrum condition, and KMS and ground states
for a one-parameter subgroup of the Poincaré group. All declarations of the chapter are in the
namespace Physicslib4.AQFT.HaagKastler, written without it below.
6.2. Design🔗
The design decisions behind the axiom structures, and their universes, are summarised in the
conventions chapter, under The axiom structures and
Universes.
The blueprint is the specification: each definition below is checked against its blueprint entry,
which records the reasons for the choices made. This section collects those reasons.
6.2.1. Regions are causal diamonds🔗
The 1964 axioms attach algebras to the open sets of spacetime with compact closure, without naming
the topology. The library uses the Alexandrov topology, whose basic open sets are the causal
diamonds I^+(p) \cap I^-(q), and attaches algebras to the diamonds themselves. The predicate is
IsAlexandrovBasisSet. Chronological rather than causal cones make every diamond open, so no
algebra is attached to a point, and the empty set counts as a diamond, the one with
p \not\ll q; its algebra is \mathbb{C}\mathbf{1}. The
tutorial
explains why diamonds are the right regions physically.
In Lean the field LocalNet.algebra is a function on all subsets of spacetime. This keeps it a
plain function, so that \mathfrak{U}(L\mathbf{B}) is simply U.algebra (L • B). Its values on
sets that are not diamonds are never constrained: every axiom, and every embedding into the
quasilocal algebra, takes a proof hB : IsAlexandrovBasisSet B as an argument, and quantifies only
over diamonds. Indexing the quasilocal embeddings over all subsets would be wrong, not merely
wasteful: the blueprint gives a net for which no such family exists
(thrm:quasilocal-algebra-exists,
first design note).
6.2.2. Isotony is data🔗
The 1964 isotony axiom says \mathfrak{U}(\mathbf{B}_1) \subset \mathfrak{U}(\mathbf{B}_2) for
\mathbf{B}_1 \subseteq \mathbf{B}_2. For abstract algebras, inclusion must be a map, and the
library makes the maps part of the net: Isotony is a structure, not a proposition, with the
family map of unital *-monomorphisms and the laws
i_{\mathbf{B}\mathbf{B}} = \mathrm{id}, \qquad i_{\mathbf{B}_2\mathbf{B}_3} \circ i_{\mathbf{B}_1\mathbf{B}_2} = i_{\mathbf{B}_1\mathbf{B}_3}.
An existence statement, "for each inclusion there is some monomorphism", could not express these
laws, which are equations between particular maps. The laws are required rather than derived:
nothing about the spacetime constrains which monomorphism a net chooses. They make the local
algebras a directed system, and this is what gives the quasilocal algebra a well-defined product
(blueprint
def:isotony).
Because the maps are unital (Mathlib's StarAlgHom preserves \mathbf{1}), the local algebras
have in effect a common unit, as the 1964 Axiom 2 requires; because they are injective, they are
isometric.
Since isotony is data, the later axioms are stated relative to it: LocalCommutativity U i and
LorentzCovariance U i both take the isotony family i as a parameter, and so does
QuasilocalAlgebra U i. There is one isotony family in a net, and every condition refers to it.
6.2.3. Local commutativity in a common diamond🔗
Two completely spacelike diamonds \mathbf{B}_1 and \mathbf{B}_2 have algebras with nothing
in common, so their elements can only be multiplied after both are mapped into one algebra. The
library's Axiom 3 uses the algebra of a diamond \mathbf{B} containing both:
i_{\mathbf{B}_1\mathbf{B}}(a_1)\, i_{\mathbf{B}_2\mathbf{B}}(a_2) = i_{\mathbf{B}_2\mathbf{B}}(a_2)\, i_{\mathbf{B}_1\mathbf{B}}(a_1) \quad\text{for every such } \mathbf{B}.
The statement uses only the net and isotony; in particular it does not use the quasilocal algebra.
In Minkowski spacetime a containing diamond always exists (Spacetime.alexandrovBasis_directed),
and the axiom is equivalent to commutation of \iota_{\mathbf{B}_1}(a_1) and
\iota_{\mathbf{B}_2}(a_2) in the quasilocal algebra, the textbook form. The reason for the
choice is curved spacetime, where two diamonds need not lie in a common diamond and there may be no
quasilocal algebra at all; the same statement then still makes sense, and is the curved-spacetime
Axiom 3. Stating it the same way in both settings lets the Minkowski axioms be read as the special
case (blueprint
def:local-commutativity;
the tutorial works through the equivalence in
chapter 3).
6.2.4. Covariance under the identity component🔗
As you will recall, the Poincaré group has four connected components. The axioms ask only for the
component of the identity, with \det\Lambda = 1 and \Lambda preserving the direction of
time: a theory need not be invariant under parity or time reversal (the weak interaction violates
parity). InhomogeneousLorentzGroup is that component, as pairs (\Lambda, a) acting
by x \mapsto \Lambda x + a; it is a topological group. It maps diamonds to diamonds
(isAlexandrovBasisSet_smul), since \Lambda preserves chronological precedence.
LorentzCovariance U i asserts that there are *-isomorphisms
\alpha_L : \mathfrak{U}(\mathbf{B}) \to \mathfrak{U}(L\mathbf{B}) with \alpha_1 = \mathrm{id},
\alpha_{L'L} = \alpha_{L'} \circ \alpha_L, and
\alpha_L \circ i_{\mathbf{B}_1\mathbf{B}_2} = i_{L\mathbf{B}_1\,L\mathbf{B}_2} \circ \alpha_L.
Two details of the encoding are worth knowing when reading the Lean.
-
The isotony family in the third condition is the net's own i, not one chosen for the purpose,
and the inclusion L\mathbf{B}_1 \subseteq L\mathbf{B}_2 and the fact that both are diamonds are
proved inside the statement, not assumed.
-
\mathfrak{U}(1\mathbf{B}) and \mathfrak{U}(\mathbf{B}) are different types, equal only by
the theorem one_smul; similarly for (L'L)\mathbf{B} and L'(L\mathbf{B}). The first two
conditions transport along these equalities with Eq.mp, which is why they look heavier in Lean
than on paper. HaagKastlerNet.covEquiv chooses the maps, and covEquiv_one, covEquiv_mul and
covEquiv_isotony state the three conditions for them.
The maps \alpha_L act between local algebras. They extend to *-automorphisms \beta_L of the
quasilocal algebra, with \beta_L(\iota_{\mathbf{B}}a) = \iota_{L\mathbf{B}}(\alpha_L a); this is
proved, not assumed, and \beta_L is unique.
6.2.5. The quasilocal algebra is constructed🔗
The 1964 Axiom 4 takes the set-theoretic union of the local algebras to be a normed *-algebra and
completes it, which presupposes that the algebras sit inside one another. In the library the
quasilocal algebra is built from the net: the local algebras, glued along the isotony maps, form a
directed colimit; the norm \|[a]\| = \|a\| is well defined because the isotony maps are
isometric; and the completion is a C*-algebra. Mathlib has no direct limit of C*-algebras, so the
construction is carried out in QuasilocalColimit.lean, and exists_quasilocalAlgebra packages the
result. An alternative, a closed subalgebra of some ambient C*-algebra containing all the local
algebras, is rejected: it would assume the ambient algebra, and nothing in the physics supplies one.
The rest of the library does not see the construction. It uses the structure QuasilocalAlgebra,
which records the properties that characterise a quasilocal algebra: an algebra \mathfrak{U},
embeddings \iota_{\mathbf{B}} compatible with isotony, and density of their images. Results are
stated either for every quasilocal algebra, with Q : QuasilocalAlgebra U i as a hypothesis, or
for the net's own, HaagKastlerNet.quasilocal, which chooses one. The library does not prove that
the quasilocal algebra is unique up to isomorphism, although it is: injective *-homomorphisms of
C*-algebras are isometric, so the norm on the union of the images is forced.
The 1964 Axiom 4 adds that \mathfrak{U} contains "all observables of interest". Once
\mathfrak{U} is constructed, what remains is a claim about physics: every physical observable
corresponds to a self-adjoint element of \mathfrak{U}. The library keeps it apart, as
the structure ObservableCorrespondence, which no theorem about nets uses; HaagKastlerNet
therefore has no field for it (blueprint
def:quasilocal-completeness).
The von Neumann density theorem below is what keeps it consistent with the larger von Neumann
algebras of a representation.
6.2.6. Universes🔗
LocalNet is universe polymorphic: LocalNet.{u} has local algebras in Type u. A quasilocal
algebra of such a net has its carrier in the same universe. A carrier in Type 0 could not contain
injective copies of larger algebras; a free universe would not be inferable, and would make the
quasilocal form of Axiom 3 depend on it. Nothing is lost, since density makes \mathfrak{U} the
closure of the images of the local algebras. HaagKastlerNet names the universe of its field U
so that it, too, is a parameter. The consistency theorem nonempty_haagKastlerNet is stated for
HaagKastlerNet.{0}, since its model is built from \mathbb{C}; one model suffices. Universes in
general are explained in the
tutorial.
6.3. Main definitions and theorems🔗
Definitions are shown with their docstrings, which give the mathematics and the blueprint entry;
theorems with their statements, as Lean prints them, and a line or two of explanation. Each
subsection opens with the blueprint entries it covers. For the declarations not shown here, see the
API documentation
and the files listed at the end of the chapter.
6.3.1. The axioms🔗
Blueprint: def:local-algebras, def:isotony,
def:local-commutativity, def:lorentz-covariance, def:haag-kastler-net.
The regions are the causal diamonds:
🔗def
A set of Minkowski spacetime is an Alexandrov-basis set if it is a causal diamond.
A causal diamond is a set I⁺(p) ∩ I⁻(q), the chronological future of a point p intersected with
the chronological past of a point q. These sets form a basis of the Alexandrov topology, and they
are the regions to which the Haag–Kastler axioms attach local algebras. The diamond is empty unless
p chronologically precedes q, and the empty set is a basis set too.
Implementation note: the predicate is stated on subsets of StandardMinkowskiSpacetime.Carrier,
which is definitionally MinkowskiSpacetime.Carrier, so that it and the completely-spacelike
predicate of Axiom 3 are about the same sets.
Axiom 1 is a structure with three fields. Lean finds the field instCStarAlgebra automatically
(it is an instance), so U.algebra B is a C*-algebra wherever U : LocalNet is in scope:
🔗structure
Axiom 1 (local algebras): a unital C*-algebra 𝔘(B) for each region B of Minkowski spacetime.
The algebra 𝔘(B) is the abstract algebra of the observables that can be measured in B. The
regions that matter are the causal diamonds (IsAlexandrovBasisSet), and the axioms that follow
quantify over those only. The empty region is assigned the one-dimensional algebra ℂ·1 of
multiples of the unit. The algebras are unital because Mathlib's CStarAlgebra is the class of
unital C*-algebras.
Implementation note: algebra is defined on every subset of spacetime, so that it is a plain
function; its values on sets that are not diamonds are never used. The normalisation 𝔘(∅) = ℂ·1
is a *-isomorphism emptyEquivComplex onto ℂ.
Blueprint: def:local-algebras
Fields
emptyEquivComplex : self.algebra ∅ ≃⋆ₐ[ℂ] ℂ
The normalisation 𝔘(∅) = ℂ·1: a *-isomorphism from the algebra of the empty region onto ℂ.
Axiom 2 is a structure over the net. Its fields take the diamond hypotheses explicitly and the
regions as strict-implicit arguments, so the embedding of \mathbf{B}_1 in \mathbf{B}_2 is
written i.map hB₁ hB₂ h, with h : B₁ ⊆ B₂:
🔗structure
Axiom 2 (isotony): a chosen unital *-monomorphism 𝔘(B₁) → 𝔘(B₂) for each inclusion of diamonds.
An observable measurable in a diamond B₁ is also measurable in any larger diamond B₂ ⊇ B₁. Since
the local algebras are abstract, this is expressed by a map i(B₁, B₂) : 𝔘(B₁) → 𝔘(B₂), which is a
unital *-homomorphism and injective. The maps are coherent: i(B, B) is the identity, and
i(B₂, B₃) ∘ i(B₁, B₂) = i(B₁, B₃) for B₁ ⊆ B₂ ⊆ B₃. In other words B ↦ 𝔘(B) is a functor on the
diamonds ordered by inclusion.
The family is data, not an existence statement. The identity and composition laws are equations
between the maps themselves, so they can only be stated once the maps are fixed. They are required
rather than derived, since nothing about the spacetime constrains which monomorphism a net chooses.
They make the local algebras a directed system, which is what makes their directed colimit, and so
the quasilocal algebra (exists_quasilocalAlgebra), an algebra.
Implementation note: a unital *-homomorphism is Mathlib's StarAlgHom, which preserves the unit
because it is an algebra homomorphism.
Blueprint: def:isotony
Axiom 3 is a proposition about a net and its isotony family. Read with the tutorial's
unfolding
of its quantifiers, it is the displayed equation of the Design section:
🔗def
Axiom 3 (local commutativity): observables of completely spacelike diamonds commute.
Let B₁ and B₂ be completely spacelike diamonds: every point of one is spacelike to every point of
the other. To multiply an element of 𝔘(B₁) by one of 𝔘(B₂), both must lie in one algebra. The
axiom takes any diamond B containing both and asks that
i(B₁, B)(a₁) i(B₂, B)(a₂) = i(B₂, B)(a₂) i(B₁, B)(a₁)
in 𝔘(B) for all a₁ ∈ 𝔘(B₁) and a₂ ∈ 𝔘(B₂), where i is the isotony family of Axiom 2. In
Minkowski spacetime such a B always exists (Spacetime.alexandrovBasis_directed), so the
condition is never vacuous. The statement uses the net and isotony only. It is equivalent to the
commutation of ι_B₁(a₁) and ι_B₂(a₂) in a quasilocal algebra
(localCommutativity_iff_exists_commute_ι), and then holds in every quasilocal algebra
(LocalCommutativity.commute_ι).
Blueprint: def:local-commutativity
The symmetry group of Axiom 5, and the axiom itself:
🔗structure
The identity component of the Poincaré group, the symmetry group of Axiom 5.
An element is a pair (Λ, a) of a proper orthochronous Lorentz transformation Λ ∈ SO(1,3)↑ and a
translation a, acting on Minkowski spacetime by x ↦ Λx + a. The product is the composition of
these affine maps, (Λ₁, a₁)(Λ₂, a₂) = (Λ₁Λ₂, a₁ + Λ₁a₂). Haag and Kastler call the Poincaré group
the inhomogeneous Lorentz group. Space and time reflections are not included: a theory need not be
invariant under them (the weak interaction violates parity), and time reversal would act
antilinearly.
The group carries the topology induced by its embedding g ↦ (Λ, Λ⁻¹, a) into a space of bounded
operators and vectors, and is a topological group.
Blueprint: def:inhomogeneous-lorentz-group
Fields
isOrthochronous : IsOrthochronous self.linear
Λ is orthochronous: it preserves the direction of time, (Λe₀)⁰ > 0 for the unit time
vector e₀.
🔗def
Axiom 5 (Lorentz covariance): the Poincaré group acts on the net, compatibly with isotony.
The axiom asks for a unital *-isomorphism α_L : 𝔘(B) → 𝔘(LB) for every element L of the identity
component of the Poincaré group (InhomogeneousLorentzGroup) and every region B, where LB is the
image of B under L, such that
-
α_1 is the identity;
-
α_(L'L) = α_L' ∘ α_L; and
-
α_L commutes with isotony: α_L ∘ i(B₁, B₂) = i(LB₁, LB₂) ∘ α_L for diamonds B₁ ⊆ B₂, where i
is the isotony family of Axiom 2.
In condition 3, LB₁ and LB₂ are diamonds with LB₁ ⊆ LB₂ because L preserves chronological
precedence (isAlexandrovBasisSet_smul, Set.smul_set_mono), so no further hypothesis is
needed. The predicate takes the isotony family as a parameter, so the action respects the net's own
embeddings.
HaagKastlerNet.covEquiv chooses the maps α_L, and HaagKastlerNet.action extends them to
automorphisms of the quasilocal algebra.
Implementation note: 𝔘(1B) and 𝔘(B), and 𝔘((L'L)B) and 𝔘(L'(LB)), are different types that are
equal only propositionally, so conditions 1 and 2 transport along those equalities (one_smul,
mul_smul) with Eq.mp.
Blueprint: def:lorentz-covariance
The bundled net. A theorem about a quantum field theory takes N : HaagKastlerNet as a
hypothesis, and reaches the axioms as N.U, N.isotony, N.localCommutativity and
N.lorentzCovariance:
🔗structure
A Haag–Kastler net on Minkowski spacetime: a net of local algebras satisfying Axioms 1, 2, 3 and 5.
The structure bundles the local algebras B ↦ 𝔘(B) of Axiom 1, the isotony family of Axiom 2, and
proofs of local commutativity (Axiom 3) and Lorentz covariance (Axiom 5). Theorems about a theory
take a HaagKastlerNet as hypothesis and use each axiom as a field.
Two things are not fields. The quasilocal algebra is constructed from the net, as
HaagKastlerNet.quasilocal. Axiom 4, that every physical observable is a quasilocal observable,
relates the formalism to the world rather than constraining the net; it is the separate structure
ObservableCorrespondence. Primitivity, the sixth axiom of 1964, is not adopted.
nonempty_haagKastlerNet shows that the axioms are consistent.
Blueprint: def:haag-kastler-net
Fields
U : LocalNet
The local algebras B ↦ 𝔘(B) (Axiom 1).
Implementation note: the universe is named, as LocalNet.{u}, so that HaagKastlerNet takes it
as a parameter and nets with algebras in any universe are allowed.
isotony : Isotony self.U
The isotony embeddings i(B₁, B₂) : 𝔘(B₁) → 𝔘(B₂) (Axiom 2).
localCommutativity : LocalCommutativity self.U self.isotony
Local commutativity (Axiom 3): for completely spacelike diamonds B₁, B₂ and every diamond
B ⊇ B₁ ∪ B₂, the images of 𝔘(B₁) and 𝔘(B₂) in 𝔘(B) commute.
lorentzCovariance : LorentzCovariance self.U self.isotony
Lorentz covariance (Axiom 5): the identity component of the Poincaré group acts on the net,
compatibly with isotony.
The axioms are consistent. The trivial net, which assigns \mathbb{C} to every region with every
map the identity, satisfies all of them; the
tutorial
builds it step by step.
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.nonempty_haagKastlerNet : Nonempty HaagKastlerNet#check nonempty_haagKastlerNet
Physicslib4.AQFT.HaagKastler.nonempty_haagKastlerNet : Nonempty HaagKastlerNet
The statement is at universe 0, since the model is built from \mathbb{C}, a type in Type.
6.3.2. The quasilocal algebra and Axiom 4🔗
Blueprint: def:quasilocal-algebra, thrm:quasilocal-algebra-exists,
lmm:local-commutativity-any-quasilocal,
lmm:local-commutativity-iff-quasilocal, def:quasilocal-observable,
def:quasilocal-completeness.
The interface through which the library uses the quasilocal algebra:
🔗structure
A quasilocal algebra of a net: a C*-algebra 𝔘 in which the local algebras embed with dense union.
Take the local algebras 𝔘(B) of all diamonds, identify each element of 𝔘(B₁) with its images under
the isotony maps of Axiom 2, and complete in norm. The result is the C*-algebra 𝔘 of the
quasilocal observables, those approximated in norm by observables of bounded regions. This
structure records what characterises it: a unital C*-algebra 𝔘 with an injective unital
*-homomorphism ι_B : 𝔘(B) → 𝔘 for each diamond B, such that
-
ι_B₂ ∘ i(B₁, B₂) = ι_B₁ for B₁ ⊆ B₂ (the embeddings respect isotony), and
-
the union of the images ι_B(𝔘(B)) is dense in 𝔘.
Every net satisfying Axiom 2 has one, built as the completion of the directed colimit of its local
algebras (exists_quasilocalAlgebra), and HaagKastlerNet.quasilocal chooses one for each net. So
the structure describes a constructed object; it is not an extra hypothesis on the net.
Implementation note: Mathlib has no direct limit of C*-algebras, so the construction is carried out
in QuasilocalColimit.lean and QuasilocalExistence.lean; this structure is the interface that
the rest of the library uses.
Blueprint: def:quasilocal-algebra
Fields
carrier : Type u
The quasilocal algebra 𝔘, a type in the universe of the net's local algebras.
Implementation note: a carrier fixed in Type 0 could not contain injective copies of local
algebras in a higher universe, and a free universe could not be inferred and would make the
quasilocal form of Axiom 3 depend on it. Tying it to the net's universe loses nothing, since
density makes 𝔘 the closure of the images of the local algebras.
instCStarAlgebra : CStarAlgebra self.carrier
The quasilocal algebra 𝔘 is a unital C*-algebra.
ι : ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ → IsAlexandrovBasisSet B → U.algebra B →⋆ₐ[ℂ] self.carrier
The embedding ι_B : 𝔘(B) → 𝔘 of the local algebra of a diamond B, a unital *-homomorphism.
Implementation note: ι is defined on diamonds only, as Isotony.map is. An embedding of the
algebras of all subsets would make the structure impossible to build for some nets: density
bounds 𝔘 by the algebras of the diamonds, while a unital *-homomorphism from a large simple
algebra on some other subset into the nonzero algebra 𝔘 would be injective, so 𝔘 would have to
be large too (blueprint: thrm:quasilocal-algebra-exists, first design note).
dense_range : Dense (⋃ B, ⋃ (hB : IsAlexandrovBasisSet B), Set.range ⇑(self.ι hB))
The union of the images ι_B(𝔘(B)) over all diamonds B is dense in 𝔘: 𝔘 is the completion of
the union of the local algebras.
ι_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
The embeddings respect isotony: ι_B₂ ∘ i(B₁, B₂) = ι_B₁ for B₁ ⊆ B₂, with i the isotony
family of Axiom 2. An element of 𝔘(B₁) therefore has the same image in 𝔘 whichever larger diamond
it is viewed in. This is the cocone condition of the directed colimit.
Every net satisfying Axiom 2 has a quasilocal algebra. The proof assembles the colimit-and-completion
construction of QuasilocalColimit.lean; nothing about \mathfrak{U} is assumed.
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.exists_quasilocalAlgebra.{u} (U : LocalNet) (i : Isotony U) :
Nonempty (QuasilocalAlgebra U i)#check exists_quasilocalAlgebra
Physicslib4.AQFT.HaagKastler.exists_quasilocalAlgebra.{u} (U : LocalNet) (i : Isotony U) :
Nonempty (QuasilocalAlgebra U i)
A net's own quasilocal algebra is chosen from this theorem:
🔗def
The quasilocal algebra 𝔘 of the net, with its embeddings ι_B : 𝔘(B) → 𝔘.
The algebra is constructed, not assumed: exists_quasilocalAlgebra builds one from the local
algebras and isotony alone, as the completion of their directed colimit, and this definition
chooses it. Results about the net's quasilocal observables, representations and states are stated
for this algebra.
Blueprint: thrm:quasilocal-algebra-exists
Local commutativity then holds in every quasilocal algebra. The proof picks a diamond containing
both regions, uses the compatibility \iota_{\mathbf{B}} \circ i_{\mathbf{B}_k\mathbf{B}} =
\iota_{\mathbf{B}_k} to move both elements into the image of \mathfrak{U}(\mathbf{B}), and
applies the homomorphism \iota_{\mathbf{B}} to the commutation in \mathfrak{U}(\mathbf{B}):
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.LocalCommutativity.commute_ι.{u_1} {U : LocalNet} {i : Isotony U}
(h : LocalCommutativity U i) (Q : QuasilocalAlgebra U i) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
(hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
(hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) (a : U.algebra B₁)
(b : U.algebra B₂) : Commute ((Q.ι hB₁) a) ((Q.ι hB₂) b)#check LocalCommutativity.commute_ι
Physicslib4.AQFT.HaagKastler.LocalCommutativity.commute_ι.{u_1} {U : LocalNet} {i : Isotony U}
(h : LocalCommutativity U i) (Q : QuasilocalAlgebra U i) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
(hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
(hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) (a : U.algebra B₁)
(b : U.algebra B₂) : Commute ((Q.ι hB₁) a) ((Q.ι hB₂) b)
For a bundled net and its own quasilocal algebra this is HaagKastlerNet.commute_ι_of_spacelike.
Conversely, commutation in a single quasilocal algebra implies Axiom 3; this direction uses the
injectivity of \iota_{\mathbf{B}}. So the library's axiom is equivalent to the textbook form:
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.localCommutativity_iff_exists_commute_ι.{u_1} (U : LocalNet) (i : Isotony U) :
LocalCommutativity U i ↔
∃ Q,
∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁)
(hB₂ : IsAlexandrovBasisSet B₂),
StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂ →
∀ (a : U.algebra B₁) (b : U.algebra B₂), Commute ((Q.ι hB₁) a) ((Q.ι hB₂) b)#check localCommutativity_iff_exists_commute_ι
Physicslib4.AQFT.HaagKastler.localCommutativity_iff_exists_commute_ι.{u_1} (U : LocalNet) (i : Isotony U) :
LocalCommutativity U i ↔
∃ Q,
∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁)
(hB₂ : IsAlexandrovBasisSet B₂),
StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂ →
∀ (a : U.algebra B₁) (b : U.algebra B₂), Commute ((Q.ι hB₁) a) ((Q.ι hB₂) b)
As you will recall, the observables of a theory in a state \omega are the self-adjoint operators
\pi_\omega(a) of its GNS representation. The library defines them for any representation:
🔗def
An operator T is a quasilocal observable in a representation π if T = π(a) with a self-adjoint.
Here π is a *-representation of the quasilocal algebra 𝔘 on a Hilbert space H, in practice the GNS
representation of a state (Physicslib4.GNS.gns_construction), and a is a self-adjoint element of
𝔘. Such an operator is self-adjoint (IsQuasilocalObservable.isSelfAdjoint); conversely the
quasilocal observables are exactly the self-adjoint operators in the range of π
(isQuasilocalObservable_iff).
Blueprint: def:quasilocal-observable
Axiom 4 joins the physical observables to these. Its encoding lands in the algebra, not in a
representation, so that whether a physical observable is quasilocal does not depend on a choice of
state:
🔗structure
Axiom 4 (quasilocal completeness): every physical observable is a quasilocal observable.
Unlike the other axioms, this one relates the formalism to the world: a physical observable is a
quantity that can be measured, not a mathematical object. The structure therefore takes the
physical observables as an uninterpreted type Observable, with a map measure that sends each
to the element of the quasilocal algebra 𝔘 answering it, and asks that every such element be
self-adjoint. Then π(measure o) is a quasilocal observable in every representation π
(isQuasilocalObservable_measure).
The inclusion runs one way only. The axiom says the formalism is not too small: nothing measurable
lies outside 𝔘. It does not say that every self-adjoint element of 𝔘 is measured by some
procedure. Accordingly the structure is easy to inhabit (ObservableCorrespondence.maximal), no
theorem about nets uses it, and HaagKastlerNet does not contain it.
Blueprint: def:quasilocal-completeness
Fields
Observable : Type v
The physical observables, an uninterpreted type.
measure : self.Observable → Q.carrier
The element of the quasilocal algebra 𝔘 that answers each physical observable.
isSelfAdjoint_measure : ∀ (o : self.Observable), IsSelfAdjoint (self.measure o)
The axiom: every physical observable corresponds to a self-adjoint element of 𝔘, and hence
to a quasilocal observable in every representation (isQuasilocalObservable_measure).
Being a quasilocal observable in every representation is then a theorem:
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.isQuasilocalObservable_measure.{u, u_1, u_2} {U : LocalNet} {i : Isotony U}
{Q : QuasilocalAlgebra U i} (C : ObservableCorrespondence Q) {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (o : C.Observable) :
IsQuasilocalObservable Q π (π (C.measure o))#check isQuasilocalObservable_measure
Physicslib4.AQFT.HaagKastler.isQuasilocalObservable_measure.{u, u_1, u_2} {U : LocalNet} {i : Isotony U}
{Q : QuasilocalAlgebra U i} (C : ObservableCorrespondence Q) {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] (π : Q.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (o : C.Observable) :
IsQuasilocalObservable Q π (π (C.measure o))
6.3.3. Representations and local von Neumann algebras🔗
Blueprint: thrm:einstein-causality, def:local-von-neumann,
def:local-von-neumann-algebra, thrm:von-neumann-isotony,
thrm:von-neumann-bundled-order, thrm:statistical-independence-bundled,
thrm:quasilocal-strongly-dense.
The results of this part hold in any *-representation
π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H) of the quasilocal algebra on a complex Hilbert space
H, in particular in the GNS representation of any state. As a StarAlgHom, π is unital.
Einstein causality is local commutativity pushed through π: the operators representing
observables of completely spacelike diamonds commute.
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.einstein_causality.{u, u_1} (N : HaagKastlerNet) {H : Type u_1}
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H)
⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
(hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) (a : N.U.algebra B₁)
(b : N.U.algebra B₂) : Commute (π ((N.quasilocal.ι hB₁) a)) (π ((N.quasilocal.ι hB₂) b))#check HaagKastlerNet.einstein_causality
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.einstein_causality.{u, u_1} (N : HaagKastlerNet) {H : Type u_1}
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H)
⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
(hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) (a : N.U.algebra B₁)
(b : N.U.algebra B₂) : Commute (π ((N.quasilocal.ι hB₁) a)) (π ((N.quasilocal.ι hB₂) b))
HaagKastlerNet.exists_gns_einstein_causality states the same for the GNS triple of a state.
In a representation, the local algebras generate von Neumann algebras. The library defines them in
two forms, as sets of operators and as Mathlib's bundled VonNeumannAlgebra, with the same
underlying set:
🔗def
The local von Neumann algebra R(B) = π(𝔘(B))'' of a diamond B, as a set of operators.
As you will recall, the commutant S' of a set S of bounded operators is the set of bounded
operators commuting with every element of S, and the bicommutant S'' is the commutant of S'. By von
Neumann's bicommutant theorem, π(𝔘(B))'' is the weak operator closure of the unital *-algebra
π(𝔘(B)), and it is in general larger. localVonNeumannAlgebra is the same set as a bundled von
Neumann algebra.
Implementation note: the commutant is Mathlib's Set.centralizer in the bounded operators on H.
Blueprint: def:local-von-neumann
🔗def
The local von Neumann algebra R(B) = π(𝔘(B))'' of a diamond B, as a von Neumann algebra.
The local operators π(𝔘(B)) form a self-adjoint set, and the bicommutant of a self-adjoint set is a
von Neumann algebra (Physicslib4.GNS.vonNeumannOfSelfAdjoint). This is that algebra, an element
of Mathlib's VonNeumannAlgebra; its underlying set is localVonNeumann
(coe_localVonNeumannAlgebra). Inclusions and commutants of local algebras are stated for it with
≤ and VonNeumannAlgebra.commutant.
Blueprint: def:local-von-neumann-algebra
The von Neumann algebras inherit isotony and local commutativity. Isotony, R(\mathbf{B}_1) \le
R(\mathbf{B}_2) for \mathbf{B}_1 \subseteq \mathbf{B}_2, follows from the compatibility of the
embeddings \iota with isotony, and makes \mathbf{B} \mapsto R(\mathbf{B}) a monotone map
(HaagKastlerNet.vonNeumannNet):
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_mono.{u_1, u_2} (N : HaagKastlerNet) {H : Type u_1}
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H)
⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
(h : B₁ ⊆ B₂) : N.localVonNeumannAlgebra π hB₁ ≤ N.localVonNeumannAlgebra π hB₂#check HaagKastlerNet.localVonNeumannAlgebra_mono
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_mono.{u_1, u_2} (N : HaagKastlerNet) {H : Type u_1}
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H)
⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
(h : B₁ ⊆ B₂) : N.localVonNeumannAlgebra π hB₁ ≤ N.localVonNeumannAlgebra π hB₂
Microcausality, R(\mathbf{B}_1) \le R(\mathbf{B}_2)' for completely spacelike diamonds, follows
from Einstein causality, since taking commutants reverses inclusions and S''' = S':
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_le_commutant.{u_1, u_2} (N : HaagKastlerNet)
{H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
(π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
(hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
(hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) :
N.localVonNeumannAlgebra π hB₁ ≤ (N.localVonNeumannAlgebra π hB₂).commutant#check HaagKastlerNet.localVonNeumannAlgebra_le_commutant
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_le_commutant.{u_1, u_2} (N : HaagKastlerNet)
{H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
(π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
(hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
(hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) :
N.localVonNeumannAlgebra π hB₁ ≤ (N.localVonNeumannAlgebra π hB₂).commutant
Statistical independence (the Schlieder property): if \mathbf{B}_1 and \mathbf{B}_2 are
completely spacelike and a vector \Omega is cyclic for the local operators of \mathbf{B}_1,
then \Omega is separating for R(\mathbf{B}_2), so an element of R(\mathbf{B}_2) that
annihilates \Omega is zero. In a vacuum representation the cyclicity is the content of the
Reeh–Schlieder theorem, which the library does not prove; it is a hypothesis here.
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_separating.{u_1, u_2} (N : HaagKastlerNet)
{H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
(π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
(hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
(hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) {Ω : H}
(hcyc : Dense ((fun T => T Ω) '' N.localOperators π hB₁)) {R : H →L[ℂ] H} (hR : R ∈ N.localVonNeumannAlgebra π hB₂)
(hRΩ : R Ω = 0) : R = 0#check HaagKastlerNet.localVonNeumannAlgebra_separating
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_separating.{u_1, u_2} (N : HaagKastlerNet)
{H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
(π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
(hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
(hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) {Ω : H}
(hcyc : Dense ((fun T => T Ω) '' N.localOperators π hB₁)) {R : H →L[ℂ] H} (hR : R ∈ N.localVonNeumannAlgebra π hB₂)
(hRΩ : R Ω = 0) : R = 0
LocalVonNeumann.lean also develops relative commutants
R(\mathbf{B}_1)' \cap R(\mathbf{B}_2) and irreducible inclusions, and
GeometricCovariance.lean shows that a unitary U implementing \beta_L,
U\pi(a)U^{-1} = \pi(\beta_L a), carries R(\mathbf{B}) onto R(L\mathbf{B}).
The von Neumann density theorem keeps Axiom 4 consistent with these algebras. The bicommutant
\pi(\mathfrak{U})'' is in general larger than \pi(\mathfrak{U}), and so contains self-adjoint
operators that are not quasilocal observables. But \pi(\mathfrak{U}) is dense in it in the strong
operator topology: for every T \in \pi(\mathfrak{U})'', finite set of vectors and \varepsilon >
0 there is an a with \|\pi(a)\psi_k - T\psi_k\| < \varepsilon for all k. No finite set of
measurements distinguishes T from \pi(a) to any given accuracy. The theorem is stated for any
unital *-representation of a *-algebra; unitality is essential, since for \pi = 0 the
bicommutant is \mathbb{C}\mathbf{1}. The statement expresses the strong operator topology as the
topology of pointwise convergence, that is, uniform convergence on finite sets, through
UniformConvergenceCLM.ofFun with the family of finite sets:
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.dense_range_in_bicommutant.{u_1, u_2} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {𝔄 : Type u_2} [Ring 𝔄] [StarRing 𝔄] [Algebra ℂ 𝔄]
(π : 𝔄 →⋆ₐ[ℂ] H →L[ℂ] H) :
⇑(UniformConvergenceCLM.ofFun (RingHom.id ℂ) H {s | s.Finite}) '' (Set.range ⇑π).centralizer.centralizer ⊆
closure (⇑(UniformConvergenceCLM.ofFun (RingHom.id ℂ) H {s | s.Finite}) '' Set.range ⇑π)#check dense_range_in_bicommutant
Physicslib4.AQFT.HaagKastler.dense_range_in_bicommutant.{u_1, u_2} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {𝔄 : Type u_2} [Ring 𝔄] [StarRing 𝔄] [Algebra ℂ 𝔄]
(π : 𝔄 →⋆ₐ[ℂ] H →L[ℂ] H) :
⇑(UniformConvergenceCLM.ofFun (RingHom.id ℂ) H {s | s.Finite}) '' (Set.range ⇑π).centralizer.centralizer ⊆
closure (⇑(UniformConvergenceCLM.ofFun (RingHom.id ℂ) H {s | s.Finite}) '' Set.range ⇑π)
The Kaplansky density theorem, which would also make the approximants self-adjoint, is not proved;
the argument above does not need it.
The blueprint section also develops the representation theory used here: irreducibility and
Schur's lemma, unitary equivalence and superselection, disjointness and quasi-equivalence, direct
sums and amplification, and the separating vector of a faithful state. These hold for any
C*-algebra and are formalised in Physicslib4/GNS/
(Section 10.6,
from "Irreducibility and Schur's Lemma"). Purity.lean specialises purity and irreducibility to
the quasilocal algebra.
6.3.4. Symmetry and states🔗
Blueprint: def:covariant-quasilocal-algebra, lmm:quasilocal-lift-unique,
def:invariant-state, thrm:invariant-state-gns-unitary,
def:vacuum-state, def:future-timelike-translation,
def:vacuum-state-concrete, def:kms-state-for-flow-covariance,
def:ground-state-for-flow-covariance.
Axiom 5 acts between local algebras. Its action on the quasilocal algebra is constructed:
🔗def
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
The defining property, \beta_L(\iota_{\mathbf{B}}a) = \iota_{L\mathbf{B}}(\alpha_L a), is
action_ι. (Lean prints the proof that L\mathbf{B} is a diamond as ⋯.)
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.action_ι.{u_1} (N : HaagKastlerNet) (L : InhomogeneousLorentzGroup)
{B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) (a : N.U.algebra B) :
(N.action L) ((N.quasilocal.ι hB) a) = (N.quasilocal.ι ⋯) ((N.covEquiv L B) a)#check HaagKastlerNet.action_ι
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.action_ι.{u_1} (N : HaagKastlerNet) (L : InhomogeneousLorentzGroup)
{B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) (a : N.U.algebra B) :
(N.action L) ((N.quasilocal.ι hB) a) = (N.quasilocal.ι ⋯) ((N.covEquiv L B) a)
The property determines \beta_L: two automorphisms of any quasilocal algebra that satisfy it
agree on the dense union of the local images, and are continuous.
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.QuasilocalLift.unique.{u_1} {N : HaagKastlerNet}
{Q : QuasilocalAlgebra N.U N.isotony} {L : InhomogeneousLorentzGroup} (l₁ l₂ : N.QuasilocalLift Q L) : l₁.β = l₂.β#check HaagKastlerNet.QuasilocalLift.unique
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.QuasilocalLift.unique.{u_1} {N : HaagKastlerNet}
{Q : QuasilocalAlgebra N.U N.isotony} {L : InhomogeneousLorentzGroup} (l₁ l₂ : N.QuasilocalLift Q L) : l₁.β = l₂.β
As you will recall, a state on a unital C*-algebra is a positive linear functional of norm 1; in
the library it is Physicslib4.GNS.State A, a continuous linear functional with
\omega(a^*a) \ge 0 and \|\omega\| = 1. A state of the net is a state on
N.quasilocal.carrier.
🔗def
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
For an invariant state, the library proves that the action is implemented by unitaries on the GNS
space, U(L)\pi(a)\Omega = \pi(\beta_L a)\Omega and U(L)\Omega = \Omega, forming a unitary
representation of the group
(IsInvariantState.exists_gns_unitaryRep).
The representation is strongly continuous when the matrix coefficients
L \mapsto \omega(a^*\beta_L b) are continuous
(IsInvariantState.exists_gns_unitaryRep_strongContinuous),
and irreducible when \omega is also pure
(IsInvariantState.exists_gns_irreducible_covariant).
These statements are long existentials over the Hilbert space and its structure, so they are linked
rather than printed.
A vacuum state adds the spectrum condition. The library states it as positive energy along every
future-timelike translation: the unitary group t \mapsto U(\gamma(t)) is strongly continuous and
its generator is a positive operator (Physicslib4.AQFT.IsPositiveEnergy). By Stone's theorem,
proved in the library, this says U(\gamma(t)) = e^{itA} with A positive and self-adjoint.
🔗def
A vacuum state: a Poincaré-invariant state satisfying the spectrum condition.
A state ω on the quasilocal algebra is a vacuum state, relative to a predicate ftl that selects
the future-timelike translation subgroups, when
-
ω is invariant under the action of the Poincaré group (IsInvariantState); and
-
there is a representation (K, π, Ω) reproducing ω, ω(a) = ⟨Ω, π(a)Ω⟩, with unitaries U(L)
implementing the action, U(L)π(a)Ω = π(β_L a)Ω, such that for every one-parameter subgroup γ
selected by ftl the unitary group t ↦ U(γ(t)) has positive energy (AQFT.IsPositiveEnergy):
it is strongly continuous and its generator, the energy in the direction of γ, is positive.
Condition 2 is the spectrum condition. Positive energy along every future-timelike translation is
equivalent to the textbook form, that the joint spectrum of the energy-momentum operators lies in
the closed forward light cone; that form needs a joint spectral measure for commuting unbounded
operators, which the library does not have. These are necessary conditions for a vacuum; the
library constructs no vacuum state of a nontrivial net.
IsVacuumStateConcrete fixes ftl to IsFutureTimelikeTranslation.
Blueprint: def:vacuum-state
🔗def
A one-parameter subgroup γ is a future-timelike translation: γ(t) = (1, tn), n future timelike.
That is, γ is the translation flow t ↦ (1, tn) (translationFlow) in a direction n that lies in
the open forward light cone at the origin. These are the subgroups on which the spectrum condition
of a vacuum state is imposed (HaagKastlerNet.IsVacuumStateConcrete).
Blueprint: def:future-timelike-translation
🔗def
A vacuum state, with the spectrum condition imposed on the future-timelike translations.
This is IsVacuumState with its predicate fixed to IsFutureTimelikeTranslation: positive energy
is required of exactly the translation subgroups t ↦ (1, tn) with n in the open forward light
cone. The definition has no free parameter.
Blueprint: def:vacuum-state-concrete
The library proves the consequences of a vacuum state that do not use the spectrum condition: it is
invariant (HaagKastlerNet.IsVacuumState.invariant), and if it is pure its GNS representation is
covariant and irreducible
(IsVacuumState.exists_gns_irreducible_covariant).
It does not construct a vacuum state of a nontrivial net, and it does not prove the Reeh–Schlieder
theorem.
Thermal equilibrium is described by KMS states. In Minkowski spacetime every Poincaré
transformation acts on the one algebra \mathfrak{U}, so a one-parameter subgroup t \mapsto
L_t, such as the time translations, defines dynamics on it:
🔗def
The automorphisms t ↦ β_(L_t) of the quasilocal algebra along a curve t ↦ L_t of Poincaré
transformations.
Here β_L is the action HaagKastlerNet.action of L on 𝔘. When t ↦ L_t is a one-parameter subgroup,
for instance the time translations, this is a one-parameter group of automorphisms, the dynamics of
the theory (isOneParameterAut_flowAut).
Blueprint: def:flow-aut-covariance
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isOneParameterAut_flowAut.{u_1} (N : HaagKastlerNet)
(flow : ℝ → InhomogeneousLorentzGroup) (h0 : flow 0 = 1) (hadd : ∀ (s t : ℝ), flow (s + t) = flow s * flow t) :
IsOneParameterAut (N.flowAut flow)#check HaagKastlerNet.isOneParameterAut_flowAut
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isOneParameterAut_flowAut.{u_1} (N : HaagKastlerNet)
(flow : ℝ → InhomogeneousLorentzGroup) (h0 : flow 0 = 1) (hadd : ∀ (s t : ℝ), flow (s + t) = flow s * flow t) :
IsOneParameterAut (N.flowAut flow)
🔗def
A state ω on the quasilocal algebra is a KMS state at inverse temperature β for a flow t ↦ L_t.
As you will recall, the Kubo–Martin–Schwinger condition characterises thermal equilibrium: for
all a, b the correlation function t ↦ ω(a τ_t(b)) extends to a bounded continuous function on the
strip 0 ≤ Im z ≤ β, holomorphic inside, whose values on Im z = β are ω(τ_t(b) a). This definition
is the general KMS condition AQFT.IsKMSState for the automorphisms τ_t = β_(L_t) of 𝔘
(flowAut). In Minkowski spacetime every Poincaré transformation acts on the single algebra 𝔘, so
any one-parameter subgroup may serve as the dynamics.
Blueprint: def:kms-state-for-flow-covariance
The KMS states for a flow at a given temperature form a convex set:
open Physicslib4 AQFT HaagKastler in
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsKMSStateForFlow.convexCombo.{u_1} (N : HaagKastlerNet)
(flow : ℝ → InhomogeneousLorentzGroup) {β : ℝ} {ω₁ ω₂ : GNS.State N.quasilocal.carrier} (s : ℝ) (hs0 : 0 ≤ s)
(hs1 : s ≤ 1) (h₁ : N.IsKMSStateForFlow flow β ω₁) (h₂ : N.IsKMSStateForFlow flow β ω₂) :
N.IsKMSStateForFlow flow β (ω₁.convexCombo ω₂ s hs0 hs1)#check HaagKastlerNet.IsKMSStateForFlow.convexCombo
Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsKMSStateForFlow.convexCombo.{u_1} (N : HaagKastlerNet)
(flow : ℝ → InhomogeneousLorentzGroup) {β : ℝ} {ω₁ ω₂ : GNS.State N.quasilocal.carrier} (s : ℝ) (hs0 : 0 ≤ s)
(hs1 : s ≤ 1) (h₁ : N.IsKMSStateForFlow flow β ω₁) (h₂ : N.IsKMSStateForFlow flow β ω₂) :
N.IsKMSStateForFlow flow β (ω₁.convexCombo ω₂ s hs0 hs1)
The general theory of the KMS condition, including the invariance of a KMS state under its
dynamics at positive inverse temperature, is in Physicslib4/AQFT/KMS.lean
(Physicslib4.AQFT.IsKMSState). At zero temperature the counterpart is a ground state:
🔗def
A ground state for a flow t ↦ L_t: a flow-invariant state in which the flow has a positive
generator.
A state ω on the quasilocal algebra is a ground state for t ↦ L_t when
-
ω(β_(L_t) a) = ω(a) for all t and a; and
-
there is a representation (K, π, Ω) reproducing ω, with unitaries U(t) that fix Ω and implement
the flow, U(t)π(a)Ω = π(β_(L_t) a)Ω, such that t ↦ U(t) has positive energy
(AQFT.IsPositiveEnergy): it is strongly continuous with positive generator.
For a timelike translation the generator is the Hamiltonian. The ground state is the
zero-temperature counterpart of the KMS states of IsKMSStateForFlow.
Blueprint: def:ground-state-for-flow-covariance