PhyslibAlpha.ProbabilisticTheory.LocalNet.GlobalRealization

For a local net $\mathcal{N}$ of observables indexed by a set of regions $R$, where $A(i)$ denotes the space of observables localized in region $i \in R$, given two regions such that $i \le j$, this definition provides the inclusion map $\iota_{ij}: A(i) \to A(j)$ as an $\mathbb{R}$-linear map.

Let $\mathcal{N}$ be a local net of observables indexed by a set of regions $R$. For each region $i \in R$, let $A(i)$ denote the space of observables localized in $i$, and for any regions $i \le j$, let $\iota_{ij} : A(i) \to A(j)$ be the linear inclusion map. Then the family of spaces $A(i)$ together with the maps $\iota_{ij}$ forms a directed system.

Given a faithful local net $\mathcal{N}$ over a directed set of regions $R$, where each region $i \in R$ is associated with a space of local observables $A(i)$, the **global system** is defined as the algebraic direct limit of these local systems, denoted by $\varinjlim A(i)$. This limit is taken with respect to the family of linear inclusion maps $\iota_{ij}: A(i) \to A(j)$ for all $i \le j$ in $R$. This construction represents the observables of the entire infinite system by identifying local observables that are images of one another under inclusion into larger regions.

The global system of local observables, constructed as the algebraic direct limit $\varinjlim A(i)$ of the local observable spaces $A(i)$ in a local net $\mathcal{N}$, carries the structure of an additive commutative group. This means that for any observables in the global system, addition is well-defined, commutative, and associative, with a zero element and additive inverses.

The global system of local observables, defined as the algebraic direct limit $\varinjlim A(i)$ of the local spaces $A(i)$ for a faithful local net $\mathcal{N}$, carries the structure of a module over the real numbers $\mathbb{R}$. This means that scalar multiplication of an observable by a real number is well-defined and satisfies the standard axioms of a real vector space.

Given a faithful local net $\mathcal{N}$ over a directed set of regions $R$, let $A(i)$ be the $\mathbb{R}$-vector space of observables localized in a region $i \in R$. The map $\text{ofLoc}_i: A(i) \to \varinjlim A(j)$ is the canonical $\mathbb{R}$-linear map that embeds the local observables from region $i$ into the global system, defined as the algebraic direct limit of the local systems.

Let $\mathcal{N}$ be a faithful local net over a directed set of regions $R$, where $A(i)$ denotes the space of local observables for each region $i \in R$. Let $\iota_{ij} : A(i) \to A(j)$ be the inclusion map for $i \le j$, and let $\text{ofLoc}_i : A(i) \to \text{GlobalSystem}$ be the canonical injection into the global system (the algebraic direct limit of the local spaces). For any regions $i, j \in R$ with $i \le j$ and any local observable $a \in A(i)$, the following identity holds: $$\text{ofLoc}_j(\iota_{ij}(a)) = \text{ofLoc}_i(a)$$

Given a faithful local net $\mathcal{N}$ over a nonempty directed set of regions $R$, where each region $i \in R$ is associated with a space of local observables $A(i)$, let the global system be the algebraic direct limit $\varinjlim A(j)$. For any global observable $x$ in this global system, there exists a region $i \in R$ and a local observable $a \in A(i)$ such that $x$ is the image of $a$ under the canonical injection $\text{ofLoc}_i : A(i) \to \varinjlim A(j)$.

For any two observables $x$ and $y$ in the global system $\varinjlim A(i)$ constructed from a faithful local net over a non-empty directed set of regions $R$, there exists a common region $i \in R$ and local observables $a, b \in A(i)$ such that $x$ and $y$ are the images of $a$ and $b$ under the canonical injection $\text{ofLoc}_i: A(i) \to \varinjlim A(j)$.

Let $\mathcal{N}$ be a faithful local net over a directed set of regions $R$, where $A(i)$ is the space of local observables associated with region $i \in R$. Let the global system be the algebraic direct limit $\varinjlim A(j)$ of these local spaces. For any region $i \in R$, the canonical linear map $\text{ofLoc}_i : A(i) \to \varinjlim A(j)$, which identifies local observables with their representatives in the global system, is injective.

