QuantumInfo.Finite.CPTPMap.CPTP

Let $\Lambda$ be a completely positive trace-preserving (CPTP) map from $\text{Mat}_{d_{in}}(\mathbb{C})$ to $\text{Mat}_{d_{out}}(\mathbb{C})$. The function returns the Choi matrix $\mathcal{J}(\Lambda) \in \text{Mat}_{d_{out} \times d_{in}}(\mathbb{C})$ associated with the underlying linear map of $\Lambda$. The Choi matrix is defined such that its entries are given by $(\mathcal{J}(\Lambda))_{(j_1, i_1), (j_2, i_2)} = (\Lambda(E_{i_1, i_2}))_{j_1, j_2}$, where $E_{i_1, i_2}$ is the standard basis matrix.

Let $\Lambda_1$ and $\Lambda_2$ be completely positive trace-preserving (CPTP) maps from input dimension $d_{In}$ to output dimension $d_{Out}$. If their Choi matrices are equal, denoted by $\text{choi}(\Lambda_1) = \text{choi}(\Lambda_2)$, then the maps themselves are equal, i.e., $\Lambda_1 = \Lambda_2$.

Let $\Lambda$ be a completely positive trace-preserving (CPTP) map from matrices of dimension $d_{in}$ to matrices of dimension $d_{out}$ over $\mathbb{C}$. Then its associated Choi matrix $\mathcal{J}(\Lambda)$ is positive semidefinite.

Let $\Lambda$ be a completely positive trace-preserving (CPTP) map from the space of matrices over an input index set $d_{In}$ to a space of matrices over an output index set $d_{Out}$. The trace of its associated Choi matrix, denoted $\text{Tr}(\mathcal{J}(\Lambda))$, is equal to the cardinality of the input space $|d_{In}|$.

Given a matrix $M \in \mathbb{C}^{(d_{Out} \times d_{In}) \times (d_{Out} \times d_{In})}$, if $M$ is positive semi-definite ($M \succeq 0$) and its partial trace over the output system satisfies $\text{Tr}_{Out}(M) = I$, then the linear map $L$ constructed via the Choi-Jamiołkowski isomorphism such that $J(L) = M$ is a completely positive trace-preserving (CPTP) map from $d_{In} \times d_{In}$ matrices to $d_{Out} \times d_{Out}$ matrices.

Let $M \in \text{Mat}_{(d_{out} \times d_{in}) \times (d_{out} \times d_{in})}(\mathbb{C})$ be a matrix such that $M$ is positive semi-definite ($M \succeq 0$) and its partial trace over the output system satisfies $\text{Tr}_{out}(M) = I$. If $\Lambda$ is the completely positive trace-preserving (CPTP) map constructed from $M$ via the Choi-Jamiołkowski isomorphism, then the Choi matrix of $\Lambda$ is equal to $M$, i.e., $\mathcal{J}(\Lambda) = M$.

Let $\Lambda$ be a completely positive trace-preserving (CPTP) map from $d_{In}$-dimensional density matrices to $d_{Out}$-dimensional density matrices. For any mixed state $\rho \in \text{MState}(d_{In})$, the underlying complex matrix of the state resulting from the application of the map, denoted $(\Lambda(\rho)).m$, is equal to the result of applying the underlying linear map of $\Lambda$ to the underlying matrix of $\rho$, denoted $\Lambda.\text{map}(\rho.m)$.

Let $\Lambda_1$ and $\Lambda_2$ be completely positive trace-preserving (CPTP) maps from the space of matrix states $\text{MState}(d_{In})$ to $\text{MState}(d_{Out})$. If for every density matrix $\rho \in \text{MState}(d_{In})$, the application of the maps yields the same result, i.e., $\Lambda_1(\rho) = \Lambda_2(\rho)$, then the CPTP maps are equal, $\Lambda_1 = \Lambda_2$.

