10 Haag Kastler Axioms Blueprint

With all the original Haag Kastler Axioms unpacked, we are now in a position to “sharpen” their formulation.

However, before even stating the “sharpened” axioms, the first thing we need to do is to define a number of terms to a level amenable to auto-formalization and also prove a number of theorems.

10.1 GNS Construction Details

Here we will state and prove the GNS Construction Theorem, which we make use of in the axioms we present later.

We generally follow the clear, straightforward presentation in Entanglement in Algebraic Quantum Field Theories.

10.1.1 GNS Construction Theorem

In this section we will state the GNS Construction Theorem, which we prove in subsequent sections.

Before stating the theorem we’ll need to introduce terminology that appears in the theorem’s statement. We begin with the definition of "state" and some closely associated terms.

Definition 13 State

✓

Let $\mathfrak {U}$ be an abstract C*-algebra. A state is an element $\omega $ of the dual space $\mathfrak {U}^*$ that is

Positive - for any $a \in \mathfrak {U}$ we have $0 \le \omega (a^*a)$ and
Normalized - the operator norm satisfies $\| \omega \| =1$.

Furthermore, a state $\omega $ is said to be faithful if for any non-zero $a$ in $\mathfrak {U}$, it follows that $0 {\lt} \omega (a^*a)$.

We will also have need of the term "cyclic vector".

Definition 14 Cyclic Vector

✓

Let $\mathcal{A}$ be an algebra represented by the bounded operators $\pi (\mathcal{A})$ on the Hilbert space $\mathcal{H}$. A vector $\Omega $ in $\mathcal{H}$ is said to be a cyclic vector if the set

\begin{align} \{ A\Omega : A \in \pi (\mathcal{A}) \} \end{align}

is dense in $\mathcal{H}$.

With this terminology we are then able to state the GNS Construction Theorem.

Theorem 15 GNS Construction Theorem

✓

Let $\omega $ be a state over a unital C*-algebra $\mathfrak {U}$. One can then construct a Hilbert space $\mathcal{H}_\omega $ and *-representation $\pi _\omega $ of $\mathfrak {U}$ by bounded operators on $\mathcal{H}_\omega $ such that

\begin{align} \pi _\omega (a^*) = \pi _\omega (a)^\dagger . \end{align}

As $\mathfrak {U}$ is unital, there exists a cyclic vector $\Omega $ in $\mathcal{H}_\omega $ for the representation $\pi _\omega $ such that

\begin{align} \omega (a) = \left\langle \Omega , \pi _\omega (a)\Omega \right\rangle _{\mathcal{H}_\omega }. \end{align}

The triple $(\mathcal{H}_\omega , \pi _\omega , \Omega )$ is called the GNS triple associated to $(\mathfrak {U}, \omega )$ or the cyclic representation of $(\mathfrak {U}, \omega )$. Furthermore, if $\omega $ is a faithful state, then the *-representation $\pi _\omega $ is faithful. In addition the GNS triple associated to $(\mathfrak {U}, \omega )$ is unique up to unitary equivalence.

With the GNS Construction Theorem stated, we can now commence with its proof.

This proof has five parts: (1) the construction of the GNS Hilbert space $\mathcal{H}_\omega $, (2) the construction of the *-representation $\pi _\omega $, (3) the construction of the cyclic vector $\Omega $ in $\mathcal{H}_\omega $, (4) the proof that the *-representation $\pi _\omega $ is faithful, and (5) the proof of uniqueness up to unitary equivalence. Each part corresponds to a subsequent subsection.

Construction of the GNS Hilbert Space

We’ll construct the GNS Hilbert space $\mathcal{H}_\omega $ from the C*-algebra $\mathfrak {U}$ itself, modifying $\mathfrak {U}$ as needed to obtain the desired $\mathcal{H}_\omega $.

Let’s start by attempting to place an inner product on $\mathfrak {U}$. Naively one might hope the following defines an inner product

\begin{align} \left\langle a, b \right\rangle \equiv \omega (a^*b) \end{align}

on $\mathfrak {U}$. Unfortunately it doesn’t. Let’s examine why this fails.

Consider the set

\begin{align} \mathcal{N} \equiv \{ n \in \mathfrak {U} : \omega (n^*n) = 0 \} . \end{align}

Generically $\omega $ isn’t faithful. Thus in $\mathcal{N}$ there exist non-zero $n$. For such $n$ one has

\begin{align} \left\langle n, n \right\rangle \equiv \omega (n^*n) = 0. \end{align}

Hence, there are non-zero $n$ in $\mathfrak {U}$ such that $\left\langle n, n \right\rangle = 0$. The existence of such $n$ proves that our naive inner product on $\mathfrak {U}$

\begin{align} \left\langle a, b \right\rangle \equiv \omega (a^*b) \end{align}

actually isn’t an inner product. However, the form $\mathcal{N}$ takes gives us a hint as to how to repair this naive inner product.

In particular, if we quotient $\mathfrak {U}$ by $\mathcal{N}$ we may rid ourselves of the problem we encountered above and hopefully be able to construct an inner product on $\mathfrak {U} / \mathcal{N}$ and its completion. We’ll see this plan actually works.

However, before being able to see this plan through we’ll need to take a quick detour and prove a few needed results.

The most famous of these results is the Cauchy-Schwarz Inequality

Lemma 16 Cauchy-Schwarz Inequality

Let $\mathcal{A}$ be a *-algebra and $\omega $ a positive element of the dual space $\mathcal{A}^*$, i.e. $\omega $ is an element of the dual space $\mathcal{A}^*$ such that for any $a \in \mathcal{A}$ one has $0 \le \omega (a^*a)$. Then

\begin{align} \omega (a^*b) & = \overline{\omega (b^*a)} \\ |\omega (a^*b)|^2 & \le \omega (a^*a) \omega (b^*b) \end{align}

for all $a$ and $b$ in $\mathcal{A}$.

Proof ▶

Positivity of $\omega $ implies that for any $a$ and $b$ in $\mathcal{A}$ and $\lambda \in \mathbb {C}$ one has

\begin{align} 0 \le \omega \left((\lambda a + b)^*(\lambda a + b)\right). \end{align}

As $\omega $ is an element of the dual space $\mathcal{A}^*$ and thus linear, this implies

\begin{align} 0 \le |\lambda |^2\omega (a^*a) + \overline{\lambda }\omega (a^*b) + \lambda \omega (b^*a) + \omega (b^*b). \end{align}

This inequality then implies both desired results,

\begin{align} \omega (a^*b) & = \overline{\omega (b^*a)} \\ |\omega (a^*b)|^2 & \le \omega (a^*a) \omega (b^*b). \end{align}

We will prove these one-by-one. Let us first prove this inequality implies $\omega (a^*b) = \overline{\omega (b^*a)}$.

Notice that the inequality is between two real numbers, $0$ and the right-hand side. As $\omega $ is positive, the first and last summands on the right-hand side are obviously real. This then implies

\begin{align} \overline{\lambda }\omega (a^*b) + \lambda \omega (b^*a) \in \mathbb {R}. \end{align}

As $\lambda $ is arbitrary, we are free to choose it to be real, which implies the imaginary parts of $\omega (a^*b)$ and $\omega (b^*a)$ are equal but have the opposite signs.

Similarly, we are free to choose $\lambda $ to be imaginary, which implies that the real parts of $\omega (a^*b)$ and $\omega (b^*a)$ are equal. Together these facts imply the first result

\begin{align} \omega (a^*b) = \overline{\omega (b^*a)}. \end{align}

Let us next prove that our inequality

\begin{align} 0 \le |\lambda |^2\omega (a^*a) + \overline{\lambda }\omega (a^*b) + \lambda \omega (b^*a) + \omega (b^*b) \end{align}

implies $\lvert \omega (a^*b) \rvert ^2 \le \omega (a^*a) \omega (b^*b)$.

Again, as $\lambda $ is arbitrary, we are free to choose it to extremize the right-hand side of the inequality. Extremizing the right-hand of this inequality with respect to $\overline{\lambda }$ and assuming $\omega (a^*a) \ne 0$ one finds at the extrema

\begin{align} \lambda = - \frac{\omega (a^*b)}{\omega (a^*a)}. \end{align}

Substituting this into the inequality, multiplying by $\omega (a^*a)$ while using the fact that $\omega $ is positive, and using $\omega (a^*b) = \overline{\omega (b^*a)}$, then one obtains

\begin{align} 0 \le \lvert \omega (a^*b) \rvert ^2 - \lvert \omega (a^*b) \rvert ^2 - \lvert \omega (a^*b) \rvert ^2 + \omega (a^*a) \omega (b^*b) \end{align}

which implies

\begin{align} \lvert \omega (a^*b) \rvert ^2 \le \omega (a^*a) \omega (b^*b), \end{align}

the second desired result under the assumption that $\omega (a^*a) \ne 0$.

If we now allow for the case $\omega (a^*a) = 0$, our inequality reduces to

\begin{align} 0 \le \overline{\lambda }\omega (a^*b) + \lambda \omega (b^*a) + \omega (b^*b). \end{align}

Our previous result implies $\omega (b^*a) = \overline{\omega (a^*b)}$. Hence, this inequality takes the form

\begin{align} 0 \le \overline{\lambda }\omega (a^*b) + \lambda \overline{\omega (a^*b)} + \omega (b^*b) = 2\text{Re}\left(\overline{\lambda } \omega (a^*b)\right) + \omega (b^*b). \end{align}

Now as $\lambda $ is arbitrary we are free to select it as follows

\begin{align} \overline{\lambda } = -r \overline{\omega (a^*b)} \end{align}