In a faithful local net $\mathcal{N}$ over a directed set of regions $R$, let $A(i)$ be the space of local observables for each region $i \in R$. Let $\text{ofLoc}_i : A(i) \to \text{GlobalSystem}$ be the canonical linear map that embeds local observables into the global system (the algebraic direct limit $\varinjlim A(i)$). For any local observables $a \in A(i)$ and $b \in A(j)$, their images in the global system are equal, $\text{ofLoc}_i(a) = \text{ofLoc}_j(b)$, if and only if there exists a common larger region $k \in R$ (with $i \le k$ and $j \le k$) such that their inclusions into $A(k)$ are identical: $$\iota_{ik}(a) = \iota_{jk}(b)$$ where $\iota_{ik} : A(i) \to A(k)$ and $\iota_{jk} : A(j) \to A(k)$ are the inclusion maps defined by the local net.

Given a faithful local net $\mathcal{N}$ over a directed set of regions $R$, where each region $i \in R$ is associated with a space of local observables $A(i)$, the set of **non-negative global observables** in the global system $\varinjlim A(i)$ is defined as the set of all elements $x$ that are images of non-negative local observables. Specifically, an element $x \in \varinjlim A(i)$ belongs to this set if there exists a region $i \in R$ and a local observable $a \in A(i)$ such that $a \ge 0$ and $\text{ofLoc}_i(a) = x$, where $\text{ofLoc}_i: A(i) \to \varinjlim A(j)$ is the canonical injection into the direct limit.

Given a faithful local net $\mathcal{N}$ over a directed set of regions $R$, for any region $i \in R$ and any local observable $a \in A(i)$, if $a$ is non-negative ($0 \le a$), then its image under the canonical injection into the global system, $\text{ofLoc}_i(a)$, belongs to the set of non-negative global observables $\text{Pos}$.

In the global system of local observables $\varinjlim A(i)$ associated with a faithful local net $\mathcal{N}$, the zero observable $0$ is non-negative, i.e., $0 \in \text{Pos}$.

Let $\varinjlim A(i)$ be the global system of local observables associated with a faithful local net $\mathcal{N}$ over a directed set of regions $R$. Let $\text{Pos}$ be the set of non-negative global observables, defined as the set of elements $x \in \varinjlim A(i)$ such that $x$ is the image of some non-negative local observable $a \in A(i)$ under the canonical injection. For any two global observables $x$ and $y$, if $x \in \text{Pos}$ and $y \in \text{Pos}$, then their sum $x + y$ is also in $\text{Pos}$.

In the global system of local observables $\varinjlim A(i)$ (the algebraic direct limit of local systems in a faithful local net $\mathcal{N}$), let $\text{Pos}$ denote the set of non-negative global observables. For any non-negative real number $c \ge 0$ and any global observable $x \in \text{Pos}$, the scalar multiple $c \cdot x$ is also an element of $\text{Pos}$.

The global system of local observables $\varinjlim A(i)$ is equipped with a partial order relation $\le$. For any two global observables $x, y \in \varinjlim A(i)$, the relation $x \le y$ holds if and only if $y - x \in \text{Pos}$, where $\text{Pos}$ is the cone of non-negative global observables consisting of elements that are images of non-negative local observables $a \in A(i)$ for some region $i$.

In the global system of local observables $\varinjlim A(i)$ associated with a faithful local net $\mathcal{N}$, the partial order relation $\le$ between two observables $x$ and $y$ is characterized such that $x \le y$ if and only if their difference $y - x$ is a non-negative global observable, i.e., $y - x \in \text{Pos}$.

In the global system of local observables $\varinjlim A(i)$, an element $x$ is non-negative (denoted $0 \le x$) if and only if $x \in \text{Pos}$, where $\text{Pos}$ is the set of global observables that are images of non-negative local observables from the underlying local net.

The global system of local observables $\varinjlim A(i)$ is an ordered additive monoid. This means that the addition operation is compatible with the partial order relation $\le$: for any global observables $x, y, z \in \varinjlim A(i)$, if $x \le y$, then $x + z \le y + z$.