Given two completely positive trace-preserving (CPTP) maps, $\Lambda_1: \text{Mat}_{d_{in}}(\mathbb{C}) \to \text{Mat}_{d_{m}}(\mathbb{C})$ and $\Lambda_2: \text{Mat}_{d_{m}}(\mathbb{C}) \to \text{Mat}_{d_{out}}(\mathbb{C})$, their composition $\Lambda_2 \circ \Lambda_1$ is the CPTP map from $\text{Mat}_{d_{in}}(\mathbb{C})$ to $\text{Mat}_{d_{out}}(\mathbb{C})$ whose underlying linear map is the function composition of the linear maps of $\Lambda_1$ and $\Lambda_2$. This composition inherits the properties of being completely positive and trace-preserving from its constituents.

The symbol $\circ_m$ denotes the composition of two completely positive trace-preserving (CPTP) maps. Given $\Lambda_2$ and $\Lambda_1$, $\Lambda_2 \circ_m \Lambda_1$ is defined as the composition $\text{CPTPMap.compose}(\Lambda_2, \Lambda_1)$.

Let $\Lambda_1: \text{Mat}_{d_{in}}(\mathbb{C}) \to \text{Mat}_{d_{m}}(\mathbb{C})$ and $\Lambda_2: \text{Mat}_{d_{m}}(\mathbb{C}) \to \text{Mat}_{d_{out}}(\mathbb{C})$ be two completely positive trace-preserving (CPTP) maps. Application of the composed CPTP map $\Lambda_2 \circ_m \Lambda_1$ to a density matrix (matrix state) $\rho$ is equal to applying $\Lambda_2$ to the result of applying $\Lambda_1$ to $\rho$, i.e., $(\Lambda_2 \circ_m \Lambda_1)(\rho) = \Lambda_2(\Lambda_1(\rho))$.

Let $\Lambda_1: \text{Mat}_{d_{in}}(\mathbb{C}) \to \text{Mat}_{d_{m}}(\mathbb{C})$, $\Lambda_2: \text{Mat}_{d_{m}}(\mathbb{C}) \to \text{Mat}_{d_{m_2}}(\mathbb{C})$, and $\Lambda_3: \text{Mat}_{d_{m_2}}(\mathbb{C}) \to \text{Mat}_{d_{out}}(\mathbb{C})$ be completely positive trace-preserving (CPTP) maps. Then the composition of these maps is associative, satisfying $(\Lambda_3 \circ \Lambda_2) \circ \Lambda_1 = \Lambda_3 \circ (\Lambda_2 \circ \Lambda_1)$.

The type of completely positive trace-preserving (CPTP) maps from $d_{In} \times d_{In}$ matrices to $d_{Out} \times d_{Out}$ matrices admits a convex structure. This is established by identifying each CPTP map with its Choi matrix in $\mathbb{C}^{(d_{Out} \times d_{In}) \times (d_{Out} \times d_{In})}$. Specifically, a linear combination of CPTP maps $\sum w_i \Lambda_i$ (where $w_i \ge 0$ and $\sum w_i = 1$) is again a CPTP map because the corresponding convex combination of Choi matrices preserves positive semi-definiteness and the trace-preserving condition $\text{Tr}_{Out}(J(\Lambda)) = I$.

Let $d_{In}$ be a finite type representing the dimensions of a Hilbert space. The identity CPTP map $id : \text{CPTPMap}(d_{In}, d_{In})$ is the completely positive trace-preserving map that acts as the identity operator on the space of complex matrices. It is defined such that its underlying linear map is the identity, and it inherits the properties of being completely positive and trace-preserving from the identity linear map.

Let $\text{id}$ be the identity completely positive trace-preserving (CPTP) map on matrices of dimension $d_{in}$. The underlying linear map of $\text{id}$ is equal to the identity linear map $I$ on the space of matrices.

Let $\text{id}$ be the identity completely positive trace-preserving (CPTP) map from $d_{In}$-dimensional density matrices to themselves. For any mixed state $\rho \in \text{MState}(d_{In})$, applying the identity map to the state leaves it unchanged, such that $\text{id}(\rho) = \rho$.

