When the Choi representation of a channel is seperable

Let $\X$ and $\Y$ be complex Euclidean spaces, and let $\Phi\in\Channel(\X,\Y)$ be a channel. A positive operator $P\in \Pos(\X\otimes\Y)$ is separable if and only if there exists a positive integer $m$ and positive semi definite operators
\[
Q_1,Q_2, \dots, Q_m\in\Pos(\X) \ \ \text{and} \ \ R_1,R_2, \dots, R_m\in\Pos(\Y)
\]
such that
\[
P=\SUM{j=1}{m}Q_j\otimes R_j
\]
Denote by $\Sep(\X : \Y)$ the collection of all such separable operators.

Theorem:

The following two properties are equivalent:
  1. For every complex Euclidean space $\Z$ and everydensity operator $\rho\in\Density(\X\otimes\Z)$, it holds that $\bigl(\Phi\otimes \I_{\Lin(\Z)}\bigr)(\rho) \in \Sep(\Y:\Z)$.
  2. $J(\Phi) \in \Sep(\Y:\X)$.

Proof:

Recall that the Choi representation $J(\Phi)$ can be expressed as
\[
J(\Phi)=(\Phi\otimes\I_{\Lin(\X)})(\vec(\I_{\X})\vec(\I_{\X})^\ast).
\]
Now first assume that property 1 holds, and let $\Z=\X=\mathbb{C}^\Sigma$ and consider the density operator $\rho\in\Density(\X\otimes\X)$ given by
\[
\rho=\frac{1}{|\Sigma|}(\vec(\I_\X)\vec(\I_\X)^\ast).
\]
The assumption of property 1 then reads
\[
(\Phi\otimes\I_{\Lin(\X)})(\vec(\I_\X)\vec(\I_\X)^\ast)\in\Sep(\Y:\X),
\]
implying that $J(\Phi)\in\Sep(\Y : \X)$, which is the claim of property 2

Instead, now assume that property 2 holds so that 2: $J(\Phi) \in \Sep(\Y:\X)$. Then by the Woronowicz-Horodecki criterion this statement is equivalent to one where for every complex Euclidean space $\Z$ and every positive map $\Xi\in\Trans(\Y,\Z)$
\[
(\Xi\otimes\I_{\Lin(\X)})(J(\Phi))\in\Pos(\Z\otimes\X).
\]

Substituting the expression recalled above for $J(\Phi)$ then gives
\[\begin{align*}
(\Xi\otimes\I_{\Lin(\X)})(J(\Phi))&=(\Xi\otimes\I_{\Lin(\X)})(\Phi\otimes\I_{\Lin(\X)})(\vec(\I_{\X})\vec(\I_{\X})^\ast) \\
&=(\Xi(\Phi)\otimes\I_{\Lin(\X)})(\vec(\I_{\X})\vec(\I_{\X}^\ast))\\
&=J(\Xi(\Phi)).
\end{align*}\]

Hence, $J(\Xi(\Phi))\in\Pos(\Z\otimes\X)$. This implies that there exists a complex Euclidean space $\W$ an an operator $A\in\Lin(\X,\Z\otimes\W)$ such that
\[
\Xi(\Phi)(X)=\tr_{|W}(AXA^\ast)
\]
for all $X\in\Lin(\X)$. Consider any $\rho\Density(\X\otimes\Z)$. Then
\[
(\Xi\otimes\I_{\Lin(\X)})(\Phi\otimes\I_{\Lin(\X)})(\vec(\I_{\X})\vec(\I_{\X})^\ast)(\rho)\in\Pos(\Z\otimes\X),
\]
 which should imply that $(\Phi\otimes\I_{L(\Z)})(\rho)\in\Sep(\Y:\Z)$ by the Woronowicz-Horodecki criterion.