Isometric Stinespring representation

Let $H$, $K$, and $E$ be finite-dimensional (have finite bases by Finite-dimensional vector space, and its dimension ${\dim }_{F}V$; infinite-dimensional means having no finite basis) complex inner-product spaces (Real and complex inner-product spaces and their induced length), and let $V:H\to K\otimes E$ be a linear isometry (Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces), so $V^{†}V=I_H$ by Finite-dimensional linear isometries satisfy the adjoint identity. The map

${\mathrm{\Phi }}_V(X):={\mathrm{Tr}}_E(VX{V}^{†}),X\in \mathcal{L}(H),$

is the isometric Stinespring form associated with $V$. An isometric Stinespring representation (Linear map between vector spaces over the same field) of $\mathrm{\Phi }:\mathcal{L}(H)\to \mathcal{L}(K)$ is such a formula, where ${\mathrm{Tr}}_E$ is the finite partial trace (Partial trace over a finite tensor factor) under the tensor convention Ordered tensor registers, their inner product, and wire permutations, together with its chosen finite environment $E$ and isometry $V$. The composition $V\circ X\circ V^{†}$ is an endomorphism of $K\otimes E$, and the partial trace maps it linearly to an endomorphism of $K$. Thus the displayed formula defines a complex-linear map on the full input operator space. This definition makes no existence assertion for an arbitrary map.