For any completely positive trace-preserving (CPTP) map $\Lambda$ from a system of dimension $d_{In}$ to a system of dimension $d_{Out}$, the composition of the identity CPTP map $\text{id}$ with $\Lambda$ is equal to $\Lambda$ itself, i.e., $\text{id} \circ_m \Lambda = \Lambda$.

For any completely positive trace-preserving (CPTP) map $\Lambda$ from a system with dimension $d_{In}$ to a system with dimension $d_{Out}$, the composition of $\Lambda$ with the identity CPTP map $id$ on the input system is equal to $\Lambda$ itself, i.e., $\Lambda \circ_m id = \Lambda$.

Given an equivalence (bijection) $\sigma : d_{In} \simeq d_{Out}$ between two finite types, the function `CPTPMap.ofEquiv` defines a Completely Positive Trace Preserving (CPTP) map between the corresponding spaces of matrices. This map is defined by the action $M \mapsto M_{\sigma^{-1}, \sigma^{-1}}$, which permutes or relabels the indices of a density matrix $\rho \in \text{MState}(d_{In})$ according to the inverse bijection $\sigma^{-1}$. Such maps represent unitary-like operations that change the underlying label type of a quantum system without loss of information.

Let $d_{In}$ and $d_{Out}$ be finite sets representing the basis dimensions of quantum systems. For any bijection (equivalence) $\sigma: d_{In} \simeq d_{Out}$ and any mixed state $\rho \in \text{MState}(d_{In})$, the action of the CPTP map induced by $\sigma$, denoted as $\text{ofEquiv}(\sigma)$, on the state $\rho$ is equal to the relabeling of $\rho$ by the inverse bijection $\sigma^{-1}$. That is, $\text{ofEquiv}(\sigma)(\rho) = \text{relabel}(\rho, \sigma^{-1})$.

Let $d_{In}$ and $d_{Out}$ be finite types, and let $\sigma: d_{In} \simeq d_{Out}$ be a bijection (equivalence) between them. Let $\text{ofEquiv}(\sigma)$ and $\text{ofEquiv}(\sigma^{-1})$ be the completely positive trace-preserving (CPTP) maps induced by $\sigma$ and its inverse, respectively. The composition of the map induced by $\sigma$ with the map induced by $\sigma^{-1}$ is equal to the identity CPTP map on the space of density matrices indexed by $d_{Out}$, such that $\text{ofEquiv}(\sigma) \circ \text{ofEquiv}(\sigma^{-1}) = \text{id}_{d_{Out}}$.

The Swap operator $\text{SWAP}$ is defined as a completely positive trace-preserving (CPTP) map from the space of density matrices on the bipartite system $d_1 \times d_2$ to the space of density matrices on the permuted system $d_2 \times d_1$. It is constructed from the underlying equivalence $\sigma: d_1 \times d_2 \simeq d_2 \times d_1$ that maps $(i, j)$ to $(j, i)$.

The associator channel `assoc` is a completely positive trace-preserving (CPTP) map from the space of density matrices on the nested system $((d_1 \times d_2) \times d_3)$ to the space $(d_1 \times (d_2 \times d_3))$. It is the quantum channel induced by the set-theoretic associativity equivalence $((i, j), k) \mapsto (i, (j, k))$ for indices $i \in d_1, j \in d_2, k \in d_3$.

The inverse associator for Completely Positive Trace Preserving (CPTP) maps is defined as the quantum channel $\Phi: \text{Lin}(\mathcal{H}_{d_1} \otimes (\mathcal{H}_{d_2} \otimes \mathcal{H}_{d_3})) \to \text{Lin}((\mathcal{H}_{d_1} \otimes \mathcal{H}_{d_2}) \otimes \mathcal{H}_{d_3})$ induced by the set-theoretic inverse associativity equivalence $(x, (y, z)) \mapsto ((x, y), z)$. It maps density matrices between these differently grouped tensor product spaces.