In the global system of local observables $\varinjlim A(i)$ associated with a faithful local net $\mathcal{N}$, scalar multiplication by non-negative real numbers is monotonic. That is, for any real number $r \in \mathbb{R}$ such that $r \ge 0$ and any global observables $x, y \in \varinjlim A(i)$, if $x \le y$, then $r \cdot x \le r \cdot y$.

The global system of local observables $\varinjlim A(i)$, constructed as the algebraic direct limit of the local spaces $A(i)$ for a faithful local net $\mathcal{N}$, is an ordered vector space over the real numbers $\mathbb{R}$. This means that the space is a real vector space equipped with a partial order $\le$ such that for any elements $x, y, z \in \varinjlim A(i)$ and any scalar $r \in \mathbb{R}$ with $r \ge 0$, the relation $x \le y$ implies $x + z \le y + z$ and $rx \le ry$.

The global system of local observables, defined as the algebraic direct limit $\varinjlim A(i)$, is a unital space. Its unit element $1$ is defined as the image of the identity element $1 \in A(i)$ from any local region $i \in R$ under the canonical injection $\iota_i: A(i) \to \varinjlim A(j)$. Because the inclusion maps in the local net preserve the unit, this definition is consistent across all regions.

For any region $i$ in the set of regions $R$, let $A(i)$ be the space of local observables and $\varinjlim A(j)$ be the global system of observables. The canonical injection map $\text{ofLoc}_i: A(i) \to \varinjlim A(j)$ maps the identity element $1 \in A(i)$ to the identity element $1$ of the global system: $$\text{ofLoc}_i(1) = 1$$

The global system of local observables $\varinjlim A(i)$ is an order unit space. This means that the global system is an ordered vector space where the identity element $1$ satisfies two conditions: 1. The identity element is non-negative: $1 \ge 0$. 2. The identity element is an order unit: for every element $x$ in the global system $\varinjlim A(i)$, there exists a natural number $n \in \mathbb{N}$ such that $x \le n \cdot 1$. These properties are inherited from the local order unit spaces $A(i)$ via the direct limit construction, as every global observable $x$ is the image of some local observable $a \in A(i)$ which itself satisfies the order unit property.

Given a faithful local net $\mathcal{N}$ over a directed set of regions $R$, let $A(i)$ be the space of local observables for a region $i \in R$ and $\varinjlim A(j)$ be the global system. The map $\text{ofChan}_i: A(i) \to \varinjlim A(j)$ is the canonical channel (a unital positive linear map) that embeds the local observables of region $i$ into the global system. This map is constructed from the canonical linear injection $\text{ofLoc}_i$ by providing proofs that it is both positive (preserving the order) and unital (mapping the identity of $A(i)$ to the identity of the global system).

Given a faithful local net $\mathcal{N}$ over a directed set of regions $R$, let $A(i)$ be the space of local observables for a region $i \in R$ and $\varinjlim A(j)$ be the global system. For any region $i \in R$ and any local observable $a \in A(i)$, the value of the canonical channel $\text{ofChan}_i : A(i) \to \varinjlim A(j)$ applied to $a$ is equal to the value of the canonical linear map $\text{ofLoc}_i : A(i) \to \varinjlim A(j)$ applied to $a$, that is, $\text{ofChan}_i(a) = \text{ofLoc}_i(a)$.

Consider a faithful local net $\mathcal{N}$ over a directed set of regions $R$, where each region $i \in R$ is associated with a space of local observables $A(i)$. Let $\varinjlim A(j)$ be the global system of local observables. For any region $i \in R$, the canonical channel $\text{ofChan}_i : A(i) \to \varinjlim A(j)$ is an order embedding. That is, for any local observables $a, b \in A(i)$, the relation $\text{ofChan}_i(a) \le \text{ofChan}_i(b)$ holds in the global system if and only if $a \le b$ holds in the local system $A(i)$.

Given a faithful local net $\mathcal{N}$ over a directed set of regions $R$, where each region $i \in R$ is associated with a space of local observables $A(i)$, let $\varinjlim A(j)$ be the global system. The **canonical representation** of the net in its global system is the net representation whose components $\pi_i: A(i) \to \varinjlim A(j)$ are the canonical inclusion channels. For any two regions $i \le j$ with a local inclusion $\iota_{ij}: A(i) \to A(j)$, this representation satisfies $\pi_i = \pi_j \circ \iota_{ij}$.