where $0 {\lt} r$ is an arbitrary positive real number. Then the previous inequality takes the form

\begin{align} 0 & \le 2\text{Re}\left(\overline{\lambda } \omega (a^*b)\right) + \omega (b^*b) \\ & = -2r \lvert \omega (a^*b) \rvert ^2 + \omega (b^*b). \end{align}

Now if we assume for the moment that $0 {\lt} \lvert \omega (a^*b) \rvert $, then we can always select $0 {\lt} r$ large enough such that this inequality is violated, the $-2r \lvert \omega (a^*b) \rvert ^2$ term dominating the $\omega (b^*b)$ term. Hence, it must be the case that $\lvert \omega (a^*b) \rvert = 0$.

Now we have $\omega (a^*a) = 0$ and $\lvert \omega (a^*b) \rvert = 0$. Hence, the desired inequality

\begin{align} \lvert \omega (a^*b) \rvert ^2 \le \omega (a^*a) \omega (b^*b), \end{align}

follows trivially, completing our proof.

The next result we need to prove is:

Lemma 17

Let $\omega $ be a state over a unital C*-algebra $\mathfrak {U}$. Then the set $\mathcal{N}_1$ defined by

\begin{align} \mathcal{N}_1 \equiv \{ n \in \mathfrak {U} : \omega (b^*n) = 0 \; \; \forall \, b \in \mathfrak {U} \} \end{align}

is equivalent to the set $\mathcal{N}$ defined by

\begin{align} \mathcal{N} \equiv \{ n \in \mathfrak {U} : \omega (n^*n) = 0 \} . \end{align}

Proof ▶

We will first prove that $\mathcal{N} \subseteq \mathcal{N}_1$. Then we will prove $\mathcal{N}_1 \subseteq \mathcal{N}$. Together these imply $\mathcal{N} = \mathcal{N}_1$, the final desired result.

Let us begin by proving $\mathcal{N} \subseteq \mathcal{N}_1$.

$\mathfrak {U}$ is a C*-algebra and thus a *-algebra. In addition $\omega $ is a state and thus a positive element of the dual space $\mathfrak {U}^*$. Thus, for arbitrary $b$ and $n$ in $\mathfrak {U}$ we can apply the Cauchy-Schwarz inequality to obtain

\begin{align} \lvert \omega (b^*n) \rvert ^2 \le \omega (b^*b) \omega (n^*n). \end{align}

Thus if $n$ is in $\mathcal{N}$, and thus satisfies $\omega (n^*n) = 0$, then this inequality implies $\omega (b^*n) = 0$ for all $b$ in $\mathfrak {U}$. This then implies $n$ is in $\mathcal{N}_1$. As $n$ was an arbitrary element of $\mathcal{N}$, this in turn implies that $\mathcal{N} \subseteq \mathcal{N}_1$, the first desired result.

Next let us prove that $\mathcal{N}_1 \subseteq \mathcal{N}$.

Consider an arbitrary $n_1$ in $\mathcal{N}_1$. By definition $\omega (b^*n_1) = 0$ for any $b$ in $\mathfrak {U}$. In particular we can select $b=n_1$. Doing so we have $\omega (n_1^*n_1) = 0$. This then implies $n_1$ is in $\mathcal{N}$. As $n_1$ was an arbitrary element of $\mathcal{N}_1$ this further implies $\mathcal{N}_1 \subseteq \mathcal{N}$, the second desired result.

We have thus proven $\mathcal{N} \subseteq \mathcal{N}_1$ and $\mathcal{N}_1 \subseteq \mathcal{N}$ which together imply $\mathcal{N} = \mathcal{N}_1$, the final desired result.

Next we will prove $\mathcal{N}$ is a closed, linear subspace of $\mathfrak {U}$. Establishing this will allow us to take the quotient of $\mathfrak {U}$ by $\mathcal{N}$.

Lemma 18

Let $\omega $ be a state over a unital C*-algebra $\mathfrak {U}$. Then the set $\mathcal{N}$ defined by

\begin{align} \mathcal{N} \equiv \{ n \in \mathfrak {U} : \omega (n^*n) = 0 \} . \end{align}

is a closed, linear subspace of $\mathfrak {U}$.

Proof ▶

First let us prove that $\mathcal{N}$ is a linear subspace of $\mathfrak {U}$.

Consider arbitrary $n,m \in \mathcal{N}$ and arbitrary $\lambda , \mu \in \mathbb {C}$. As proven above $\mathcal{N} = \mathcal{N}_1$, thus for arbitrary $b \in \mathfrak {U}$, one has

\begin{align} \omega (b^*n) & = 0 \\ \omega (b^*m) & = 0. \end{align}

Hence, the linearity of $\omega $ then implies

\begin{align} \omega (b^*(\lambda n + \mu m)) = \lambda \omega (b^*n) + \mu \omega (b^*m) = 0. \end{align}

As $b \in \mathfrak {U}$ was arbitrary, this implies that $(\lambda n + \mu m) \in \mathcal{N}_1$. As we previously proved $\mathcal{N} = \mathcal{N}_1$, this in turn implies $(\lambda n + \mu m) \in \mathcal{N}$. Hence $\mathcal{N}$ is a linear subspace of $\mathfrak {U}$, the first desired result.

Next let us prove that $\mathcal{N}$ is a closed subspace of $\mathfrak {U}$.

First, let us note that as $\omega $ is a state, it is by definition a linear, normalized operator on $\mathfrak {U}$. Hence, it is a linear, bounded operator on $\mathfrak {U}$, a normed space. Thus, as a result of the standard theorem (Theorem B.2.4 of Entanglement in Algebraic Quantum Field Theories)

Theorem. Let $X$ and $Y$ be normed spaces and $T: \mathcal{D}(T) \rightarrow Y$ be a linear operator where $\mathcal{D}(T) \subseteq X$. Then $T$ is continuous if and only if it is bounded.

along with the fact that $\mathbb {C}$ is a normed space, it follows that $\omega $ is continuous.

With the continuity of $\omega $ in hand, consider a sequence $(n_i)_{i \in \mathbb {N}}$ in $\mathcal{N}$ that converges to $n$ in $\mathfrak {U}$. As $\omega $ is continuous, for any $b$ in $\mathfrak {U}$ one has

\begin{align} \omega \left(b^*n\right) = \omega \left(b^*(\lim \limits _{i \rightarrow \infty } n_i)\right) = \lim \limits _{i \rightarrow \infty } \omega (b^*n_i) = 0, \end{align}

where the final equality follows from our previous result $\mathcal{N} = \mathcal{N}_1$. This proves that $n$ is an element of $\mathcal{N}_1$ and thus, as a consequence of our previous result $\mathcal{N}_1 = \mathcal{N}$, that $n$ is an element of $\mathcal{N}$. This establishes that $\mathcal{N}$ is closed, proving the second and final desired result, $\mathcal{N}$ is a closed subspace of $\mathfrak {U}$.

As we have established that $\mathcal{N}$ is a closed, linear subspace of $\mathfrak {U}$, we can now take the quotient of $\mathfrak {U}$ by $\mathcal{N}$. Elements of the quotient $\mathfrak {U} / \mathcal{N}$ are equivalence classes of the form

\begin{align} [a] \equiv \{ a + n : n \in \mathcal{N} \} \end{align}

with the zero vector in $\mathfrak {U} / \mathcal{N}$ given by

\begin{align} [0] \equiv \{ n : n \in \mathcal{N} \} . \end{align}

On $\mathfrak {U} / \mathcal{N}$ we can introduce an inner product

\begin{align} \left\langle [a], [b]\right\rangle \equiv \omega (a^*b) \end{align}

motivated by our naive attempt at placing an inner product on $\mathfrak {U}$. This inner product is well-defined on $\mathfrak {U} / \mathcal{N}$ as one can see from its invariance under $a \rightarrow a + n$ where $n$ is in $\mathcal{N}$,

\begin{align} \omega ((a + n)^*b) = \omega (a^*b) + \omega (n^*b) = \omega (a^*b) + \overline{\omega (b^*n)} = \omega (a^*b). \end{align}

In this the first equality follows from $\omega $ being linear, the second from our previous result $\omega (n^*b) = \overline{\omega (b^*n)}$, and the final from our previous result $\mathcal{N} = \mathcal{N}_1$. A similar argument using $\mathcal{N} = \mathcal{N}_1$ yields invariance under $b \rightarrow b + n$ too.

Furthermore, the inner product

\begin{align} \left\langle [a], [b]\right\rangle \equiv \omega (a^*b) \end{align}

on $\mathfrak {U} / \mathcal{N}$ doesn’t suffer from the same problem that our naive inner product on $\mathfrak {U}$ did. In particular, one can easily prove

\begin{align} \left\langle [a], [a]\right\rangle = 0 \end{align}

if and only if $[a] = [0]$. This is essentially by construction.

The final step in going from $\mathfrak {U} / \mathcal{N}$ to the Hilbert space $\mathcal{H}_\omega $ consists of completing $\mathfrak {U} / \mathcal{N}$ in the norm defined by the inner product above. As this is standard, we will not present the details here. The completion of $\mathfrak {U} / \mathcal{N}$ in this norm is the Hilbert space $\mathcal{H}_\omega $ of the GNS Construction Theorem.

Construction of the GNS Representation

Next we will construct $\pi _\omega $ the *-representation of $\mathfrak {U}$ by bounded operators on $\mathcal{H}_\omega $. This will be much easier than the construction of $\mathcal{H}_\omega $.

