PhyslibAlpha.ProbabilisticTheory.LocalNet.Net

Let $N$ be a local net of observables that assigns a space of observables $A(X)$ to each region $X$. For any region $X$ and any observable $a \in A(X)$, the inclusion map $\iota_{X,X}$ associated with the reflexivity of the region ordering ($X \leq X$) satisfies: $$\iota_{X,X}(a) = a$$ This indicates that regarding a measurement in region $X$ as a measurement in the same region $X$ leaves the observable unchanged.

Let $N$ be a local net of observables, and let $X, Y, Z$ be regions such that $X \leq Y$ and $Y \leq Z$. For any observable $a \in A(X)$ belonging to the region $X$, applying the inclusion map from $X$ to $Z$ to $a$ is equivalent to first applying the inclusion map from $X$ to $Y$ and then applying the inclusion map from $Y$ to $Z$. That is, $$\iota_{X,Z}(a) = \iota_{Y,Z}(\iota_{X,Y}(a))$$ where $\iota_{U,V}$ denotes the inclusion map `N.incl` from the observables of region $U$ to the observables of region $V$.

Let $N$ be a local net of observables. For any two proofs $h$ and $h'$ of the inclusion between regions $X \leq Y$, the induced inclusion maps from the observables of region $X$ to the observables of region $Y$ are identical. That is, $$N.\text{incl}(h) = N.\text{incl}(h')$$ where $N.\text{incl}$ is the map regarding a measurement in a subregion as a measurement in a larger region.

Let $N$ be a local net of observables and $W, X, Y, Z$ be regions such that $W \leq X$, $X \leq Y$, and $Y \leq Z$. Let $\iota_{U,V}$ denote the inclusion map from the observables of region $U$ to the observables of region $V$. Then the composition of the inclusion maps along the chain $W \to X \to Y \to Z$ is equal to the direct inclusion map from $W$ to $Z$: $$\iota_{Y,Z} \circ (\iota_{X,Y} \circ \iota_{W,X}) = \iota_{W,Z}$$

Let $N$ be a local net of observables. For any regions $X, Y$, and $Z$ such that $X \leq Y$ and $Y \leq Z$, the composition of the inclusion map from $X$ to $Y$ (denoted $\iota_{X,Y}$) and the inclusion map from $Y$ to $Z$ (denoted $\iota_{Y,Z}$) is equal to the inclusion map from $X$ to $Z$. That is, $\iota_{Y,Z} \circ \iota_{X,Y} = \iota_{X,Z}$.

Let $N$ be a local net that assigns to each region $X$ a space of observables $A(X)$. For any two regions $X$ and $Y$ such that $X \leq Y$, let $\iota_{X,Y} : A(X) \to A(Y)$ be the inclusion map (a unital positive linear map). Given an effect $e$ in the region $X$ (an element $e \in A(X)$ satisfying $0 \leq e \leq 1$), this definition represents the image $\iota_{X,Y}(e)$ as an effect in the region $Y$. Since the inclusion is a unital positive linear map, the resulting element satisfies $0 \leq \iota_{X,Y}(e) \leq 1$.

Let $N$ be a local net of observables that assigns to each region $X$ a space of observables $A(X)$. For regions $X$ and $Y$ such that $X \leq Y$, let $\iota_{X,Y} : A(X) \to A(Y)$ be the inclusion map (a unital positive linear map). For any effect $e$ in the region $X$ (an element $e \in A(X)$ satisfying $0 \le e \le 1$), the effect mapped into the larger region $Y$ via $\iota_{X,Y}$ is equal to the result of applying the inclusion map $\iota_{X,Y}$ to $e$.

Let $N$ be a local net and let $X, Y, Z$ be regions with inclusions $h_1 : X \le Y$ and $h_2 : Y \le Z$. For any effect $e$ in region $X$ (an element $e \in A(X)$ such that $0 \le e \le 1$), let $\iota_{X,Y}(e)$ denote the corresponding effect in region $Y$. Then mapping the effect $e$ directly from $X$ to $Z$ is equivalent to mapping it first from $X$ to $Y$ and then from $Y$ to $Z$: $$\iota_{X,Z}(e) = \iota_{Y,Z}(\iota_{X,Y}(e)).$$

Given a local net $N$ and an inclusion of regions $X \leq Y$, let $\iota : A(X) \to A(Y)$ be the unital positive linear map that includes the observables of the smaller region into the larger one. For a state $\omega$ on the observables of the region $Y$, its restriction to the subregion $X$ is the state on $A(X)$ defined by the composition $\omega \circ \iota$.

Let $N$ be a local net and let $X \leq Y$ be an inclusion of regions. Let $\iota : A(X) \to A(Y)$ denote the unital positive linear map that includes the observables of the smaller region $X$ into the larger region $Y$. For any state $\omega$ on the observables of $Y$ and any observable $a \in A(X)$, the value of the restricted state $N.\text{restrict } h \, \omega$ evaluated at $a$ is equal to the value of the state $\omega$ evaluated at the included observable $\iota(a)$. That is, $$(N.\text{restrict } h \, \omega)(a) = \omega(\iota(a)).$$

Given a local net $N$ and a region $X$, let $A(X)$ be the space of observables associated with that region and $\mathcal{S}[\mathbb{R}, A(X)]$ be the set of states on those observables. For any state $\omega \in \mathcal{S}[\mathbb{R}, A(X)]$, the restriction of $\omega$ to the region $X$ itself, corresponding to the identity inclusion $X \leq X$, is equal to $\omega$.

Given a local net $N$ and regions $X, Y,$ and $Z$ such that $X \le Y$ and $Y \le Z$, let $\omega$ be a state on the observable space $A(Z)$. The restriction of $\omega$ from $Z$ to $Y$ followed by a restriction from $Y$ to $X$ is equal to the direct restriction of $\omega$ from $Z$ to $X$ via the inclusion $X \le Z$.

A local net $N$ is **faithful** if for every pair of regions $X, Y$ with $X \le Y$, the inclusion map $\iota_{X,Y} : A(X) \to A(Y)$ is an order embedding. This means that for any observables $a, b \in A(X)$, the relation $\iota_{X,Y}(a) \le \iota_{X,Y}(b)$ holds in $A(Y)$ if and only if $a \le b$ holds in $A(X)$.

Let $N$ be a faithful local net of observables that assigns a space of observables $A(X)$ to each region $X$. For any two regions $X$ and $Y$ such that $X \le Y$, the inclusion map $\iota_{X,Y} : A(X) \to A(Y)$ is injective.