Unital channels as a real convex set

For every natural number $d$, including $d=0$, this definition gives a set of functions $\Phi:M_d(\mathbb C)\to M_d(\mathbb C)$, where $M_d(\mathbb C)$ consists of complex matrices whose rows and columns are indexed by $\{0,\ldots,d-1\}$. A function belongs to this set exactly when there exist a natural number $m$ and matrices $E_j\in M_d(\mathbb C)$ for every $j\in\{0,\ldots,m-1\}$ such that $\sum_{j=0}^{m-1}E_j^*E_j=I_d$, and for every complex matrix $\rho\in M_d(\mathbb C)$ one has $\Phi(\rho)=\sum_{j=0}^{m-1}E_j\rho E_j^*$, and additionally $\Phi(I_d)=I_d$. Here $E_j^*$ denotes the conjugate transpose, matrix products and sums have their usual meanings, and $I_d$ is the identity matrix. The universal quantifier over $\rho$ ranges over all complex matrices without positivity or trace restrictions; no linearity assumption is separately imposed on the initially quantified function. The integer $m$ may be zero, in which case both sums are zero matrices: the normalization then cannot hold when $d>0$, whereas when $d=0$ there is only one empty matrix, its identity equals its zero matrix, and the unique function on this one-element matrix space satisfies the conditions with $m=0$.