By construction we can consider $\mathfrak {U} / \mathcal{N}$ as dense in $\mathcal{H}_\omega $. On this dense subset we define the action of $\pi _\omega $ the *-representation of $\mathfrak {U}$ on $\mathfrak {U} / \mathcal{N}$ as follows

\begin{align} \pi _\omega (a)[z] \equiv [az] \end{align}

where $[z]$ is an arbitrary element of $\mathfrak {U} / \mathcal{N}$.

This definition of $\pi _\omega $ on $\mathfrak {U} / \mathcal{N}$ is well-defined as for any other member of the equivalence class $[z]$ of the form $[z + n]$ one has

\begin{align} \pi _\omega (a)[z + n] = [az + an] = [az], \end{align}

where the second equality follows from our previous result $\mathcal{N}_1 = \mathcal{N}$. In other words, $\pi _\omega $ is well-defined as $\mathcal{N}$ is a left-ideal in $\mathfrak {U}$.

Furthermore, it trivially follows from the definition of $\pi _\omega $ that it is linear and an algebraic morphism. So it remains to prove that $\pi _\omega $ is bounded and also a *-morphism.

Let us first prove that $\pi _\omega $ is bounded.

Consider a non-zero $[z]$ in $\mathfrak {U} / \mathcal{N}$. Simply applying definitions one has

\begin{align} \| \pi _\omega (a)[z]\| ^2 & = \| [az]\| ^2 \\ & = \left\langle [az], [az]\right\rangle \\ & = \omega ((az)^*(az)) \\ & = \omega (z^*(a^*a)z) \\ & = \frac{\omega (z^*(a^*a)z)}{\omega (z^*z)} \omega (z^*z) \\ & = \frac{\omega (z^*(a^*a)z)}{\omega (z^*z)} \| [z]\| ^2. \end{align}

With that last equation in mind let us define the map $\phi $ acting on $\mathfrak {U}$ by

\begin{align} \phi (a) \equiv \frac{\omega (z^*az)}{\omega (z^*z)}. \end{align}

One can easily check that $\phi $ when acting on $\mathfrak {U}$ is linear and positive as

\begin{align} \phi (c^*c) = \frac{\omega (z^*(c^*c)z)}{\omega (z^*z)} = \frac{\omega ((cz)^*(cz))}{\omega (z^*z)} \ge 0 \end{align}

as a result of $\omega $ being positive.

Now as $\phi $ is a positive, linear function on the unital C*-algebra $\mathfrak {U}$ we can invoke the theorem (Chapter III Theorem 2.2.9 of Haag)

Theorem. A positive, linear operator $\phi $ on a unital Banach *-algebra $\mathcal{A}$ is bounded and satisfies
\begin{align} \| \phi \| = \phi (\mathbf{1}) \end{align}
where $\phi (\mathbf{1})$ is $\phi $ acting on the unit $\mathbf{1}$ of $\mathcal{A}$.

to prove that $\| \phi \| = \phi (\mathbf{1})$. A short computation finds

\begin{align} \phi (\mathbf{1}) = \frac{\omega (z^*\mathbf{1}z)}{\omega (z^*z)} = 1 \end{align}

proving $\| \phi \| =1$, i.e. $\phi $ is normalized. As $\phi $ is a linear, positive, normalized operator on the unital C*-algebra $\mathfrak {U}$, it is indeed a state.

Now as $\phi $ is normalized and thus $\| \phi \| =1$, the definition of the norm $\| \phi \| $ implies

\begin{align} \| \phi (c)\| \le \| \phi \| \, \| c\| = \| c\| . \end{align}

This along with our previous derivation gives

\begin{align} \| \pi _\omega (a)[z]\| ^2 & = \phi (a^*a) \| [z]\| ^2 \\ & \le \| \phi \| \, \| a^*a\| \, \| [z]\| ^2 \\ & = \| a^*a\| \, \| [z]\| ^2 \\ & = \| a\| ^2 \, \| [z]\| ^2. \end{align}

Using the definition of the norm $\| \pi _\omega (a)\| $ this equation then implies

\begin{align} \| \pi _\omega (a)\| \le \| a\| \end{align}

which is the statement that $\pi _\omega (a)$ is a bounded operator on $\mathfrak {U} / \mathcal{N}$.

Thus using the following standard theorem (Theorem A.36 Hall)

Bounded Linear Transformation Theorem. Let $V_1$ be a normed space and $V_2$ a Banach space. Suppose $W$ is a dense subspace of $V_1$ and $T: W \rightarrow V_2$ is a bounded linear map. Then there exists a unique bounded linear map $\widetilde{T}: V_1 \rightarrow V_2$ such that $\widetilde{T}|_W = T$. Furthermore, the norm of $\widetilde{T}$ equals the norm of $T$.

one can extend $\pi _\omega $ from the dense subset $\mathfrak {U} / \mathcal{N}$ of $\mathcal{H}_\omega $ to all of $\mathcal{H}_\omega $. We do so and use the same notation $\pi _\omega $ for this extension.

Finally we need to prove that $\pi _\omega $ is not only an algebraic morphism but is a *-morphism. Thankfully this is relatively simple.

For $[x]$ and $[y]$ in $\mathfrak {U} / \mathcal{N}$ and $a$ in $\mathfrak {U}$, we have

\begin{align} \left\langle [x], \pi _\omega (a^*)[y]\right\rangle & = \left\langle [x], [a^*y]\right\rangle \\ & = \omega (x^*a^*y) \\ & = \omega ((ax)^*y) \\ & = \left\langle [ax], [y]\right\rangle \\ & = \left\langle \pi _\omega (a)[x], [y]\right\rangle \\ & = \left\langle [x], \pi _\omega (a)^\dagger [y]\right\rangle \end{align}

Hence, $\pi _\omega (a^*) = \pi _\omega (a)^\dagger $ and $\pi _\omega $ is a *-morphism.

Construction of the Cyclic Vector

Our next task is to construct the cyclic vector $\Omega $. This is relatively straightforward.

As $\mathfrak {U}$ is unital we can make the definition

\begin{align} \Omega \equiv [\mathbf{1}]. \end{align}

Tracing definitions we have

\begin{align} \{ \pi _\omega (a)\Omega : a \in \mathfrak {U}\} = \{ [a] : a \in \mathfrak {U}\} = \mathfrak {U} / \mathcal{N}. \end{align}

As $\mathfrak {U} / \mathcal{N}$ is dense in $\mathcal{H}_\omega $, this implies that $\Omega $ is a cyclic vector in $\mathcal{H}_\omega $ for the representation $\pi _\omega $, the property claimed of $\Omega $ in the GNS Construction Theorem.

In addition tracing definitions gives

\begin{align} \left\langle \Omega , \pi _\omega (a)\Omega \right\rangle = \left\langle [\mathbf{1}], \pi _\omega (a)[\mathbf{1}]\right\rangle = \left\langle [\mathbf{1}], [a]\right\rangle = \omega (\mathbf{1}a) = \omega (a) \end{align}

which proves another relation

\begin{align} \omega (a) = \left\langle \Omega , \pi _\omega (a)\Omega \right\rangle \end{align}

claimed in the GNS Construction Theorem.

Faithfulness of the GNS Representation

Now we are going to prove the *-representation $\pi _\omega $ is faithful if $\omega $ is a faithful state.

For this section of the proof, assume that $\omega $ is a faithful state.

To prove that $\pi _\omega $ is a faithful representation, we must prove that $\ker \pi _\omega = \{ 0\} $. In other words, we must prove that $\pi _\omega (a) = 0$ implies that $a=0$.

Assume that $\pi _\omega (a) = 0$. Thus we have

\begin{align} 0 = \left\langle \pi _\omega (a)\Omega , \pi _\omega (a)\Omega \right\rangle = \omega (a^*a). \end{align}

As $\omega $ is assumed faithful in this section of the proof, this implies that $a=0$. This in turn implies $\ker \pi _\omega = \{ 0\} $, which proves that if $\omega $ is faithful, then $\pi _\omega $ is faithful, the desired result.

Uniqueness up to Unitary Equivalence

Finally to complete the proof of the GNS Construction Theorem we now prove that the GNS triple associated to $(\mathfrak {U}, \omega )$ is unique up to unitary equivalence.

To that end let $(\mathcal{H}_\omega ', \pi _\omega ', \Omega ')$ be a second GNS triple associated to $(\mathfrak {U}, \omega )$. (This implies, in particular, that the inner product on $\mathcal{H}_\omega '$ is given by $\omega $.) Then define an operator $U$ by

\begin{align} U\pi _\omega (a)\Omega \equiv \pi _\omega (a)’\Omega ’. \end{align}

The operator $U$ is obviously linear. Furthermore, as $\Omega $ and $\Omega '$ are cyclic, the domain of $U$ is dense in $\mathcal{H}_\omega $ and its range is dense in $\mathcal{H}_\omega '$. Now, as a result of chasing definitions

\begin{align} \left\langle U\pi _\omega (a)\Omega , U\pi _\omega (b)\Omega \right\rangle ’ & = \left\langle \pi _\omega (a)’\Omega ’, \pi _\omega (b)’\Omega ’\right\rangle ’ \\ & = \omega (a^*b) \\ & = \left\langle \pi _\omega (a)\Omega , \pi _\omega (b)\Omega \right\rangle \end{align}

we find that $U$ preserves the inner product and is thus bounded. Furthermore, as $U$ preserves the inner product on its dense domain and dense range, it’s also unitary there.

As $U$ is bounded on its dense domain, the Bounded Linear Transformation Theorem (Theorem A.36 Hall)

