AQFT in Lean

5 Axiom 3 (Local Commutativity)

Let us now consider Axiom 3 (Local Commutativity) which states

Axiom 3 (Local Commutativity) If \(\mathbf{B_1}\) and \(\mathbf{B_2}\) are completely spacelike with respect to each other, then \(\mathfrak {U}(\mathbf{B_1})\) and \(\mathfrak {U}(\mathbf{B_2})\) commute.

This axiom is largely self-explanatory. However, there are a couple of aspects that demand clarification.

5.1 Completely Spacelike

First, the term “completely spacelike” as applied to regions \(\mathbf{B}_1\) and \(\mathbf{B}_2\) is never defined. However, it’s relatively clear what is meant.

Two regions \(\mathbf{B}_1\) and \(\mathbf{B}_2\) are completely spacelike if any \(p_1\) in \(\mathbf{B}_1\) one selects is spacelike related to any \(p_2\) in \(\mathbf{B}_2\) one selects. Simple.

5.2 Quasilocal Algebra

The second point that requires clarification is a bit more subtle.

When one requires that \(\mathfrak {U}(\mathbf{B_1})\) and \(\mathfrak {U}(\mathbf{B_2})\) commute, this tacitly implies that \(\mathfrak {U}(\mathbf{B_1})\) and \(\mathfrak {U}(\mathbf{B_2})\) are subalgebras of a single, larger algebra, an algebra in which products and sums of their elements are defined.

Naively one might hope that isotony would come to the rescue. However, this isn’t the case. If, say, \(\mathbf{B_1} \subset \mathbf{B_2}\), isotony would imply that \(\mathfrak {U}(\mathbf{B_1}) \subset \mathfrak {U}(\mathbf{B_2})\). This would place \(\mathfrak {U}(\mathbf{B_1})\) and \(\mathfrak {U}(\mathbf{B_2})\) in a single, larger algebra \(\mathfrak {U}(\mathbf{B_2})\) in which they could commute. However, the assumption that \(\mathbf{B_1} \subset \mathbf{B_2}\) would imply that \(\mathbf{B_1}\) and \(\mathbf{B_2}\) are not completely spacelike. Isotony doesn’t come to the rescue.

However, what does come to the rescue is the quasilocal algebra \(\mathfrak {U}\). By definition \(\mathfrak {U}(\mathbf{B_1}) \subset \mathfrak {U}\) and \(\mathfrak {U}(\mathbf{B_2}) \subset \mathfrak {U}\). So \(\mathfrak {U}(\mathbf{B_1})\) and \(\mathfrak {U}(\mathbf{B_2})\) are in a single, larger algebra \(\mathfrak {U}\). We can thus interpret the statement

If \(\mathbf{B_1}\) and \(\mathbf{B_2}\) are completely spacelike with respect to each other, then \(\mathfrak {U}(\mathbf{B_1})\) and \(\mathfrak {U}(\mathbf{B_2})\) commute.

as the statement

If \(\mathbf{B_1}\) and \(\mathbf{B_2}\) are completely spacelike with respect to each other, then \(\mathfrak {U}(\mathbf{B_1})\) and \(\mathfrak {U}(\mathbf{B_2})\) commute in the quasilocal algebra \(\mathfrak {U}\).

Clarification.