QuantumInfo.Finite.CPTPMap.Bundled

Let $\Lambda$ be a Hermitian-preserving matrix map from matrices of dimension $d_{in}$ to matrices of dimension $d_{out}$ over a field $\mathbb{k}$. The function $\Lambda.\text{map}$ returns the underlying linear map $M: \text{Mat}_{d_{in}}(\mathbb{k}) \to \text{Mat}_{d_{out}}(\mathbb{k})$ associated with $\Lambda$.

Let $\Lambda_1$ and $\Lambda_2$ be Hermitian-preserving matrix maps. If their underlying matrix mapping functions are equal (i.e., $\Lambda_1.\text{map} = \Lambda_2.\text{map}$), then the bundled maps $\Lambda_1$ and $\Lambda_2$ are equal.

Let $\Lambda_1$ and $\Lambda_2$ be Hermitian-preserving matrix maps from matrices of dimension $d_{in}$ to matrices of dimension $d_{out}$ over $\mathbb{C}$. If for every Hermitian matrix $M$ of dimension $d_{in}$, the maps agree such that $\Lambda_1(M) = \Lambda_2(M)$, then the maps themselves are equal ($\Lambda_1 = \Lambda_2$).

Let $C\Lambda_1$ and $C\Lambda_2$ be hermitian-preserving matrix maps from $dIn$ to $dOut$ over $\mathbb{C}$. If for every hermitian matrix $M$ of dimension $dIn$ that is positive semidefinite ($0 \le M$), the maps agree such that $C\Lambda_1(M) = C\Lambda_2(M)$, then the maps themselves are equal ($C\Lambda_1 = C\Lambda_2$).

Let $C\Lambda_1$ and $C\Lambda_2$ be hermitian-preserving matrix maps from $dIn$ to $dOut$ over the complex numbers $\mathbb{C}$. If for every hermitian matrix $M$ of dimension $dIn$ that is both positive semidefinite ($0 \le M$) and has a trace equal to one ($M.\text{trace} = 1$), the maps agree such that $C\Lambda_1(M) = C\Lambda_2(M)$, then the maps themselves are equal ($C\Lambda_1 = C\Lambda_2$).

Let $\Lambda_1$ and $\Lambda_2$ be Hermitian-preserving matrix maps from $d_{In} \times d_{In}$ matrices to $d_{Out} \times d_{Out}$ matrices over the complex numbers $\mathbb{C}$. If for every mixed state $\rho$ of dimension $d_{In}$, the maps agree on the underlying matrix representation $m(\rho)$ of the state, such that $\Lambda_1(m(\rho)) = \Lambda_2(m(\rho))$, then the maps are equal ($\Lambda_1 = \Lambda_2$). (Here, a mixed state $\rho$ is a positive semidefinite Hermitian matrix with trace 1).

The type `HPMap dIn dOut ℂ` of Hermitian-preserving maps is endowed with a function-like structure (`FunLike`). This allows an element $\Lambda \in \text{HPMap}(d_{In}, d_{Out}, \mathbb{C})$ to be treated as a function that maps a Hermitian matrix $\rho \in \text{HermitianMat}_{d_{In}}(\mathbb{C})$ to a Hermitian matrix in $\text{HermitianMat}_{d_{Out}}(\mathbb{C})$. The value of this function is defined as $\Lambda(\rho) = \Lambda.\text{map}(\rho_{mat})$, where $\Lambda.\text{map}$ is the underlying linear map on complex matrices.

Let $\Lambda$ be a Hermitian-preserving map (an `HPMap`) from $d_{in} \times d_{in}$ matrices to $d_{out} \times d_{out}$ matrices over the complex numbers $\mathbb{C}$. Let $\rho$ be a Hermitian matrix of dimension $d_{in}$ (represented as a subtype consisting of a matrix and a proof of its Hermiticity). The application of $\Lambda$ to $\rho$, denoted by $\Lambda \rho$, is equal to the Hermitian matrix whose underlying matrix is $\Lambda.\text{map}(\rho.1)$ and whose proof of Hermiticity is $\Lambda.\text{HP}(\rho.2)$.