Bounded Linear Transformation Theorem. Let $V_1$ be a normed space and $V_2$ a Banach space. Suppose $W$ is a dense subspace of $V_1$ and $T: W \rightarrow V_2$ is a bounded linear map. Then there exists a unique bounded linear map $\widetilde{T}: V_1 \rightarrow V_2$ such that $\widetilde{T}|_W = T$. Furthermore, the norm of $\widetilde{T}$ equals the norm of $T$.

can be used to extend the domain of $U$ to all of $\mathcal{H}_\omega $. This gives a well-defined, unitary map from $\mathcal{H}_\omega $ to $\mathcal{H}_\omega '$ that we also denote by $U : \mathcal{H}_\omega \rightarrow \mathcal{H}_\omega '$.

Now, the definition of $U$

\begin{align} U\pi _\omega (a)\Omega = \pi _\omega (a)’\Omega ’. \end{align}

gives for the case $a = \mathbf{1}$

\begin{align} U\Omega = \Omega ’. \end{align}

Hence, the fact that $U$ is unitary and thus $U^{-1}$ is well-defined gives

\begin{align} \left\langle U\pi _\omega (a)\Omega , U\pi _\omega (b)\Omega \right\rangle ’ & = \left\langle U\pi _\omega (a)U^{-1}U\Omega , U\pi _\omega (b)\Omega \right\rangle ’ \\ & = \left\langle U\pi _\omega (a)U^{-1}U\Omega , \pi _\omega (b)’\Omega ’ \right\rangle ’ \\ & = \left\langle U\pi _\omega (a)U^{-1}\Omega ’, \pi _\omega (b)’\Omega ’ \right\rangle ’. \end{align}

However, the definition of $U$ implies

\begin{align} \left\langle U\pi _\omega (a)\Omega , U\pi _\omega (b)\Omega \right\rangle ’ = \left\langle \pi _\omega (a)’\Omega ’, \pi _\omega (b)’\Omega ’\right\rangle ’. \end{align}

Thus the previous two equations imply

\begin{align} \left\langle U\pi _\omega (a)U^{-1}\Omega ’, \pi _\omega (b)’\Omega ’ \right\rangle ’ = \left\langle \pi _\omega (a)’\Omega ’, \pi _\omega (b)’\Omega ’\right\rangle ’. \end{align}

As a result of cyclicity of $\Omega '$ this implies that

\begin{align} U\pi _\omega (a)U^{-1}\Omega ’ = \pi _\omega (a)’\Omega ’. \end{align}

To complete the proof we must first show that $U\pi _\omega (a)U^{-1}$ and $\pi _\omega (a)'$ agree not only on $\Omega '$, but also on $\pi _\omega (c)'\Omega '$, which as $\Omega '$ is cyclic is dense in $\mathcal{H}_\omega '$. This can then be used along with the Bounded Linear Transformation Theorem to prove that $U\pi _\omega (a)U^{-1}$ and $\pi _\omega (a)'$ agree on $\mathcal{H}_\omega '$.

Let us first prove that $U\pi _\omega (a)U^{-1}$ and $\pi _\omega (a)'$ agree on $\pi _\omega (c)'\Omega '$. We have

\begin{align} U\pi _\omega (a)U^{-1} \pi _\omega (c)’\Omega ’ & = U\pi _\omega (a)U^{-1} U\pi _\omega (c)U^{-1} \Omega ’ \\ & = U\pi _\omega (a)\pi _\omega (c)U^{-1} \Omega ’ \\ & = U\pi _\omega (ac)U^{-1} \Omega ’ \\ & = \pi _\omega (ac)’ \Omega ’ \\ & = \pi _\omega (a)’\pi _\omega (c)’ \Omega ’ \end{align}

Thus $U\pi _\omega (a)U^{-1}$ and $\pi _\omega (a)'$ agree on $\pi _\omega (c)'\Omega '$.

As $\Omega '$ is cyclic, $\pi _\omega (c)'\Omega '$ is dense in $\mathcal{H}_\omega '$, and thus the Bounded Linear Transformation Theorem (Theorem A.36 Hall)

Bounded Linear Transformation Theorem. Let $V_1$ be a normed space and $V_2$ a Banach space. Suppose $W$ is a dense subspace of $V_1$ and $T: W \rightarrow V_2$ is a bounded linear map. Then there exists a unique bounded linear map $\widetilde{T}: V_1 \rightarrow V_2$ such that $\widetilde{T}|_W = T$. Furthermore, the norm of $\widetilde{T}$ equals the norm of $T$.

can be invoked to prove that $U\pi _\omega (a)U^{-1}$ and $\pi _\omega (a)'$ agree on $\mathcal{H}_\omega '$, proving that

\begin{align} \pi _\omega (a)’ = U\pi _\omega (a)U^{-1}, \end{align}

and two GNS triples associated to $(\mathfrak {U}, \omega )$ can differ at most by a unitary transformation, completing our proof of the GNS Construction Theorem.

10.1.2 Summary

This concludes the proof of the GNS Construction Theorem (see Theorem 15). To summarise: given a state $\omega $ over a unital C*-algebra $\mathfrak {U}$ one can construct a Hilbert space $\mathcal{H}_\omega $, a *-representation $\pi _\omega $ of $\mathfrak {U}$ by bounded operators on $\mathcal{H}_\omega $ satisfying $\pi _\omega (a^*) = \pi _\omega (a)^\dagger $, and a cyclic vector $\Omega $ in $\mathcal{H}_\omega $ such that

\begin{align} \omega (a) = \left\langle \Omega , \pi _\omega (a)\Omega \right\rangle _{\mathcal{H}_\omega }. \end{align}

The triple $(\mathcal{H}_\omega , \pi _\omega , \Omega )$ is called the GNS triple associated to $(\mathfrak {U}, \omega )$, or the cyclic representation of $(\mathfrak {U}, \omega )$. If $\omega $ is faithful then so is $\pi _\omega $, and the GNS triple is unique up to unitary equivalence.

The reason we provided such detail is that we will have need not only of the theorem, but also of the details of the theorem’s proof in subsequent blog posts.

10.2 Spacetime

Definition 19 Spacetime

✓

A spacetime is a real, four-dimensional, connected, smooth, Hausdorff manifold $M$ with a globally defined smooth tensor field $g$ of type $(0,2)$ which is non-degenerate and “Lorentzian”. By Lorentzian we mean that for any $p \in M$ there is a basis of the tangent space $TM|_p$ to $M$ at $p$ relative to which $g|_p$ is zero in its non-diagonal entries and on the diagonal takes the form $\text{diag}(-1,1,1,1)$.

Definition 20 Standard Minkowski Spacetime

✓

Standard Minkowski spacetime is a spacetime in which the underlying real, four-dimensional, connected, smooth, Hausdorff manifold is $\mathbb {R}^4$ with the Euclidean topology. In addition $g$ takes the form $g|_p=\text{diag}(-1,1,1,1)$ for all $p$ in $\mathbb {R}^4$ with respect to the standard coordinates on $\mathbb {R}^4$.

Definition 21 Timelike, Spacelike, or Null Vectors

✓

Let $M$ be a spacetime, $p$ a point in $M$, and $g$ the tensor field of type $(0,2)$ associated to $M$. Any tangent vector $v \in TM|_p$ is timelike, spacelike, or null if $g|_p(v,v)$ is negative, positive, or zero respectively.

Lemma 22 Causal Classification

✓

Every tangent vector $v \in TM|_p$ is exactly one of timelike, null, or spacelike. In particular the three classes are mutually exclusive, and the zero vector is null.

Proof ▶

Immediate from the trichotomy of ${\lt}$, $=$, ${\gt}$ applied to $g|_p(v,v)$, together with $g|_p(0,0) = 0$ since $g|_p$ is bilinear.

Lemma 23 Reverse Cauchy-Schwarz for Timelike Vectors

Let $g$ be a symmetric Lorentzian bilinear form on a real four-dimensional vector space and let $v, w$ be timelike, that is $g(v,v) {\lt} 0$ and $g(w,w) {\lt} 0$. Then the reverse Cauchy-Schwarz inequality holds:

\begin{align} g(v,v)\, g(w,w) \le g(v,w)^2. \end{align}

In particular this applies pointwise to the metric $g|_p$ of any spacetime $M$ and any two timelike tangent vectors at a point $p$.

Proof ▶

Choose a Lorentzian basis $b$, so that $g$ has Gram matrix $\mathrm{diag}(-1,1,1,1)$. Expanding $v$ and $w$ in this basis and using bilinearity, $g(v,v) = -(v^0)^2 + \lVert \mathbf{v}\rVert ^2$ and $g(v,w) = -v^0 w^0 + \langle \mathbf{v}, \mathbf{w}\rangle $, where $v^0, w^0$ are the time components, $\mathbf{v}, \mathbf{w}$ the spatial parts, and $\langle \cdot ,\cdot \rangle $, $\lVert \cdot \rVert $ the Euclidean inner product and norm on the three spatial coordinates. Timelikeness gives $(v^0)^2 {\gt} \lVert \mathbf{v}\rVert ^2$ and $(w^0)^2 {\gt} \lVert \mathbf{w}\rVert ^2$. The ordinary Cauchy-Schwarz inequality gives $\lvert \langle \mathbf{v},\mathbf{w}\rangle \rvert \le \lVert \mathbf{v}\rVert \, \lVert \mathbf{w}\rVert {\lt} \lvert v^0\rvert \, \lvert w^0\rvert $, so $\lvert g(v,w)\rvert \ge \lvert v^0 w^0\rvert - \lVert \mathbf{v}\rVert \, \lVert \mathbf{w}\rVert \ge 0$. Squaring and applying the algebraic identity