For any quantum mixed state $\rho$ on a composite system with dimensions $d_1 \times d_2$, the application of the SWAP CPTP map to $\rho$ is equal to the SWAP operation applied directly to the mixed state, denoted as $\text{SWAP}(\rho) = \rho.\text{SWAP}$.

Let $\rho$ be a quantum mixed state on a tripartite Hilbert space with dimensions structured as $((d_1 \times d_2) \times d_3)$. Then the application of the associator CPTP map, denoted by $\text{assoc}$, to the state $\rho$ is equal to the state-level associator $\rho.\text{assoc}$, which maps the density matrix from the space $\mathcal{M}_{(d_1 \times d_2) \times d_3}$ to $\mathcal{M}_{d_1 \times (d_2 \times d_3)}$.

For any quantum mixed state $\rho$ on a tripartite system with dimensions $d_1 \times d_2 \times d_3$, the application of the completely positive trace-preserving (CPTP) associator map $\text{assoc}'$ to $\rho$ is equal to the state-level association operation $\rho.\text{assoc}'$, which re-groups the system into dimensions $(d_1 \times d_2) \times d_3$.

Let $\text{assoc}: \text{Lin}((\mathcal{H}_{d_1} \otimes \mathcal{H}_{d_2}) \otimes \mathcal{H}_{d_3}) \to \text{Lin}(\mathcal{H}_{d_1} \otimes (\mathcal{H}_{d_2} \otimes \mathcal{H}_{d_3}))$ and $\text{assoc}': \text{Lin}(\mathcal{H}_{d_1} \otimes (\mathcal{H}_{d_2} \otimes \mathcal{H}_{d_3})) \to \text{Lin}((\mathcal{H}_{d_1} \otimes \mathcal{H}_{d_1}) \otimes \mathcal{H}_{d_3})$ be the associator and inverse associator completely positive trace-preserving (CPTP) maps, respectively. Then their composition $\text{assoc} \circ \text{assoc}'$ is equal to the identity CPTP map $\text{id}$.

A completely positive trace-preserving (CPTP) map that performs the partial trace over the first subsystem of a bipartite system. For dimensions $d_1$ and $d_2$, it maps a density matrix acting on the joint Hilbert space $\mathbb{C}^{d_1} \otimes \mathbb{C}^{d_2}$ (represented as a matrix of size $(d_1 \times d_2) \times (d_1 \times d_2)$) to a density matrix acting on the second subsystem $\mathbb{C}^{d_2}$ (represented as a matrix of size $d_2 \times d_2$). The map is defined by the partial trace operator $\text{Tr}_1: \text{Mat}_{d_1 d_2}(\mathbb{C}) \to \text{Mat}_{d_2}(\mathbb{C})$, which traces out the $d_1$-dimensional component.

A completely positive trace-preserving (CPTP) map that performs the partial trace over the second subsystem of a bipartite system. For dimensions $d_1$ and $d_2$, it maps a density matrix in the joint Hilbert space (represented as a matrix of size $d_1 \times d_2$) to a density matrix in the first subsystem of size $d_1$. Formally, it is defined as the composition of the swap operation $\text{SWAP}: d_1 \times d_2 \to d_2 \times d_1$ and the partial trace over the left subsystem $\text{traceLeft}: d_2 \times d_1 \to d_1$.

Let $\rho$ be a mixed state (density matrix) of a composite quantum system with dimensions $d_1 \times d_2$. The result of applying the partial trace channel $\text{traceLeft}$ (viewed as a completely positive trace-preserving map) to $\rho$ is equal to the reduced density matrix $\text{Tr}_1(\rho)$ obtained by the partial trace operation over the first subsystem.