Let $d_{In}$ be a finite type (dimension index) and $d_{Out}$ be a type. Let $\text{HPMap}(d_{In}, d_{Out}, \mathbb{C})$ be the type of Hermitian-preserving linear maps between complex matrices of these dimensions. There exists an instance of `ContinuousLinearMapClass` for $\text{HPMap}(d_{In}, d_{Out}, \mathbb{C})$ over the scalar field $\mathbb{R}$, treating the space of Hermitian matrices $\text{HermitianMat}(d, \mathbb{C})$ as a real vector space. This characterizes complex Hermitian-preserving maps as continuous $\mathbb{R}$-linear maps when restricted to the domain and codomain of Hermitian matrices.

Let $\Lambda_1$ and $\Lambda_2$ be positive-preserving maps (of type `PMap`) from input dimension $dIn$ to output dimension $dOut$ over a field $\mathbb{k}$. If the underlying matrix maps associated with $\Lambda_1$ and $\Lambda_2$ are equal (i.e., $\Lambda_1.\text{map} = \Lambda_2.\text{map}$), then the positive-preserving maps themselves are equal ($\Lambda_1 = \Lambda_2$).

Let $d_{In}$ and $d_{Out}$ be finite types and $\mathbb{k}$ be a field (typically $\mathbb{C}$ or $\mathbb{R}$). Consider the mapping `toHPMap` which casts a positive-preserving map (an element of `PMap`) to its underlying Hermitian-preserving map (an element of `HPMap`). This mapping is injective; that is, if two positive-preserving maps map to the same Hermitian-preserving map, they are identical.

The type of positive-preserving maps $\text{PMap}$ between complex matrices of dimensions $d_{In}$ and $d_{Out}$ behaves like a type of functions. It maps a Hermitian matrix $\rho \in \text{HermitianMat}(d_{In}, \mathbb{C})$ to another Hermitian matrix $\Lambda(\rho) \in \text{HermitianMat}(d_{Out}, \mathbb{C})$. This is implemented by composing the coercion of its underlying Hermitian-preserving map with the conversion from a positive-preserving map.

Let $\Lambda$ be a positive-preserving map (an element of `PMap`) between the spaces of matrices of dimensions $d_{In}$ and $d_{Out}$ over the complex numbers $\mathbb{C}$. Let $\rho$ be a Hermitian matrix of dimension $d_{In}$, represented as a subtype pair $\langle\rho.1, \rho.2\rangle$ where $\rho.1$ is the underlying matrix and $\rho.2$ is the proof of its hermiticity. The application of the map $\Lambda$ to $\rho$ is equal to the Hermitian matrix whose underlying matrix is $\Lambda.map$ applied to $\rho.1$, and whose hermiticity proof is given by the fact that $\Lambda$ is a Hermitian-preserving map ($\Lambda.HP$).

Let $\text{PMap}(d_{In}, d_{Out}, \mathbb{C})$ be the type of positive-preserving maps between matrices of dimension $d_{In}$ and $d_{Out}$ over the complex numbers $\mathbb{C}$. These maps satisfy the properties of a linear map class over the real numbers $\mathbb{R}$, mapping the space of Hermitian matrices of dimension $d_{In}$ to the space of Hermitian matrices of dimension $d_{Out}$.

The type of positive-preserving maps $\text{PMap}(d_{In}, d_{Out}, \mathbb{C})$ between spaces of complex matrices is an instance of a continuous order-preserving homomorphism class (`ContinuousOrderHomClass`). This means that for any such map $\Lambda$, the induced function from the space of Hermitian matrices $\text{HermitianMat}(d_{In}, \mathbb{C})$ to $\text{HermitianMat}(d_{Out}, \mathbb{C})$ is both continuous and monotonic with respect to the Loewner order (the partial order $\le$ defined by positive semidefiniteness).

Let $M$ be a positive-preserving map (PMap) from $d_{\text{in}} \times d_{\text{in}}$ complex matrices to $d_{\text{out}} \times d_{\text{out}}$ complex matrices. For any Hermitian matrix $x$ of dimension $d_{\text{in}}$ such that $x$ is positive semidefinite ($0 \le x$), the image $M(x)$ is also positive semidefinite ($0 \le M(x)$).

