PhyslibAlpha.ProbabilisticTheory.LocalNet.Maps

Let $E$ and $F$ be spaces of observables (order-unit spaces). A channel $\phi : E \to F$ is an **order embedding** if it reflects the partial order of the observables: for any $a, b \in E$, the condition $\phi(a) \le \phi(b)$ implies $a \le b$. Since channels are monotonic by definition, this property ensures that $\phi$ preserves and reflects the order, identifying $E$ as an ordered subsystem of $F$.

Let $E$ and $F$ be order-unit spaces representing systems of observables. For a channel $\phi : E \to F$ that is an order embedding, the order between any two observables $a, b \in E$ is preserved and reflected by $\phi$. That is, $\phi(a) \le \phi(b)$ if and only if $a \le b$.

Let $E$ and $F$ be order-unit spaces representing systems of physical observables. A channel $\phi : E \to F$ is an order embedding (meaning $\phi(a) \le \phi(b) \implies a \le b$ for all $a, b \in E$) if and only if it reflects positivity: for any observable $a \in E$, if $0 \le \phi(a)$, then $0 \le a$.

Let $E$ and $F$ be order-unit spaces representing physical systems of observables. If a channel $\phi : E \to F$ is an order embedding (meaning that for any $a, b \in E$, $\phi(a) \le \phi(b)$ implies $a \le b$), then $\phi$ is injective.

Let $E$ be an order-unit space representing a physical system of observables. The identity channel $\text{id} : E \to E$, which maps every observable to itself, is an order embedding. That is, for any observables $a, b \in E$, the condition $\text{id}(a) \le \text{id}(b)$ implies $a \le b$.

Let $E, F$, and $G$ be spaces of observables. If $\phi : E \to F$ and $\psi : F \to G$ are channels that are order embeddings (meaning $\phi(a) \le \phi(b) \implies a \le b$ and $\psi(a) \le \psi(b) \implies a \le b$ for all observables in their respective domains), then their composition $\psi \circ \phi : E \to G$ is also an order embedding.

An order-unit isomorphism $e$ between two systems of observables $E$ and $F$ can be treated as a function. This allows for the direct application of $e$ to an observable $x \in E$ to produce a value $e(x) \in F$, where the underlying mapping is the isomorphism's forward channel.

Let $E$ and $F$ be systems of observables. For any two order-unit isomorphisms $e, e' : E \to F$, if $e(x) = e'(x)$ for all $x \in E$, then $e = e'$.

Let $E$ and $F$ be systems of observables (modeled as order-unit spaces). For any order-unit isomorphism $e : E \to F$ and any observable $x \in E$, the application of the underlying channel (the forward unital positive linear map) of $e$ to $x$ is equal to the application of $e$ to $x$ when treated as a function. That is, $e.\text{toChannel}(x) = e(x)$.

Let $E$ and $F$ be order-unit spaces representing systems of observables. For any order-unit isomorphism $e : E \to F$ and any observable $x \in E$, applying the isomorphism $e$ and then applying its inverse channel $e^{-1}$ returns the original observable $x$. Mathematically, this is expressed as $e^{-1}(e(x)) = x$.

Let $E$ and $F$ be systems of observables (order-unit spaces). For any order-unit isomorphism $e: E \to F$ and any observable $y \in F$, applying the inverse channel $e^{-1}$ of the isomorphism to $y$ and then applying $e$ to the result returns the original observable $y$. That is, $e(e^{-1}(y)) = y$.

Let $E$ be an order-unit space, representing a physical system of observables. The identity order-unit isomorphism is the reversible transformation from $E$ to itself where both the forward mapping and its inverse are the identity map. It maps every observable $x \in E$ to itself while preserving the ordering of observables and the unit element $1$.

Let $E$ be an order-unit space representing a physical system of observables. For any observable $x \in E$, applying the identity order-unit isomorphism $\text{refl}_E$ to $x$ results in the observable itself: $$\text{refl}_E(x) = x$$