Let $\mathcal{N}$ be a faithful local net over a directed set of regions $R$, where each region $i \in R$ is associated with a space of local observables $A(i)$. The canonical representation of $\mathcal{N}$ in its global system $\varinjlim A(j)$ is faithful. This means that for every region $i \in R$, the canonical inclusion map $\pi_i : A(i) \to \varinjlim A(j)$ is an order embedding: for any local observables $a, b \in A(i)$, $a \le b$ if and only if $\pi_i(a) \le \pi_i(b)$ in the global system.

Given a state $\sigma$ of a local net $\mathcal{N}$ (defined as a compatible family of local linear functionals $\omega_i: A(i) \to \mathbb{R}$ for each region $i$), this definition provides the unique induced linear functional $L: \varinjlim A(i) \to \mathbb{R}$ on the global system of local observables. For any local observable $a \in A(i)$ viewed as an element of the global system, its value under this functional is given by the local expectation value $L(a) = \sigma.\omega_i(a)$.

Let $\mathcal{N}$ be a faithful local net of observable spaces $A(i)$ over a directed set of regions $R$. Let $\sigma$ be a state of the local net (a compatible family of local linear functionals $\omega_i: A(i) \to \mathbb{R}$), and let $L_\sigma: \varinjlim A(j) \to \mathbb{R}$ be the linear functional induced by $\sigma$ on the global system. For any region $i \in R$ and any local observable $a \in A(i)$, the value of $L_\sigma$ applied to the image of $a$ under the canonical injection $\iota_i: A(i) \to \varinjlim A(j)$ is equal to the local expectation value: $$L_\sigma(\iota_i(a)) = \omega_i(a).$$

Given a faithful local net $\mathcal{N}$ and a net state $\sigma$ (defined as a compatible family of local states $\{\omega_i: A(i) \to \mathbb{R}\}_{i \in R}$), this definition constructs the corresponding state on the global system $\varinjlim A(i)$. The resulting state is a unital positive linear map $L: \varinjlim A(i) \to \mathbb{R}$ such that for any local observable $a \in A(i)$ represented as an element of the global system, the expectation value is $L(a) = \omega_i(a)$. This construction uses the induced linear functional $L_\sigma$ and formally proves that it preserves non-negativity and maps the global identity element to $1$.

Let $\mathcal{N}$ be a faithful local net of observable spaces $A(i)$ over a directed set of regions $R$. Let $\sigma$ be a net state, which is a compatible family of local states $\{\omega_k\}_{k \in R}$, and let $L_\sigma: \varinjlim A(j) \to \mathbb{R}$ be the state on the global system induced by $\sigma$. For any region $i \in R$ and any local observable $a \in A(i)$, the value of the global state $L_\sigma$ applied to the image of $a$ under the canonical injection $\iota_i: A(i) \to \varinjlim A(j)$ is equal to the local expectation value $\omega_i(a)$: $$L_\sigma(\iota_i(a)) = \omega_i(a)$$

Let $\mathcal{N}$ be a faithful local net of observables over a directed set of regions $R$, where each region $i \in R$ is associated with a space of local observables $A(i)$. Let the global system be the algebraic direct limit $\varinjlim A(i)$. There is a natural bijection (equivalence) between: 1. **Global states**: The set of states $\mathcal{S}(\varinjlim A(i))$, defined as unital positive linear maps from the global system to $\mathbb{R}$. 2. **Net states**: The set of compatible families of local states $\{\omega_i\}_{i \in R}$, where each $\omega_i: A(i) \to \mathbb{R}$ is a local state and for any $i \le j$, the condition $\omega_j \circ \iota_{ij} = \omega_i$ holds. The bijection maps a global state $\omega$ to the family of local states defined by its restriction to each region, $\omega_i = \omega \circ \pi_i$, where $\pi_i: A(i) \to \varinjlim A(j)$ is the canonical inclusion. Conversely, any compatible family of local states uniquely extends to a state on the global system by the universal property of the direct limit.