\begin{align} (pq - rs)^2 - (p^2 - r^2)(q^2 - s^2) = (ps - rq)^2 \ge 0 \end{align}

with $p = \lvert v^0\rvert $, $q = \lvert w^0\rvert $, $r = \lVert \mathbf{v}\rVert $, $s = \lVert \mathbf{w}\rVert $ yields $g(v,w)^2 \ge g(v,v)\, g(w,w)$.

Lemma 24 Timelike Cone Convexity and Reverse Triangle Inequality

Let $g$ be a symmetric Lorentzian bilinear form on a real four-dimensional vector space and let $v, w$ be timelike and aligned, that is $g(v,v) {\lt} 0$, $g(w,w) {\lt} 0$ and $g(v,w) \le 0$. Then $v + w$ is timelike, and the reverse (Lorentzian) triangle inequality holds:

\begin{align} \sqrt{-g(v,v)} + \sqrt{-g(w,w)} \le \sqrt{-g(v+w,\, v+w)}. \end{align}

In particular the timelike vectors sharing a time cone (so that $g(v,w) \le 0$) form a convex cone, and this applies pointwise to the metric $g|_p$ of any spacetime.

Proof ▶

Bilinearity and symmetry give $g(v+w,v+w) = g(v,v) + 2g(v,w) + g(w,w)$. Writing $a = -g(v,v) {\gt} 0$, $b = -g(w,w) {\gt} 0$ and $c = -g(v,w) \ge 0$, this equals $-(a + b + 2c) {\lt} 0$, so $v+w$ is timelike. The reverse Cauchy-Schwarz inequality (23) gives $g(v,w)^2 \ge g(v,v)\, g(w,w)$, that is $c^2 \ge ab$, hence $c \ge \sqrt{ab} = \sqrt a \, \sqrt b$. Therefore $-g(v+w,v+w) = a + b + 2c \ge a + b + 2\sqrt a\, \sqrt b = (\sqrt a + \sqrt b)^2$, and taking square roots yields the reverse triangle inequality.

Definition 25 Time Orientation

✓

A spacetime $M$ is time-orientable if it admits a smooth, non-vanishing vector field $t$ that is timelike. Such a smooth, non-vanishing vector field is called a time-orientation.

Definition 26 Future and Past Pointing Vectors

✓

For any $p$ in a spacetime $M$ a timelike tangent vector $v \in TM|_p$ is future-pointing if $g|_p(t,v)$ is negative and past-pointing if $g|_p(t,v)$ is positive. A null tangent vector $n \in TM|_p$ is future-pointing if it is the limit of future-pointing timelike tangent vectors and it is past-pointing if it is the limit of past-pointing timelike tangent vectors.

Lemma 27 Orientation of Pointing Vectors

✓

A future-pointing or past-pointing vector is timelike or null. Moreover a timelike vector cannot be both future-pointing and past-pointing with respect to a fixed time orientation.

Proof ▶

The first claim is immediate from the definition, which is a disjunction over the timelike and null cases. For the second, a timelike $v$ is not null, so both pointing conditions reduce to their timelike branches $g|_p(t,v) {\lt} 0$ and $g|_p(t,v) {\gt} 0$, which cannot hold simultaneously.

Lemma 28 Sign Lemma for the Future Cone

Let $g$ be a symmetric Lorentzian bilinear form, $t$ a timelike vector, and write $t^\perp = \{ u : g(t,u) = 0\} $ for the spacelike complement. Then $g$ is positive semidefinite on $t^\perp $ (so the ordinary Cauchy-Schwarz inequality holds there), and consequently for any timelike $v, w$ with $g(t,v) {\lt} 0$ and $g(t,w) {\lt} 0$ one has $g(v,w) {\lt} 0$. In particular two timelike tangent vectors that are future-pointing with respect to a common time orientation have negative inner product; by time reversal the same holds for two past-pointing timelike vectors (with $g(t,v) {\gt} 0$ and $g(t,w) {\gt} 0$).

Proof ▶

If $u \in t^\perp $ had $g(u,u) {\lt} 0$ then $u$ would be timelike, and reverse Cauchy-Schwarz (23) would give $g(t,t)\, g(u,u) \le g(t,u)^2 = 0$, contradicting $g(t,t)\, g(u,u) {\gt} 0$; hence $g$ is positive semidefinite on $t^\perp $, and Cauchy-Schwarz follows from nonnegativity of the quadratic $s \mapsto g(s u + u', s u + u')$. For the sign claim, decompose $v$ and $w$ along $t$: the vectors $v_\perp = g(t,t)\, v - g(t,v)\, t$ and $w_\perp = g(t,t)\, w - g(t,w)\, t$ lie in $t^\perp $, and $g(v,w) = g(t,t)^{-2}\big(g(t,t)\, g(v,w)\big)$ expands so that $g(t,t)\, g(v,w) = g(t,v)\, g(t,w) + g(v_\perp , w_\perp )/g(t,t)$. Applying Cauchy-Schwarz to $g(v_\perp ,w_\perp )$ together with the reverse Cauchy-Schwarz bounds $g(t,v)^2 \ge g(t,t)g(v,v)$ and $g(t,w)^2 \ge g(t,t)g(w,w)$ forces $g(t,t)\, g(v,w) {\gt} 0$, and since $g(t,t) {\lt} 0$ this gives $g(v,w) {\lt} 0$.

Lemma 29 Definiteness of the Spacelike Complement

A Lorentzian bilinear form is nondegenerate: if $g(v,w) = 0$ for every $w$, then $v = 0$ (this is read off the signature basis, on which the Gram matrix $\mathrm{diag}(-1,1,1,1)$ is invertible). Consequently $g$ is positive definite on the spacelike complement: if $t$ is timelike and $u \ne 0$ satisfies $g(t,u) = 0$, then $g(u,u) {\gt} 0$, i.e. $u$ is spacelike.

Proof ▶

Nondegeneracy follows because $g(v, b_j) = (b.\mathrm{repr}\, v)_j \cdot \mathrm{diag}(-1,1,1,1)_{jj}$ in the signature basis $b$, and the diagonal entries are nonzero; so $g(v, \cdot ) = 0$ forces every coordinate of $v$ to vanish. For definiteness, semidefiniteness (28) gives $g(u,u) \ge 0$; if $g(u,u) = 0$ then for any $u' \in t^\perp $ Cauchy-Schwarz gives $g(u,u')^2 \le g(u,u)\, g(u',u') = 0$, so $u$ is orthogonal to all of $t^\perp $, and since it is also orthogonal to $t$ it is orthogonal to everything, whence $u = 0$ by nondegeneracy, contradicting $u \ne 0$.

Lemma 30 Convexity of the Future Cone

The sum of two timelike future-pointing tangent vectors (with respect to a fixed time orientation) is again timelike and future-pointing. More generally, the sum of any two future-pointing tangent vectors – timelike or null – is future-pointing, so the full future cone, including its null boundary, is convex. Since a vector is past-pointing exactly when its negation is future-pointing, the past cone is convex as well. Downstream this packages as the statement that the future-pointing and past-pointing tangent vectors each form a convex cone: they are closed under positive scaling and, more generally, under positive linear combinations $a v + b w$ with $a, b {\gt} 0$.

Proof ▶

For two timelike future-pointing $v, w$ we have $g(t,v) {\lt} 0$ and $g(t,w) {\lt} 0$. By the sign lemma (28) $g(v,w) {\lt} 0$, so $v$ and $w$ are aligned and $v + w$ is timelike by cone convexity (24); moreover $g(t, v+w) = g(t,v) + g(t,w) {\lt} 0$, so $v + w$ is future-pointing. For the general case, every future-pointing vector is a limit of future-pointing timelike vectors (the constant sequence if timelike, the approximating sequence from the definition if null). Approximating $v$ and $w$ by such sequences $v_n, w_n$, each $v_n + w_n$ is timelike future-pointing by the timelike case. Passing to the limit gives $g(v,w) \le 0$ (continuity of the fixed maps $u \mapsto g(a,u)$ with symmetry), so $g(v+w,v+w) = g(v,v) + 2g(v,w) + g(w,w) \le 0$ and $v+w$ is causal, and $g(t,v+w) = g(t,v) + g(t,w) \le 0$. If $g(v+w,v+w) {\lt} 0$ the sum is timelike and reverse Cauchy-Schwarz makes $g(t,v+w) \ne 0$, hence negative, so the sum is future-pointing timelike; if $g(v+w,v+w) = 0$ the sum is null and is the limit of the future-pointing timelike sequence $v_n + w_n$, hence future-pointing null.

Definition 31 Paths

✓

A path is a continuous map $\mu :\Sigma \rightarrow M$ from the parameter space–a closed, connected subset $\Sigma $ of $\mathbb {R}$ that contains more than a single point–to a spacetime $M$. A smooth path is a path $\mu $ that is smooth and has a non-vanishing derivative.

Definition 32 Curves

✓

A curve is an equivalence class of paths equivalent under homeomorphisms of the parameter space. A smooth curve is an equivalence class of smooth paths equivalent under diffeomorphisms of the parameter space.

Definition 33 Timelike and Causal Smooth Curves

✓

A timelike smooth curve is a smooth curve with a tangent vector that is timelike at every point along the smooth curve. A causal smooth curve is a smooth curve with a tangent vector that is timelike or null at every point along the smooth curve.

Definition 34 Future and Past Oriented Smooth Curves

✓