Given an order-unit isomorphism $e: E \cong F$ between two order-unit spaces $E$ and $F$, this construction defines the inverse isomorphism $e^{-1}: F \cong E$ by interchanging the roles of the underlying channel and its inverse.

Let $E$ and $F$ be systems of observables. For any order-unit isomorphism $e : E \cong F$ and any observable $y \in F$, the application of the inverse isomorphism $e^{-1}$ (denoted `e.symm`) to $y$ is equal to the evaluation of the underlying inverse channel of $e$ at $y$: $$e^{-1}(y) = e.\text{invChannel}(y)$$

Let $E$ and $F$ be order-unit spaces. For any order-unit isomorphism $e : E \cong F$, the inverse of its inverse is equal to the original isomorphism, i.e., $(e^{-1})^{-1} = e$.

Let $E$, $F$, and $G$ be systems of observables. Given an order-unit isomorphism $e: E \cong F$ and an order-unit isomorphism $e': F \cong G$, their composition $e' \circ e$ (denoted as $e.\text{trans } e'$) is the order-unit isomorphism from $E$ to $G$ whose underlying forward map is the composition of the forward maps of $e'$ and $e$, and whose inverse map is the composition of the inverse maps of $e$ and $e'$.

Let $E$, $F$, and $G$ be systems of observables. For any order-unit isomorphisms $e: E \cong F$ and $e': F \cong G$, and any observable $x \in E$, the application of the composed isomorphism $e' \circ e$ (denoted in Lean as `e.trans e'`) to $x$ satisfies $(e' \circ e)(x) = e'(e(x))$.

Let $E$ and $F$ be order-unit spaces representing physical systems of observables. For any order-unit isomorphism $e: E \cong F$, the composition of the identity isomorphism $\text{refl}_E$ with $e$ is equal to $e$.

Let $E$ and $F$ be order-unit spaces representing systems of physical observables. For any order-unit isomorphism $e: E \cong F$ (a reversible change of description), let $\text{refl}_F$ be the identity order-unit isomorphism on $F$. The composition of $e$ with $\text{refl}_F$ is equal to $e$. In mathematical notation, this is expressed as $e \circ \text{id}_F = e$.

Let $E, F, G,$ and $H$ be systems of observables. For any order-unit isomorphisms $e: E \cong F$, $e': F \cong G$, and $e'': G \cong H$, the composition of these isomorphisms is associative: $$(e.\text{trans } e').\text{trans } e'' = e.\text{trans } (e'.\text{trans } e'')$$

Let $E$ and $F$ be order-unit spaces representing physical systems of observables. For any order-unit isomorphism $e: E \cong F$, the composition of its inverse $e^{-1}: F \cong E$ and the original isomorphism $e$ (applying the inverse first) is the identity isomorphism on $F$, denoted as $e \circ e^{-1} = \text{id}_F$.

Let $E$ and $F$ be order-unit spaces representing physical systems of observables. For any order-unit isomorphism $e : E \cong F$, the composition of $e$ and its inverse $e^{-1}$ (denoted as $e.\text{symm}$) is the identity order-unit isomorphism on $E$. Mathematically, this is expressed as $e \circ e^{-1} = \text{id}_E$.

Let $E$, $F$, and $G$ be systems of observables. For any order-unit isomorphisms $e: E \cong F$, $a: F \cong G$, and $b: F \cong G$, if the composition $a \circ e$ is equal to $b \circ e$, then $a$ is equal to $b$. Here, an order-unit isomorphism represents a reversible transformation between systems that preserves the order of observables and the unit (the certain outcome).

Let $E, F,$ and $G$ be systems of observables (order-unit spaces). For any order-unit isomorphisms $a, b : E \cong F$ and $e : F \cong G$, if the composition of $a$ with $e$ is equal to the composition of $b$ with $e$ (denoted $a.\text{trans } e = b.\text{trans } e$), then $a = b$. This indicates that order-unit isomorphisms are right-cancellative with respect to composition.

Given an order-unit isomorphism $e : E \to F$ between two systems of observables $E$ and $F$, the map $e$ is a bijective function. Here, an order-unit isomorphism represents a reversible transformation between systems that preserves the order of observables and the certain outcome (the order unit).

Let $E$ and $F$ be order-unit spaces representing systems of observables. For any order-unit isomorphism $e : E \to F$, the corresponding channel is an order embedding. That is, for any observables $a, b \in E$, the condition $e(a) \le e(b)$ implies $a \le b$.

Given an order-unit isomorphism $e : E \to F$ between two systems of observables and a state $\omega$ on the system $F$, the pullback of $\omega$ along $e$ is the state on system $E$ defined by the composition $\omega \circ e$. For any observable $x \in E$, the value of the pullback state is given by $\omega(e(x))$.

Given an order-unit isomorphism $e: E \to F$ between two systems of observables $E$ and $F$, for any state $\omega \in \mathcal{S}[\mathbb{R}, F]$ and any observable $x \in E$, the evaluation of the pullback state $e.\text{pullback } \omega$ at $x$ is equal to the evaluation of the state $\omega$ at the transformed observable $e(x)$, i.e., $(e.\text{pullback } \omega)(x) = \omega(e(x))$.

Let $E, F,$ and $G$ be systems of observables. Given order-unit isomorphisms $e : E \to F$ and $e' : F \to G$, and a state $\omega \in \mathcal{S}[\mathbb{R}, G]$ on the system $G$, the pullback of $\omega$ along the composition $e' \circ e$ (denoted as $e.\text{trans } e'$) is equal to the pullback along $e$ of the state obtained by pulling back $\omega$ along $e'$. That is, $$(e.\text{trans } e').\text{pullback } \omega = e.\text{pullback } (e'.\text{pullback } \omega)$$

This definition interprets an order-unit isomorphism $e: E \cong E$ from an order unit space $E$ to itself as a symmetry of the system. A symmetry is a channel (a positive, unital linear map) that possesses a two-sided inverse channel, thereby acting as an order-automorphism of $E$.

Given a symmetry $\phi$ of an order unit space $E$, this definition constructs the corresponding order-unit isomorphism from $E$ to itself. It uses the channel associated with $\phi$ as the forward map and the inverse channel $\phi^{-1}$ (provided by the fact that $\phi$ is an order-automorphism) as the inverse map, satisfying $\phi^{-1} \circ \phi = \text{id}_E$ and $\phi \circ \phi^{-1} = \text{id}_E$.

Let $E$ be an order unit space. For any two order-unit isomorphisms $e, e' : E \cong E$, the symmetry associated with their composition $e.{\text{trans }} e'$ is equal to the product of the individual symmetries of $e'$ and $e$ in the symmetry group of $E$. That is, $$(e.{\text{trans }} e').\text{toSymmetry} = e'.\text{toSymmetry} \cdot e.\text{toSymmetry}$$ where $e.{\text{trans }} e'$ denotes the composition of isomorphisms (applying $e$ then $e'$, or $e' \circ e$), and the multiplication $\cdot$ in the symmetry group corresponds to the composition of the underlying channels.

Let $E$ be an order-unit space. The symmetry of $E$ obtained from the identity order-unit isomorphism $\text{refl}_E$ is the identity element $1$ of the symmetry group $\text{Symmetry}(E)$.

For any symmetry $\phi$ of an order unit space $E$, converting $\phi$ into an order-unit isomorphism and then back into a symmetry returns the original symmetry $\phi$. That is, $(\text{ofSymmetry } \phi).\text{toSymmetry} = \phi$.

Let $E$ be an order unit space representing a physical system. For any symmetry $\phi$ of $E$ and any observable $x \in E$, applying the order-unit isomorphism induced by $\phi$ to $x$ is equivalent to applying the underlying channel of $\phi$ to $x$. That is: $$\text{ofSymmetry}(\phi)(x) = \phi(x)$$