Given a finite collection of matrices $\{M_k\}_{k \in \kappa}$ where each $M_k$ is a matrix of size $d_{\text{out}} \times d_{\text{in}}$ over a field $\mathbb{K}$ (typically $\mathbb{C}$), the map defined by the Kraus representation $\Phi(A) = \sum_{k \in \kappa} M_k A M_k^\dagger$ is a completely positive map (CPMap) from $d_{\text{in}} \times d_{\text{in}}$ matrices to $d_{\text{out}} \times d_{\text{out}}$ matrices. Here, the underlying linear map is constructed using `MatrixMap.of_kraus`, and its complete positivity is guaranteed by the property that any map in Kraus form is completely positive.

Let $\Lambda_1$ and $\Lambda_2$ be positive trace-preserving maps (PTP maps) between matrix spaces over a field $\mathbb{K}$. If the underlying linear maps associated with $\Lambda_1$ and $\Lambda_2$ are equal (i.e., $\Lambda_1.\text{map} = \Lambda_2.\text{map}$), then $\Lambda_1$ and $\Lambda_2$ are equal as PTP maps.

Let $\text{PTPMap}(d_{in}, d_{out}, \mathbb{K})$ be the space of positive trace-preserving maps between matrix spaces over a field $\mathbb{K}$, and let $\text{PMap}(d_{in}, d_{out}, \mathbb{K})$ be the space of positive-preserving maps. The canonical projection (or coercion) $f: \text{PTPMap} \to \text{PMap}$, which maps a positive trace-preserving map to its underlying positive-preserving map, is injective.

The type of positive trace-preserving maps $\text{PTPMap}$ between complex matrices of dimensions $d_{In}$ and $d_{Out}$ is equipped with an instance that allows it to behave as a type of functions. Specifically, it maps a Hermitian matrix $\rho \in \text{HermitianMat}(d_{In}, \mathbb{C})$ to another Hermitian matrix $\Lambda(\rho) \in \text{HermitianMat}(d_{Out}, \mathbb{C})$. This function behavior is defined by composing the coercion of its underlying positive-preserving map ($\text{PMap}$) with the conversion from a positive trace-preserving map.

Let $\Lambda$ be a positive trace-preserving map (PTP map) from input dimension $d_{In}$ to output dimension $d_{Out}$ over the complex numbers $\mathbb{C}$. For any Hermitian matrix $\rho$ of dimension $d_{In}$, the application of $\Lambda$ to $\rho$ is equal to the application of its underlying positive-preserving map (`toPMap`) to $\rho$.

Let $\text{PTPMap}(d_{In}, d_{Out}, \mathbb{C})$ be the type of positive trace-preserving maps between complex matrices of dimensions $d_{In}$ and $d_{Out}$. Then $\text{PTPMap}(d_{In}, d_{Out}, \mathbb{C})$ forms a class of $\mathbb{R}$-linear maps from the space of Hermitian matrices of dimension $d_{In}$ to the space of Hermitian matrices of dimension $d_{Out}$.

The type of positive trace-preserving maps ($\text{PTPMap}$) from the space of $d_{In} \times d_{In}$ Hermitian matrices to $d_{Out} \times d_{Out}$ Hermitian matrices over the complex numbers $\mathbb{C}$ forms a class of continuous order-preserving homomorphisms. Specifically, every such map $\Lambda$ is continuous and monotone, meaning that for any Hermitian matrices $\rho_1, \rho_2 \in \text{HermitianMat}(d_{In}, \mathbb{C})$, if $\rho_1 \le \rho_2$ (in the Loewner order), then $\Lambda(\rho_1) \le \Lambda(\rho_2)$.

Let $M$ be a positive trace-preserving (PTP) map from the space of Hermitian matrices of dimension $d_{In}$ to $d_{Out}$ over the complex numbers $\mathbb{C}$. For any Hermitian matrix $x$ of dimension $d_{In}$ such that $x$ is positive semidefinite ($0 \le x$), the result of applying the map $M(x)$ is also positive semidefinite ($0 \le M(x)$).