Let $\rho$ be a mixed state (density matrix) of a bipartite system with dimensions $d_1 \times d_2$. The result of applying the partial trace channel $\text{traceRight}$ (as a CPTP map) to $\rho$ is equal to the reduced density matrix $\text{Tr}_2(\rho)$ obtained via the partial trace operation on states.

Given a quantum state $\rho$ of dimension $d_{\text{out}}$, the replacement channel $\mathcal{R}_\rho$ is a completely positive trace-preserving (CPTP) map from the space of states of dimension $d_{\text{in}}$ to the space of states of dimension $d_{\text{out}}$. For any input state $\sigma$, the map is defined such that $\mathcal{R}_\rho(\sigma) = \rho$. Formally, this is constructed by taking the Kronecker product of the input matrix and the matrix $\rho$, and then performing a partial trace over the input system.

Let $d_{In}$ be a non-empty index type and $d_{Out}$ be an index type with decidable equality. For any density matrix (mixed state) $\rho \in \text{MState}(d_{Out})$, the replacement channel $\text{replacement}(\rho)$ is a completely positive trace-preserving (CPTP) map from $\mathcal{M}_{d_{In}}$ to $\mathcal{M}_{d_{Out}}$. For any input state $\rho_0 \in \text{MState}(d_{In})$, the action of this map is given by $\text{replacement}(\rho)(\rho_0) = \rho$.

For two finite-dimensional index sets $d_{In}$ and $d_{Out}$ representing Hilbert spaces, if $d_{In}$ and $d_{Out}$ are non-empty, there exists a default completely positive trace-preserving (CPTP) map from $\text{MState } d_{In}$ to $\text{MState } d_{Out}$. This default map is the replacement channel $\mathcal{R}_{\rho}$, which maps any input density matrix to the default (maximally mixed) state $\rho \in \text{MState } d_{Out}$.

Given two finite types $d_{In}$ and $d_{Out}$ which are both non-empty, the type of completely positive trace-preserving (CPTP) maps from matrices indexed by $d_{In}$ to matrices indexed by $d_{Out}$ is non-empty.

For a finite-dimensional system with index set $d_{in}$ and a one-dimensional system with a unique index set $d_{out}$, where $d_{in}$ is non-empty, the map `CPTPMap.destroy` is the unique completely positive trace-preserving (CPTP) map from the space of matrices over $d_{in}$ to the space of matrices over $d_{out}$. It is defined as the replacement map that sends any input density matrix to the unique state in the 1-dimensional output space. This represents the operation of "destroying" a system or tracing out all its degrees of freedom.

For any input Hilbert space index type $d_{\text{In}}$ that is non-empty, and any output Hilbert space index type $d_{\text{Out}}$ that is a singleton (1-dimensional space), there exists a unique Completely Positive Trace Preserving (CPTP) map from the space of matrices over $d_{\text{In}}$ to the space of matrices over $d_{\text{Out}}$. This unique map is the trace operation (often called the discarding or "destroy" channel).

Let $d_{In}$, $d_{Out}$, and $d_{Out2}$ be finite types representing the dimensions of quantum systems. Suppose $d_{In}$ and $d_{Out}$ are non-empty, and $d_{Out2}$ is a singleton set (i.e., it has a unique element). Let $\Lambda: \mathcal{L}(\mathbb{C}^{d_{In}}) \to \mathcal{L}(\mathbb{C}^{d_{Out}})$ be a completely positive trace-preserving (CPTP) map. Let $\text{destroy}$ denote the unique CPTP map whose output space is a system of dimension 1. Then the composition of $\Lambda$ followed by the destroy map to $d_{Out2}$ is equal to the destroy map from $d_{In}$ to $d_{Out2}$. That is, $\text{destroy}_{d_{Out} \to d_{Out2}} \circ \Lambda = \text{destroy}_{d_{In} \to d_{Out2}}$.