A future-oriented smooth curve is a smooth curve with a tangent vector that is future-pointing at every point. A past-oriented smooth curve is a smooth curve with a tangent vector that is past-pointing at every point.

Definition 35 Endpoints

✓

A point $p$ in a spacetime $M$ is the endpoint of a path $\mu $ or its associated curve if it is a member of the image $\mu (\partial \Sigma )$ of the boundary $\partial \Sigma $ of the parameter space under $\mu $. If $\mu $ is a smooth path and its associated smooth curve is timelike and future-oriented, then an endpoint $p$ is a past endpoint if it is the image under $\mu $ of the lesser of the two boundary components of $\partial \Sigma $. It is a future endpoint if it is the image under $\mu $ of the greater of the two boundary components of $\partial \Sigma $.

Definition 36 Trip

✓

A trip is a curve which is piecewise a future-oriented, timelike geodesic. A trip from $p$ to $q$ is a trip with past endpoint $p$ and future endpoint $q$. We write $p \ll q$ if and only if there exists a trip from $p$ to $q$.

Definition 37 Causal Trip

✓

A causal trip is a curve which is piecewise a future-oriented, causal geodesic. (Note a causal geodesic is possibly degenerate.) A causal trip from $p$ to $q$ is a causal trip with past endpoint $p$ and future endpoint $q$. We write $p \prec q$ if and only if there exists a causal trip from $p$ to $q$.

Definition 38 Chronological Future and Chronological Past

✓

For a spacetime $M$ and $p$ in $M$ the set $I^+(p) = \{ q \in M : p \ll q\} $ is called the chronological future of $p$. $I^-(p) = \{ q \in M : q \ll p\} $ is called the chronological past of $p$. The chronological future of a set $S \subset M$ is the union of the chronological future of each element of the set

\begin{align} I^+(S) = \bigcup \limits _{p \in S} I^+(p). \end{align}

The chronological past of $S$ is defined similarly

\begin{align} I^-(S) = \bigcup \limits _{p \in S} I^-(p). \end{align}

Definition 39 Causal Future and Causal Past

✓

For a spacetime $M$ and $p$ in $M$ the set $J^+(p) = \{ q \in M : p \prec q\} $ is called the causal future of $p$. $J^-(p) = \{ q \in M : q \prec p\} $ is called the causal past of $p$. The causal future of a set $S \subset M$ is the union of the causal future of each element of the set

\begin{align} J^+(S) = \bigcup \limits _{p \in S} J^+(p). \end{align}

The causal past of $S$ is defined similarly

\begin{align} J^-(S) = \bigcup \limits _{p \in S} J^-(p). \end{align}

Lemma 40 Chronological Precedence Implies Causal Precedence

✓

Every trip is a causal trip, so $p \ll q$ implies $p \prec q$. Consequently $I^+(p) \subseteq J^+(p)$ and $I^-(p) \subseteq J^-(p)$.

Proof ▶

A timelike tangent vector is in particular causal (timelike or null), so a future-oriented timelike geodesic is a future-oriented causal geodesic. Hence any trip witnessing $p \ll q$ is also a causal trip witnessing $p \prec q$. The set inclusions follow by unfolding the definitions of the futures and pasts.

Lemma 41 Monotonicity of Futures and Pasts

✓

The set-valued chronological and causal futures and pasts are monotone: if $S \subseteq T$ then $I^\pm (S) \subseteq I^\pm (T)$ and $J^\pm (S) \subseteq J^\pm (T)$.

Proof ▶

Each operator is an indexed union over the points of its argument set, and a union over a larger index set contains the union over a smaller one.

Definition 43 Completely Spacelike

✓

Consider two sets $\mathbf{O}_1$ and $\mathbf{O}_2$ in a spacetime. $\mathbf{O}_1$ and $\mathbf{O}_2$ are completely spacelike with respect to each other if every $p_1$ in $\mathbf{O}_1$ is spacelike related to every $p_2$ in $\mathbf{O}_2$.

Lemma 44 Symmetry of Spacelike Separation

✓

Spacelike relatedness is symmetric, and consequently complete spacelike separation is symmetric in its two regions: $\mathbf{O}_1, \mathbf{O}_2$ are completely spacelike if and only if $\mathbf{O}_2, \mathbf{O}_1$ are.

Proof ▶

The relation $p_2 \notin J^+(p_1) \cup J^-(p_1)$ is symmetric in $p_1, p_2$ since $J^+(p_1)$ and $J^-(p_1)$ swap roles with $J^-(p_2)$ and $J^+(p_2)$ under the exchange. Symmetry of complete spacelike separation follows by applying this pointwise.

Lemma 45 Structural Properties of Complete Spacelike Separation

✓

Complete spacelike separation is monotone under shrinking either region; the empty region is completely spacelike to any region; and a union of regions is completely spacelike to $\mathbf{O}$ if and only if each part is. The same properties hold for the bundled Lorentzian spacetime.

Proof ▶

Each follows directly from the pointwise definition: monotonicity by restricting the universally-quantified points, the empty cases vacuously, and the union cases by splitting the membership disjunction.

Definition 46 Alexandrov Topology

✓

Alexandrov topology on a spacetime $M$ is the topology generated by the basis consisting of all sets of the form $I^+(p) \cap I^-(q)$ for points $p$ and $q$ in $M$.

Lemma 47 Basis Sets Are Alexandrov-Open

✓

Every basis set $I^+(p) \cap I^-(q)$ is open in the Alexandrov topology.

Proof ▶

By construction the Alexandrov topology is generated by these basis sets, and any generating set is open in the generated topology.

Definition 48 Minkowski Spacetime

✓

Minkowski spacetime is standard Minkowski spacetime equipped with Alexandrov topology.

Definition 49 Lorentzian Spacetime

✓

Lorentzian spacetime is a spacetime equipped with a Hausdorff Alexandrov topology.

Lemma 50 Bundled Spacelike Separation and Basis Openness

✓

On a Lorentzian spacetime, complete spacelike separation of two regions is symmetric, and every basis set $I^+(p) \cap I^-(q)$ is open in the Alexandrov topology.

Proof ▶

These are restatements of the symmetry of complete spacelike separation and the openness of basis sets for the underlying spacetime, transported through the bundling of a Lorentzian spacetime over its underlying spacetime and time orientation.

10.2.1 Isometries and basis-set preservation

Lemma 51 Isometries Preserve the Causal Classification

✓

An isometry $\varphi $ of a spacetime preserves the metric square of a tangent vector, $g_{\varphi (x)}(d\varphi _x v, d\varphi _x v) = g_x(v,v)$, and therefore $d\varphi _x v$ is timelike, null, or spacelike if and only if $v$ is.

Proof ▶

Specialising the metric-preservation property of an isometry to $w = v$ gives the square identity; the three classification equivalences then follow from the sign of $g(v,v)$ being unchanged.

Lemma 52 Unique Differentials Along a Path

✓

The parameter space of a path has unique differentials: being a closed, connected subset of $\mathbb {R}$ with more than one point, it is a non-degenerate interval, hence convex with non-empty interior.

Proof ▶

A connected subset of $\mathbb {R}$ is convex, and a closed convex set with at least two points contains a non-degenerate open interval, so has non-empty interior; convex sets with non-empty interior have unique differentials.

Lemma 53 Pushforward of a Path Under an Isometry

✓

An isometry $\varphi $ pushes a smooth path $\mu $ forward to the smooth path $\varphi \circ \mu $ on the same parameter space, with tangent vector $d\varphi (\dot\mu )$. The pushforward preserves the timelike and causal conditions and carries the past and future endpoints of $\mu $ to those of $\varphi \circ \mu $.

Proof ▶

Smoothness and non-vanishing of the derivative of $\varphi \circ \mu $ follow from the chain rule (using unique differentials on the parameter space) together with the fact that an isometry’s differential is a linear isomorphism. The tangent identity then transports the classification and endpoint conditions.

Lemma 54 Isometries Preserve Chronology

✓

Say an isometry $\varphi $ preserves the future orientation if its differential sends future-pointing vectors to future-pointing vectors; this property holds for the identity and is closed under composition. Under it, $\varphi $ carries trips to trips, so $p \ll q$ implies $\varphi (p) \ll \varphi (q)$, and the chronological futures and pasts satisfy $\varphi (I^\pm (p)) = I^\pm (\varphi (p))$.

Proof ▶

Future-orientation preservation makes the pushforward of a future-oriented trip a future-oriented trip, giving $p \ll q \Rightarrow \varphi (p) \ll \varphi (q)$. Applying this to $\varphi $ and to $\varphi ^{-1}$ yields the image equalities for $I^+$ and $I^-$.

Lemma 55 Isometries Preserve Basis Sets

✓

The future-orientation-preserving isometries (those $\varphi $ with both $\varphi $ and $\varphi ^{-1}$ preserving the orientation) form a subgroup, and intersecting it with the identity component gives the oriented identity component. Every such isometry maps Alexandrov-basis diamonds to diamonds, $\varphi (I^+(p) \cap I^-(q)) = I^+(\varphi (p)) \cap I^-(\varphi (q))$, both as an image and in pointwise-action form $\varphi \cdot \mathbf{B}$, and this lifts to the bundled Lorentzian spacetime.

Proof ▶

Bundling the inverse into the predicate makes the subgroup axioms follow from the identity and composition cases with no appeal to the group topology. Basis-set preservation is then the image of an intersection of a chronological future and past, computed via the previous lemma using injectivity of the isometry.

Lemma 56 Axiom 5 Basis-Set Preservation

✓