The structure of positive trace-preserving maps (`PTPMap`) from an input dimension $d_{In}$ to an output dimension $d_{Out}$ acts as a type of functions between mixed states. Specifically, for any such map $\Lambda$ and any mixed state $\rho$ of dimension $d_{In}$, the application $\Lambda(\rho)$ is defined as the mixed state in dimension $d_{Out}$ whose underlying Hermitian matrix is the image of the matrix of $\rho$ under the map. This mapping is well-defined because $\Lambda$ preserves both the positive semidefiniteness and the unit trace of the state, and it is injective relative to the underlying linear map.

Let $\Lambda$ be a positive trace-preserving map (PTP map) from input dimension $d_{In}$ to output dimension $d_{Out}$ over the complex numbers $\mathbb{C}$. Let $\rho$ be a mixed state of dimension $d_{In}$ with associated Hermitian matrix $\rho.M$ (which is positive semidefinite and has trace 1). The application of the map $\Lambda$ to the mixed state $\rho$, denoted $\Lambda(\rho)$, is the mixed state in dimension $d_{Out}$ whose underlying matrix is obtained by applying the linear map part of $\Lambda$ to $\rho.M$. This resulting state is well-defined because $\Lambda$ preserves both the positive semidefiniteness and the unit trace of the state.

Let $d_{In}$ and $d_{Out}$ be finite dimensional Hilbert space indices. The type of positive trace-preserving maps $\text{PTPMap}(d_{In}, d_{Out})$ from input mixed states to output mixed states is an instance of `ContinuousMapClass`. This means that every positive trace-preserving map $\Lambda \in \text{PTPMap}(d_{In}, d_{Out})$ is continuous when viewed as a function between the topological spaces of mixed states $\text{MState } d_{In}$ and $\text{MState } d_{Out}$, where both spaces are equipped with the subspace topology inherited from the space of complex matrices.

Let $M$ be a positive trace-preserving (PTP) map from input dimension $d_{In}$ to output dimension $d_{Out}$ over the complex numbers $\mathbb{C}$. Let $\rho$ be a mixed state (represented by an object of type `MState dIn`). The underlying Hermitian matrix of the mixed state resulting from the application $M(\rho)$ is equal to the result of applying the map $M$ (coerced as a function) to the Hermitian matrix associated with $\rho$.

Let $\Lambda$ be a positive trace-preserving (PTP) map from $d_{In} \times d_{In}$ matrices to $d_{Out} \times d_{Out}$ matrices. If the input index set $d_{In}$ is non-empty, then the output index set $d_{Out}$ must also be non-empty.

Let $\Lambda_1$ and $\Lambda_2$ be completely positive trace-preserving (CPTP) maps from input dimension $d_{In}$ to output dimension $d_{Out}$ over the field $\mathbb{k}$. If the underlying linear matrix maps of $\Lambda_1$ and $\Lambda_2$ are equal, then $\Lambda_1 = \Lambda_2$.

Let $\text{CPTPMap}(d_{In}, d_{Out}, \mathbb{k})$ be the set of completely positive trace-preserving linear maps and $\text{PTPMap}(d_{In}, d_{Out}, \mathbb{k})$ be the set of positive trace-preserving linear maps between matrix spaces of dimensions $d_{In}$ and $d_{Out}$ over the field $\mathbb{k}$. The forgetful map $\Phi: \text{CPTPMap} \to \text{PTPMap}$, which treats a completely positive trace-preserving map as a positive trace-preserving map, is injective.

For a completely positive trace-preserving (CPTP) map $\Lambda$ from the space of density matrices (mixed states) $\mathcal{M}_{d_{In}}$ to $\mathcal{M}_{d_{Out}}$, the structure provides an instance of a function-like mapping. Specifically, for any such map $\Lambda$, there is a corresponding function $\Lambda: \text{MState}(d_{In}) \to \text{MState}(d_{Out})$ defined by its action on matrix states, ensuring that CPTP maps can be applied directly to states as mathematical functions.

Let $\Lambda$ be a completely positive trace-preserving (CPTP) map from input dimension $d_{In}$ to output dimension $d_{Out}$. For any density matrix (quantum state) $\rho$ of dimension $d_{In}$, the application of $\Lambda$ to $\rho$ is equal to the application of its underlying positive trace-preserving (PTP) map to $\rho$. That is, $\Lambda(\rho) = \text{toPTPMap}(\Lambda)(\rho)$.