Let $\Lambda_1$ be a completely positive trace-preserving (CPTP) map from matrices of dimension $d_{I_1}$ to $d_{O_1}$, and $\Lambda_2$ be a CPTP map from matrices of dimension $d_{I_2}$ to $d_{O_2}$. Their tensor product $\Lambda_1 \otimes \Lambda_2$ is a CPTP map from matrices of dimension $d_{I_1} \times d_{I_2}$ to $d_{O_1} \times d_{O_2}$. The underlying linear map is given by the Kronecker product of the maps $\Lambda_1.\text{map} \otimes_{km} \Lambda_2.\text{map}$, and it inherits the properties of being completely positive and trace-preserving from its components.

An infix notation `⊗ᶜᵖ` representing the tensor product of two completely positive trace-preserving (CPTP) maps. Given two maps $\Lambda_1: \mathcal{B}(\mathcal{H}_{in1}) \to \mathcal{B}(\mathcal{H}_{out1})$ and $\Lambda_2: \mathcal{B}(\mathcal{H}_{in2}) \to \mathcal{B}(\mathcal{H}_{out2})$, $\Lambda_1 \otimes^{cp} \Lambda_2$ denotes their tensor product as a new CPTP map from $\mathcal{B}(\mathcal{H}_{in1} \otimes \mathcal{H}_{in2})$ to $\mathcal{B}(\mathcal{H}_{out1} \otimes \mathcal{H}_{out2})$.

Given a family of completely positive trace-preserving (CPTP) maps $\Lambda_i: \mathcal{B}(\mathcal{H}_{in, i}) \to \mathcal{B}(\mathcal{H}_{out, i})$ indexed by $i \in \iota$, where each $\Lambda_i$ maps matrices over the finite type $dI_i$ to matrices over $dO_i$, the function returns their finitely-indexed tensor product $\bigotimes_{i \in \iota} \Lambda_i$. The resulting map is a CPTP map from matrices indexed by the product type $\prod_{i \in \iota} dI_i$ to matrices indexed by the product type $\prod_{i \in \iota} dO_i$. The underlying linear map is defined as the tensor product of the individual matrix maps, and it preserves both complete positivity and the trace.

Let $I$ be the index set $\{0\}$ (represented by `Fin 1`). For any family of input Hilbert spaces $dI$ and output Hilbert spaces $dO$ indexed by $I$, and for any family of completely positive trace-preserving (CPTP) maps $\Lambda_i \colon \mathcal{B}(dI_i) \to \mathcal{B}(dO_i)$, the tensor product of these maps $\bigotimes_{i \in I} \Lambda_i$ (denoted `piProd`) is equal to the single map $\Lambda_0$ up to the canonical isomorphisms between the product spaces and the individual spaces.

Let $\iota$ be an indexing set. For each $i \in \iota$, let $d_1(i)$, $d_2(i)$, and $d_3(i)$ be finite types. Suppose we have two families of completely positive trace-preserving (CPTP) maps, $\Lambda_{1,i}$ acting from matrices over $d_1(i)$ to matrices over $d_2(i)$, and $\Lambda_{2,i}$ acting from matrices over $d_2(i)$ to matrices over $d_3(i)$. Then the tensor product of the composed maps is equal to the composition of the tensor products of the maps: $$\bigotimes_{i \in \iota} (\Lambda_{2,i} \circ \Lambda_{1,i}) = \left( \bigotimes_{i \in \iota} \Lambda_{2,i} \right) \circ \left( \bigotimes_{i \in \iota} \Lambda_{1,i} \right)$$ where $\bigotimes$ denotes the tensor product of a family of CPTP maps (represented by `piProd` in the formal statement) and $\circ$ denotes map composition.

Given a unitary matrix $U \in \mathcal{U}(d_{In})$, this definition constructs the corresponding completely positive trace-preserving (CPTP) map from $\mathcal{B}(d_{In})$ to $\mathcal{B}(d_{In})$. The map is defined by the conjugation $\Lambda(X) = UXU^\dagger$ for any matrix $X$. The proof ensures that this map is both completely positive and trace-preserving.