Instantiating the abstract curved-spacetime interface with the oriented identity component, every isometry $\varphi $ of the abstract spacetime carries Alexandrov-basis sets to basis sets, $\varphi \cdot \mathbf{B}$ is again a basis set. This is exactly the well-definedness condition for the Axiom 5 action $\mathfrak {U}(\mathbf{B}) \to \mathfrak {U}(\varphi (\mathbf{B}))$.

Proof ▶

The abstract isometry group of the bridge is, by definition, the oriented identity component, so basis-set preservation transfers verbatim from the concrete statement.

10.3 Haag Kastler Axioms

With that out of the way we can state the axioms. Each axiom below is presented as a definition so that it is captured as a node in the blueprint declaration graph. In the Lean formalization each axiom corresponds to a Prop-valued predicate (or, in the case of Local Algebras, a data field), and the bundling structure HaagKastlerNet packages them together (see 64). Downstream theorems take an instance of HaagKastlerNet as a hypothesis and invoke each axiom as a projection.

Definition 57 Axiom 1: Local Algebras

✓

For any basis element $\mathbf{B}$ of the Alexandrov topology on Minkowski spacetime, i.e. any set of the form $I^+(p) \cap I^-(q)$, there is a corresponding abstract C*-algebra $\mathfrak {U}(\mathbf{B})$

\begin{align} \mathbf{B} \longmapsto \mathfrak {U}(\mathbf{B}), \end{align}

and when $\mathbf{B}$ is the empty set, we have the distinguished correspondence

\begin{align} \emptyset \longmapsto \mathbb {C} \mathbf{1}, \end{align}

where $\mathbf{1}$ is the multiplicative identity in the abstract C*-algebra $\mathbb {C} \mathbf{1}$.

Definition 58 Axiom 2: Isotony

✓

Let $\mathbf{B}_1$ and $\mathbf{B}_2$ be any two basis elements of the Alexandrov topology on Minkowski spacetime, i.e. any two sets of the form $I^+(p_1) \cap I^-(q_1)$ and $I^+(p_2) \cap I^-(q_2)$.

If $\mathbf{B}_1 \subset \mathbf{B}_2$ then $\mathfrak {U}(\mathbf{B}_1) \subset \mathfrak {U}(\mathbf{B}_2)$, where inclusion is implemented by

\begin{align} i : \mathfrak {U}(\mathbf{B}_1) \hookrightarrow \mathfrak {U}(\mathbf{B}_2), \end{align}

a unital *-monomorphism.

Before introducing the next axiom, we must introduce the definition:

Definition 59 Quasilocal Algebra

✓

Consider the set-theoretic union of all $\mathfrak {U}(\mathbf{B})$. 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 $\mathfrak {U}$. This C*-algebra $\mathfrak {U}$ is called the quasilocal algebra.

Definition 60 Axiom 3: Local Commutativity

✓

If $\mathbf{B_1}$ and $\mathbf{B_2}$ are completely spacelike, then $\mathfrak {U}(\mathbf{B_1})$ and $\mathfrak {U}(\mathbf{B_2})$ commute in the quasilocal algebra $\mathfrak {U}$, i.e. for any $a_1$ in $\mathfrak {U}(\mathbf{B_1})$ and $a_2$ in $\mathfrak {U}(\mathbf{B_2})$ it follows that

\begin{align} i(a_1) i(a_2) - i(a_2) i(a_1) = 0 \end{align}

in the quasilocal algebra $\mathfrak {U}$.

The next axiom makes use of the following new definition:

Definition 61 Quasilocal Observable

✓

The image $\pi _\omega (a)$ of a self-adjoint member $a$ of the quasilocal algebra $\mathfrak {U}$ under a GNS *-homomorphism $\pi _\omega $ is self-adjoint and thus corresponds to an “observable”. Any “observable” corresponding to such a self-adjoint $\pi _\omega (a)$ is called a quasilocal observable.

Definition 62 Axiom 4: Quasilocal Completeness

✓

All “observables” are quasilocal observables.

Definition 63 Axiom 5: Lorentz Covariance

✓

Let $\mathbf{B}$ be any basis element of the Alexandrov topology on Minkowski spacetime, i.e. any set of the form $I^+(p) \cap I^-(q)$.

A member $L$ of the inhomogeneous Lorentz group connected to the identity acts on $\mathfrak {U}(\mathbf{B})$ as follows

\begin{align} \alpha _L : \mathfrak {U}(\mathbf{B}) & \longrightarrow \mathfrak {U}(L\mathbf{B}) \\ a & \longmapsto \alpha _L(a) \end{align}

where $L\mathbf{B}$ is the image of the region $\mathbf{B}$ under the transformation $L$ and $\alpha _L$ is a unital *-isomorphism generated by $L$. The map $\alpha _L$ is such that (1) for the identity element $\mathbf{1}$ of the Lorentz group it satisfies

\begin{align} \alpha _{\mathbf{1}}(a) = a, \end{align}

(2) for all appropriate $a$, $L$, and $L'$ it satisfies

\begin{align} \alpha _{L' \cdot L}(a) = \alpha _{L'}(\alpha _{L}(a)), \end{align}

and (3) for basis elements $\mathbf{B}_\iota \subset \mathbf{B}_\kappa $ and the unital *-monomorphism $i$ of Axiom 2 (Isotony) $\alpha _L$ commutes with $i$. In other words the following diagram

$\begin{tikzcd} \mathfrak{U}(\mathbf{B}_\kappa) \arrow[r, "\alpha_L"] & \mathfrak{U}(L\mathbf{B}_\kappa) \\ \mathfrak{U}(\mathbf{B}_\iota) \arrow[r, "\alpha_L"] \arrow[u, "i"] & \mathfrak{U}(L\mathbf{B}_\iota) \arrow[u, "i"] \end{tikzcd}$

commutes.

Definition 64 Haag-Kastler Net

✓

A Haag-Kastler net on Minkowski spacetime is the bundling of the data of 57 together with the properties of 58, 60, 62, and 63. In the Lean formalization this is a single structure whose fields are the assignment $\mathbf{B} \mapsto \mathfrak {U}(\mathbf{B})$ and proofs that this assignment satisfies the four remaining axioms. Theorems about AQFT take an instance of this structure as a hypothesis and invoke each axiom as a projection.

This concludes the presentation of the “sharpened” axioms. As proven in this blog post, these “sharpened” axioms entail the original axioms save Axiom 6 (Primitivity), which is an axiom that we abandon.

These “sharpened” axioms also allow for a straightforward generalization to a set of axioms describing AQFT in curved spacetime, i.e. a set of axioms describing AQFT in a curved spacetime background that is fixed and treated classically. In a subsequent blog post we will detail these axioms.

10.3.1 Covariant States and the Covariance Action

The Lorentz covariance of a Haag-Kastler net (63) acts on the net fiberwise, through the $*$-isomorphisms $\alpha _L : \mathfrak {U}(\mathbf{B}) \to \mathfrak {U}(L\cdot \mathbf{B})$. We record two consequences: the notion of a Lorentz-covariant family of local states, and the lift of the fiberwise action to a single dynamical $*$-automorphism of the quasilocal algebra.

Definition 65 Covariant Family of Local States

✓

Given a Haag-Kastler net (64), a covariant family of local states assigns to every region $\mathbf{B}$ a state $\omega _{\mathbf{B}}$ on the local algebra $\mathfrak {U}(\mathbf{B})$ such that, for every Lorentz transformation $L$ and every $a \in \mathfrak {U}(\mathbf{B})$, one has $\omega _{\mathbf{B}}(a) = \omega _{L\cdot \mathbf{B}}(\alpha _L a)$, where $\alpha _L$ is the covariance isomorphism of 63. The local states are thus intertwined by the Lorentz action.

Lemma 66 Composition of Covariance

✓

For a covariant family of local states, the covariance relation composes along the group: $\omega _{\mathbf{B}}(a) = \omega _{L'\cdot (L\cdot \mathbf{B})}\big(\alpha _{L'}(\alpha _L a)\big)$, reflecting the multiplicativity of the Lorentz action.

Definition 67 Quasilocal Covariance Automorphism

✓

A lift of the fiberwise Lorentz action of $L$ to a quasilocal algebra $\mathfrak {U}$ (59) is a $*$-automorphism $\beta _L$ of $\mathfrak {U}$ intertwining the local embeddings $\iota _{\mathbf{B}}$ with the covariance isomorphisms: $\beta _L(\iota _{\mathbf{B}} a) = \iota _{L\cdot \mathbf{B}}(\alpha _L a)$ for every Alexandrov-basis set $\mathbf{B}$.

Lemma 68 Uniqueness of the Quasilocal Lift

✓

Any two lifts of the same $L$ have the same underlying automorphism: they agree on the union of the local images, which is dense in $\mathfrak {U}$, and $*$-automorphisms of a C*-algebra are continuous.

Theorem 69 Existence of the Quasilocal Lift

✓

For a covariance-compatible quasilocal algebra, the fiberwise Lorentz action extends to a $*$-automorphism of $\mathfrak {U}$, so the lift of 67 exists. The intertwiner is defined on the directed union of local images (a dense $*$-subalgebra) and extended by uniform continuity; the inverse is supplied by $L^{-1}$, and the group laws $\beta _{L'L} = \beta _{L'}\circ \beta _L$ and $\beta _{1} = \mathrm{id}$ furnish the two-sided inverse.

Theorem 70 Existence for the Trivial Net

✓

The covariance-compatibility hypothesis is satisfiable: the trivial net’s quasilocal algebra is covariance-compatible (every $*$-automorphism of $\mathbb {C}$ is the identity), so the quasilocal lift exists unconditionally for the trivial net.