Let $\Lambda$ be a completely positive trace-preserving (CPTP) map from $d_{in} \times d_{in}$ matrices to $d_{out} \times d_{out}$ matrices over the field $\mathbb{k}$. Then its underlying linear map $\Lambda.\text{map}$ is trace-preserving.

Given a finite family of matrices $\{M_k\}_{k \in \kappa}$ where each $M_k \in \text{Mat}_{d_{Out} \times d_{In}}(\mathbb{k})$ satisfies the completeness relation $\sum_{k \in \kappa} M_k^\dagger M_k = I$, this definition constructs a completely positive trace-preserving (CPTP) map $\Lambda$ from $\text{Mat}_{d_{In}}(\mathbb{k})$ to $\text{Mat}_{d_{Out}}(\mathbb{k})$. The map is defined via the Kraus representation $\Lambda(\rho) = \sum_k M_k \rho M_k^\dagger$.

Let $\Lambda_1$ and $\Lambda_2$ be positive unital maps (of type `PUMap`) from input dimension $d_{In}$ to output dimension $d_{Out}$ over a field $\mathbb{k}$. If the underlying matrix maps associated with $\Lambda_1$ and $\Lambda_2$ are equal (i.e., $\Lambda_1.\text{map} = \Lambda_2.\text{map}$), then the positive unital maps themselves are equal ($\Lambda_1 = \Lambda_2$).

The function `PUMap.toPMap`, which sends a positive unital map to its underlying positive map, is injective. That is, for any two positive unital maps $\Lambda_1$ and $\Lambda_2$ between matrix spaces over the field $\mathbb{k}$, if their underlying positive maps are equal, then $\Lambda_1 = \Lambda_2$.

Positive Unital Maps ($\text{PUMap}$) from the space of $d_{In} \times d_{In}$ complex Hermitian matrices to $d_{Out} \times d_{Out}$ complex Hermitian matrices can be treated as functions. Specifically, for any such map $\Lambda$, its application to a Hermitian matrix $\rho \in \text{HermitianMat}(d_{In}, \mathbb{C})$ is defined by the action of its underlying positive map.

Let $\Lambda$ be a positive unital map between complex matrix spaces, and let $\rho$ be a Hermitian matrix. The application of the positive unital map $\Lambda$ to $\rho$ is equal to the application of its underlying positive map to $\rho$.

The type of positive unital maps from $d_{In} \times d_{In}$ complex matrices to $d_{Out} \times d_{Out}$ complex matrices, denoted as $\text{PUMap}(d_{In}, d_{Out}, \mathbb{C})$, satisfies the `LinearMapClass` requirements. Specifically, any such map $\Lambda$ acts as an $\mathbb{R}$-linear map between the spaces of $\text{Hermitian}$ matrices $\text{HermitianMat}(d_{In}, \mathbb{C})$ and $\text{HermitianMat}(d_{Out}, \mathbb{C})$.

Let $\text{PUMap}(d_{In}, d_{Out}, \mathbb{C})$ be the space of positive unital maps from $d_{In} \times d_{In}$ complex matrices to $d_{Out} \times d_{Out}$ complex matrices. Any such map $\Lambda \in \text{PUMap}(d_{In}, d_{Out}, \mathbb{C})$ is a continuous order-preserving homomorphism from the space of Hermitian matrices $\text{HermitianMat}(d_{In}, \mathbb{C})$ to $\text{HermitianMat}(d_{Out}, \mathbb{C})$. This implies that $\Lambda$ is continuous with respect to the matrix topologies and satisfies $A \le B \implies \Lambda(A) \le \Lambda(B)$ for any Hermitian matrices $A, B$.

Let $\text{PUMap}(d_{In}, d_{Out}, \mathbb{C})$ be the space of positive unital maps from $d_{In} \times d_{In}$ complex matrices to $d_{Out} \times d_{Out}$ complex matrices. Any such map $\Lambda$ is a "one-preserving homomorphism" between the spaces of Hermitian matrices $\text{HermitianMat}(d_{In}, \mathbb{C})$ and $\text{HermitianMat}(d_{Out}, \mathbb{C})$. Specifically, $\Lambda$ maps the identity matrix $I_{d_{In}}$ to the identity matrix $I_{d_{Out}}$ (i.e., $\Lambda(I) = I$).

