PhyslibAlpha.ProbabilisticTheory.Channel.Basic

The notation $E \to_{p1}[R] F$ represents the type of **unital positive linear maps** from $E$ to $F$ over a ring $R$. These are linear maps that are both: 1. **Unital**: They map the identity element of $E$ to the identity element of $F$. 2. **Positive**: They map non-negative elements in $E$ to non-negative elements in $F$.

A unital positive linear map $f$ from an order-unit space $E$ to $F$ (denoted $E \to_{p1}[R] F$) can be treated as a function, allowing it to be applied to an element $x \in E$ to produce a value $f(x) \in F$.

Let $R$ be a ring and $E, F$ be modules over $R$. Any unital positive linear map $f$ from $E$ to $F$ (denoted $E \to_{p1}[R] F$) is a linear map. That is, the type of unital positive linear maps satisfies the requirements of the `LinearMapClass`, ensuring that these maps preserve addition and scalar multiplication.

Let $E$ and $F$ be order-unit spaces. Every unital positive linear map $f: E \to F$ (denoted $E \to_{p1}[R] F$) is an order homomorphism; that is, if $x \le y$ in $E$, then $f(x) \le f(y)$ in $F$.

Every unital positive linear map $f$ from an order-unit space $E$ to $F$ (denoted $E \to_{p1}[R] F$) preserves the identity element, such that $f(1) = 1$.

Let $E$ and $F$ be order-unit spaces over a semiring $R$. If two unital positive linear maps $f, g: E \to F$ satisfy $f(x) = g(x)$ for all $x \in E$, then $f = g$.

The assignment of a unital positive linear map $f : E \to_{p1}[R] F$ to its underlying linear map is injective. This implies that if two unital positive linear maps have the same underlying linear transformation, they are equal as bundled objects.

Let $R$ be a semiring, and let $E$ and $F$ be $R$-modules equipped with a partial order and a unit element $1$. Given a linear map $f: E \to F$, a proof $h_{\text{pos}}$ that $f(x) \ge 0$ for all $x \ge 0$, and a proof $h_{\text{one}}$ that $f(1) = 1$, this definition bundles $f$ into a unital positive linear map from $E$ to $F$.

Let $R$ be a semiring and $E$ be an ordered module over $R$ equipped with a unit element $1$. The identity unital positive linear map $\text{id} : E \to E$ is the linear map that sends every element $x \in E$ to itself, while preserving the unit element and the nonnegativity of observables.

Let $R$ be a semiring and $E_1$ be a module over $R$ equipped with a partial order and a unit element $1$. For any element $x \in E_1$, the identity unital positive linear map $\text{id} : E_1 \to E_1$ satisfies $\text{id}(x) = x$.

Let $R$ be a semiring and let $E$, $F$, and $G$ be modules over $R$ equipped with a partial order and a unit element $1$. Given two unital positive linear maps $f: E \to F$ and $g: F \to G$, their composition $g \circ f$ is the unital positive linear map from $E$ to $G$ obtained by composing the underlying linear maps.

Let $R$ be a semiring and let $E_1$, $E_2$, and $E_3$ be modules over $R$ that are equipped with a partial order and a unit element $1$. For any unital positive linear maps $g: E_2 \to E_3$ and $f: E_1 \to E_2$, and for any element $a \in E_1$, the application of the composed map $g \circ f$ to $a$ is equal to $g(f(a))$.

Let $R$ be a semiring, and let $E$ and $F$ be modules over $R$ equipped with a partial order and a unit element $1$. For any unital positive linear map $f: E \to F$, the composition of $f$ with the identity unital positive linear map on $E$ (denoted $\text{id}_E$) is equal to $f$, i.e., $f \circ \text{id}_E = f$.

Let $R$ be a semiring, and let $E$ and $F$ be modules over $R$ equipped with a partial order and a unit element $1$. For any unital positive linear map $f : E \to F$, the composition of the identity map on $F$, denoted as $\text{id}_F$, with $f$ is equal to $f$. That is, $\text{id}_F \circ f = f$.

Let $R$ be a semiring and let $E, F, G,$ and $H$ be modules over $R$, each equipped with a partial order and a unit element $1$. Given three unital positive linear maps $f: E \to F$, $g: F \to G$, and $h: G \to H$, the composition of these maps is associative: $$h \circ (g \circ f) = (h \circ g) \circ f$$

Let $R$ be a semiring and $E$ be a module over $R$ equipped with a partial order and a unit element $1$. The set of unital positive linear maps from $E$ to itself (endomorphisms) forms a monoid, where the binary operation is given by the composition of maps $g \circ f$ and the identity element is the identity unital positive linear map $\text{id}_E$.

For two $C^*$-algebras $A_1$ and $A_2$ equipped with a unit and a star-ordered ring structure, a quantum channel is a unital completely positive (UCP) map from $A_1$ to $A_2$. Such a map $f: A_1 \to A_2$ is linear, preserves the identity ($f(1_{A_1}) = 1_{A_2}$), and is completely positive, meaning it remains positive under matrix amplification.