Definition 71 Covariant Quasilocal Algebra

✓

A covariant quasilocal algebra bundles a Haag-Kastler net (64), a quasilocal algebra of that net (59), and a proof that the embeddings are covariance-compatible for every Lorentz transformation. On such data the quasilocal lift (67) exists for every $L$ by 69, yielding the covariance action $L \mapsto \beta _L$ on the quasilocal algebra; the trivial net provides an instance. This is the natural home for the covariance dynamics: the compatibility hypothesis of 69 becomes structural data rather than a side condition.

Lemma 72 Group-Action Coherence of the Covariance Automorphism

✓

The covariance action $L \mapsto \beta _L$ of a covariant quasilocal algebra is a genuine action of the Lorentz group by $*$-automorphisms of the quasilocal algebra: $\beta _{\mathbf{1}} = \mathrm{id}$ and $\beta _{L'L} = \beta _{L'} \circ \beta _L$.

Definition 73 Invariant State

✓

A state $\omega $ on the quasilocal algebra of a covariant quasilocal algebra (71) is (Poincaré-)invariant if it is a fixed point of the dual covariance action: $\omega (\beta _L a) = \omega (a)$ for every Lorentz transformation $L$ and observable $a$. This is the invariance condition of a vacuum state; further conditions (e.g. the spectrum condition) are imposed separately.

Theorem 74 GNS Unitary Implementation of an Invariant State

✓

For an invariant state $\omega $, the covariance action is implemented on the GNS Hilbert space by a family of unitaries $U(L)$ satisfying $U(L)\, \pi (a)\Omega = \pi (\beta _L a)\, \Omega $ and $U(L)\Omega = \Omega $. The unitaries are obtained by extending the densely-defined isometry $\pi (a)\Omega \mapsto \pi (\beta _L a)\Omega $ - isometric because $\omega $ preserves the GNS inner product $\langle \pi (a)\Omega , \pi (b)\Omega \rangle = \omega (a^* b)$ - to the whole GNS space.

10.4 Haag Kastler Axioms in Curved Spacetime

Here we recount the axioms we’ve established for AQFT in Lorentzian spacetime.

The first axiom states:

Definition 75 Axiom 1: Local Algebras

✓

For any basis element $\mathbf{B}$ of the Alexandrov topology on a Lorentzian spacetime, i.e. any set of the form $I^+(p) \cap I^-(q)$, there is a corresponding abstract C*-algebra $\mathfrak {U}(\mathbf{B})$

\begin{align} \mathbf{B} \longmapsto \mathfrak {U}(\mathbf{B}), \end{align}

and when $\mathbf{B}$ is the empty set, we have the distinguished correspondence

\begin{align} \emptyset \longmapsto \mathbb {C} \mathbf{1}, \end{align}

where $\mathbf{1}$ is the multiplicative identity in the abstract C*-algebra $\mathbb {C} \mathbf{1}$.

The second axiom can be immediately stated too.

Definition 76 Axiom 2: Isotony

✓

Let $\mathbf{B}_1$ and $\mathbf{B}_2$ be any two basis elements of the Alexandrov topology on a Lorentzian spacetime, i.e. any two sets of the form $I^+(p_1) \cap I^-(q_1)$ and $I^+(p_2) \cap I^-(q_2)$.

If $\mathbf{B}_1 \subset \mathbf{B}_2$ then $\mathfrak {U}(\mathbf{B}_1) \subset \mathfrak {U}(\mathbf{B}_2)$, where inclusion is implemented by

\begin{align} i : \mathfrak {U}(\mathbf{B}_1) \hookrightarrow \mathfrak {U}(\mathbf{B}_2), \end{align}

a unital *-monomorphism.

The next axiom can be stated as follows:

Definition 77 Axiom 3: Local Commutativity

✓

If $\mathbf{B_1}$ and $\mathbf{B_2}$ are completely spacelike, for any Alexandrov topology basis element $\mathbf{B}$ such that $\mathbf{B_1}, \mathbf{B_2} \subseteq \mathbf{B}$ the algebras $\mathfrak {U}(\mathbf{B_1})$ and $\mathfrak {U}(\mathbf{B_2})$ commute in the C*-algebra $\mathfrak {U}(\mathbf{B})$, i.e. for any $a_1$ in $\mathfrak {U}(\mathbf{B_1})$ and $a_2$ in $\mathfrak {U}(\mathbf{B_2})$ we have

\begin{align} i(a_1) i(a_2) - i(a_2) i(a_1) = 0 \end{align}

in the C*-algebra $\mathfrak {U}(\mathbf{B})$, where $i$ is the unital *-monomorphism Axiom 2 (Isotony).

If no such $\mathbf{B}$ exists, then it simply doesn’t make sense to consider if $\mathfrak {U}(\mathbf{B_1})$ and $\mathfrak {U}(\mathbf{B_2})$ commute as they are not in the same algebra.

The next axiom has need of the following definition

Definition 78 Local Observable

✓

For Lorentzian spacetime $M$ the image $\pi _\omega (a)$ of a self-adjoint member $a$ of the local algebra $\mathfrak {U}(\mathbf{B})$ under the GNS *-homomorphism $\pi _\omega $ of a state $\omega $ on $\mathfrak {U}(\mathbf{B})$ is self-adjoint and thus corresponds to an “observable”. Any “observable” corresponding to such a self-adjoint $\pi _\omega (a)$ is called a local observable.

and can be stated as follows:

Definition 79 Axiom 4: Local Completeness

✓

All “observables” are local observables.

The final axiom states:

Definition 80 Axiom 5: Isometric Covariance

✓

Let $\mathbf{B}$ be any basis element of the Alexandrov topology on a Lorentzian spacetime $M$, i.e. any set of the form $I^+(p) \cap I^-(q)$.

A member $\varphi $ of the group of isometries of $M$ connected to the identity acts on $\mathfrak {U}(\mathbf{B})$ as follows

\begin{align} \alpha _\varphi : \mathfrak {U}(\mathbf{B}) & \longrightarrow \mathfrak {U}(\varphi (\mathbf{B})) \\ a & \longmapsto \alpha _\varphi (a) \end{align}

where $\varphi (\mathbf{B})$ is the image of the basis element $\mathbf{B}$ under the isometry $\varphi $ and $\alpha _\varphi $ is a unital *-isomorphism generated by $\varphi $. The map $\alpha _\varphi $ is such that (1) for the identity isometry $\mathbf{1}$ it satisfies

\begin{align} \alpha _{\mathbf{1}}(a) = a, \end{align}

(2) for all appropriate $a$, $\varphi $, and $\varphi '$ it satisfies

\begin{align} \alpha _{\varphi ' \circ \varphi }(a) = \alpha _{\varphi '}(\alpha _{\varphi }(a)), \end{align}

and (3) for Alexandrov topology basis elements $\mathbf{B}_\iota \subset \mathbf{B}_\kappa $ and the unital *-monomorphism $i$ of Axiom 2 (Isotony) $\alpha _\varphi $ commutes with $i$. In other words the following diagram

$\begin{tikzcd} \mathfrak{U}(\mathbf{B}_\kappa) \arrow[r, "\alpha_\varphi"] & \mathfrak{U}(\varphi(\mathbf{B}_\kappa)) \\ \mathfrak{U}(\mathbf{B}_\iota) \arrow[r, "\alpha_\varphi"] \arrow[u, "i"] & \mathfrak{U}(\varphi(\mathbf{B}_\iota)) \arrow[u, "i"] \end{tikzcd}$

commutes.

Definition 81 Haag-Kastler Net in Curved Spacetime

✓

A Haag-Kastler net in curved spacetime on a Lorentzian spacetime is the bundling of the data of 75 together with the properties of 76, 77, 79, and 80. In the Lean formalization this is a single structure whose fields are the assignment $\mathbf{B} \mapsto \mathfrak {U}(\mathbf{B})$ and proofs that this assignment satisfies the four remaining axioms. Theorems about AQFT in curved spacetime take an instance of this structure as a hypothesis and invoke each axiom as a projection.

Generally these axioms follow in a straightforward manner from those of AQFT in Minkowski spacetime. The only “surprise” in this presentation is the absence of a quasilocal algebra. However, as we found, its absence is simply a reflection of the observational constraints of Lorentzian spacetime which don’t exist in Minkowski spacetime.

10.4.1 Covariant States in Curved Spacetime

As in the Minkowski case, the isometric covariance (80) acts fiberwise through the $*$-isomorphisms $\alpha _\varphi : \mathfrak {U}(\mathbf{B}) \to \mathfrak {U}(\varphi (\mathbf{B}))$. Since there is no quasilocal algebra, only the local notion of a covariant family of states is available.

Definition 82 Covariant Family of Local States in Curved Spacetime

✓

Given a Haag-Kastler net on a Lorentzian spacetime (81), a covariant family of local states assigns to every region $\mathbf{B}$ a state $\omega _{\mathbf{B}}$ on $\mathfrak {U}(\mathbf{B})$ such that, for every identity-component isometry $\varphi $ and every $a \in \mathfrak {U}(\mathbf{B})$, $\omega _{\mathbf{B}}(a) = \omega _{\varphi (\mathbf{B})}(\alpha _\varphi a)$, where $\alpha _\varphi $ is the covariance isomorphism of 80.

Lemma 83 Composition of Covariance in Curved Spacetime

✓

For a covariant family of local states, the covariance relation composes along the isometry group: $\omega _{\mathbf{B}}(a) = \omega _{\varphi '(\varphi (\mathbf{B}))}\big(\alpha _{\varphi '}(\alpha _\varphi a)\big)$.