For any unitary matrix $U \in \mathcal{U}(d_{In})$ and any density matrix (matrix state) $\rho \in \text{MState}(d_{In})$, the action of the completely positive trace-preserving (CPTP) map associated with $U$, denoted as $\text{ofUnitary}(U)$, on the state $\rho$ is equal to the unitary conjugation of $\rho$ by $U$, denoted as $\rho.U_{\text{conj}} U$ (i.e., $U \rho U^\dagger$).

A completely positive trace-preserving (CPTP) map $\Lambda$ from $d_{In}$ to $d_{In}$ is said to be unitary if there exists a unitary matrix $U \in \mathcal{U}(d_{In})$ such that $\Lambda$ is the unitary channel $\text{ofUnitary}(U)$. In terms of its action on density matrices, this means there exists a $U$ such that for all states $\rho$, $\Lambda(\rho) = U \rho U^\dagger$.

Let $\Lambda$ be a completely positive trace-preserving (CPTP) map from the space of density matrices $\mathcal{M}_{d_{In}}$ to itself. $\Lambda$ is a unitary channel (satisfies `IsUnitary`) if and only if there exists a unitary matrix $U \in \mathcal{U}(d_{In})$ such that for every density matrix $\rho \in \text{MState}(d_{In})$, the action of the map is given by unitary conjugation, $\Lambda(\rho) = U \rho U^\dagger$.

Let $d_{In}$ be a finite-dimensional Hilbert space (or a type representing the indices of a density matrix). For any permutation (equivalence) $\sigma: d_{In} \simeq d_{In}$, the CPTP map induced by this permutation, denoted as $\text{ofEquiv}(\sigma)$, is unitary.

For any completely positive trace-preserving (CPTP) map $\Lambda$ from input dimension $d_{In}$ to output dimension $d_{Out}$, there exists a unitary CPTP map $\Lambda'$ acting on the enlarged space $(d_{In} \times d_{Out} \times d_{Out})$ such that $\Lambda$ can be represented by the following sequence of operations: 1. Append a ancillary state to the input via an equivalence $\text{append}: d_{In} \to d_{In} \times \text{Unit}$. 2. Prepare an ancillary system in the fixed pure state $\rho_0 = |0\rangle\langle 0|$ on the space $d_{Out} \times d_{Out}$ and tensor it with the input: $\text{prep} = \text{id} \otimes \text{replacement}(\rho_0)$. 3. Apply the unitary evolution $\Lambda'$. 4. Perform partial traces over the ancillary systems: $\text{traceLeft} \circ \text{traceLeft}$. Mathematically, $\Lambda = \text{Tr}_{anc} \circ \Lambda' \circ (\text{id} \otimes \rho_0)$.

Given a completely positive trace-preserving (CPTP) map $\Lambda$ from an input system of dimension $d_{In}$ to an output system of dimension $d_{Out}$, its purification $\text{purify}(\Lambda)$ is a unitary CPTP map acting on the enlarged system $(d_{In} \times d_{Out} \times d_{Out})$. This construction is a canonical choice satisfying the Stinespring dilation theorem, such that $\Lambda$ can be recovered by preparing the environment in a fixed pure state $|0\rangle\langle 0|$ on $d_{Out} \times d_{Out}$ and subsequently performing a partial trace over the environment after the unitary evolution. The existence of such a map is guaranteed by the Choi–Jamiolkowski isomorphism and the fact that any CP map can be represented as a restriction of a unitary operation on a sufficiently large Hilbert space.

For any completely positive trace-preserving (CPTP) map $\Lambda$ between finite-dimensional quantum systems, its purification $\text{purify}(\Lambda)$ is a unitary CPTP map.