Let $M$ be a positive unital map from the space of $d_{In} \times d_{In}$ complex matrices to $d_{Out} \times d_{Out}$ complex matrices. For any Hermitian matrix $x$ of size $d_{In}$ such that $x$ is positive semidefinite ($0 \le x$), its image under the map $M x$ is also positive semidefinite ($0 \le M x$).

Let $\Lambda_1$ and $\Lambda_2$ be completely positive unital maps (of type `CPUMap`) from input dimension $d_{in}$ to output dimension $d_{out}$ over a field $\mathbb{k}$. If the underlying linear maps associated with $\Lambda_1$ and $\Lambda_2$ are equal (i.e., $\Lambda_1.\text{map} = \Lambda_2.\text{map}$), then the completely positive unital maps themselves are equal ($\Lambda_1 = \Lambda_2$).

The composition of the forgetful map from completely positive unital maps ($CPUMap$) to completely positive maps ($CPMap$) and the forgetful map from completely positive maps to positive-preserving maps ($PMap$) is injective. In other words, a completely positive unital map $\Lambda$ is uniquely determined by its underlying positive-preserving map.

The type of completely positive unital maps, denoted as $\text{CPUMap}(d_{In}, d_{Out}, \mathbb{C})$, acts as a space of functions. Specifically, each element $\Lambda$ in this type maps a Hermitian matrix $\rho \in \text{HermitianMat}(d_{In}, \mathbb{C})$ to a Hermitian matrix $\Lambda(\rho) \in \text{HermitianMat}(d_{Out}, \mathbb{C})$. This functional behavior is realized through the coercion to its underlying positive-preserving map ($\text{PMap}$).

Let $\Lambda$ be a completely positive unital map (CPUMap) from input dimension $d_{In}$ to output dimension $d_{Out}$ over the complex numbers $\mathbb{C}$. For any Hermitian matrix $\rho$ of dimension $d_{In}$ over $\mathbb{C}$, the action of $\Lambda$ on $\rho$ is equal to the action of its underlying positive-preserving map (PMap) on $\rho$.

Let $\text{CPUMap}(d_{In}, d_{Out}, \mathbb{C})$ denote the type of completely positive unital maps between complex matrix spaces of dimensions $d_{In}$ and $d_{Out}$. This type forms a linear map class over the real numbers $\mathbb{R}$, acting between the space of $d_{In} \times d_{In}$ complex Hermitian matrices and the space of $d_{Out} \times d_{Out}$ complex Hermitian matrices.

The type of completely positive unital maps from $d_{in} \times d_{in}$ complex Hermitian matrices to $d_{out} \times d_{out}$ complex Hermitian matrices, denoted as `CPUMap dIn dOut ℂ`, satisfies the `ContinuousOrderHomClass` predicates. This means that every such map is a continuous function between the spaces of Hermitian matrices that preserves the partial ordering $\le$ defined on these matrices.

The type of completely positive unital maps, denoted as `CPUMap dIn dOut ℂ`, which maps complex Hermitian matrices of dimension $d_{in} \times d_{in}$ to those of dimension $d_{out} \times d_{out}$, satisfies the `OneHomClass` predicate. This means that any map $M$ in this class preserves the identity element, specifically $M(\mathbb{I}_{d_{in}}) = \mathbb{I}_{d_{out}}$, where $\mathbb{I}$ denotes the identity matrix (the "one" element in the space of Hermitian matrices).

Let $M$ be a completely positive unital map from the space of $d_{in} \times d_{in}$ complex Hermitian matrices to the space of $d_{out} \times d_{out}$ complex Hermitian matrices. For any Hermitian matrix $x \in \text{HermitianMat}(d_{in}, \mathbb{C})$, if $x$ is positive semi-definite (i.e., $0 \le x$), then its image $M(x)$ is also positive semi-definite (i.e., $0 \le M(x)$).