Let $\Lambda: \mathcal{A} \to \mathcal{B}$ be a completely positive trace-preserving (CPTP) map. Let $\Lambda_{purify}: (\mathcal{A} \otimes \mathcal{B} \otimes \mathcal{B}) \to (\mathcal{A} \otimes \mathcal{B} \otimes \mathcal{B})$ be the purified unitary channel of $\Lambda$. Then $\Lambda$ can be recovered by the following sequence of operations: 1. Append a system in a trivial state (isomorphic to $\mathbb{C}$) to the input $\mathcal{A}$. 2. Prepare two auxiliary systems of type $\mathcal{B}$ in the pure state $|0\rangle\langle 0| \otimes |0\rangle\langle 0|$, where $|0\rangle$ is the default basis vector. 3. Apply the identity map on the input system and the state preparation on the auxiliary systems (denoted as $id \otimes \Lambda_{zero\_prep}$). 4. Apply the purified unitary channel $\Lambda_{purify}$ to the combined system $(\mathcal{A} \otimes \mathcal{B} \otimes \mathcal{B})$. 5. Perform a partial trace over the two leftmost components of the output. Formally, $\Lambda = \text{Tr}_{left} \circ \text{Tr}_{left} \circ \Lambda_{purify} \circ (id \otimes \Lambda_{zero\_prep}) \circ \text{append}$.

Let $\Lambda: \text{Mat}_{d_{in}}(\mathbb{C}) \to \text{Mat}_{d_{out}}(\mathbb{C})$ be a completely positive trace-preserving (CPTP) map. The complementary channel $\widetilde{\Lambda}: \text{Mat}_{d_{in}}(\mathbb{C}) \to \text{Mat}_{d_{in} \times d_{out}}(\mathbb{C})$ is defined by tracing out the "right half" of the purified unitary channel $\Lambda.purify$. Specifically, the map is constructed as follows: 1. Append a trivial system to the input $d_{in}$ via the equivalence $d_{in} \simeq d_{in} \times 1$. 2. Prepare two auxiliary systems of dimension $d_{out}$ in the pure state $|0\rangle\langle 0| \otimes |0\rangle\langle 0|$, where $|0\rangle$ is the default basis vector. 3. Apply the identity map on the input and the state preparation on the auxiliaries ($\text{id} \otimes \Lambda_{zero\_prep}$). 4. Apply the purified unitary channel $\Lambda.purify$ to the combined system $(d_{in} \times d_{out} \times d_{out})$. 5. Apply the inverse associator $\text{assoc}'$ to regroup the systems. 6. Perform a partial trace over the rightmost subsystem ($\text{traceRight}$). Formally, $\widetilde{\Lambda} = \text{Tr}_{right} \circ \text{assoc}' \circ \Lambda.purify \circ (\text{id} \otimes \Lambda_{zero\_prep}) \circ \text{append}$.

Let $\Lambda: \mathcal{L}(\mathcal{H}_{in}) \to \mathcal{L}(\mathcal{H}_{out})$ and $\Lambda_2: \mathcal{L}(\mathcal{H}_{in}) \to \mathcal{L}(\mathcal{H}_{out_2})$ be completely positive trace-preserving (CPTP) maps (quantum channels). We say that $\Lambda$ is degradable to $\Lambda_2$ if there exists a CPTP map $D: \mathcal{L}(\mathcal{H}_{out}) \to \mathcal{L}(\mathcal{H}_{out_2})$, called a degrading channel, such that $\Lambda_2 = D \circ \Lambda$.

Let $\Lambda: \mathcal{L}(\mathcal{H}_{in}) \to \mathcal{L}(\mathcal{H}_{out})$ and $\Lambda_2: \mathcal{L}(\mathcal{H}_{in}) \to \mathcal{L}(\mathcal{H}_{out_2})$ be completely positive trace-preserving (CPTP) maps. We say that $\Lambda$ is **antidegradable to** $\Lambda_2$ if $\Lambda_2$ is degradable to $\Lambda$. That is, there exists a CPTP map $D: \mathcal{L}(\mathcal{H}_{out_2}) \to \mathcal{L}(\mathcal{H}_{out})$ such that $\Lambda = D \circ \Lambda_2$.