GoI for MELL: exponentials

The tensor product of Hilbert spaces

Recall that we work in the Hilbert space $H=\ell^2(\mathbb{N})$ endowed with its canonical hilbertian basis denoted by $(e_k)_{k\in\mathbb{N}}$.

The space $H\tens H$ is the collection of sequences $(x_{np})_{n,p\in\mathbb{N}}$ of complex numbers such that

∑	| xnp | 2
n,p

converges. The scalar product is defined just as before:

$\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}$.

If $x = (x_n)_{n\in\mathbb{N}}$ and $y = (y_p)_{p\in\mathbb{N}}$ are vectors in H then their tensor is the sequence:

$x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}$.

We define: $e_{np} = e_n\tens e_p$ so that e_np is the sequence $(e_{npij})_{i,j\in\mathbb{N}}$ of complex numbers given by e_npij = δ_niδ_pj. By bilinearity of tensor we have:

$x\tens y = \left(\sum_n x_ne_n\right)\tens\left(\sum_p y_pe_p\right) = \sum_{n,p} x_ny_p\, e_n\tens e_p = \sum_{n,p} x_ny_p\,e_{np}$

Furthermore the system of vectors (e_np) is a hilbertian basis of $H\tens H$: the sequence $x=(x_{np})_{n,p\in\mathbb{N}}$ may be written:

$x = \sum_{n,p\in\mathbb{N}}x_{np}\,e_{np} = \sum_{n,p\in\mathbb{N}}x_{np}\,e_n\tens e_p$.

An algebra isomorphism

Being both separable Hilbert spaces, H and $H\tens H$ are isomorphic. We will now define explicitely an iso based on partial permutations.

We fix, once for all, a bijection from couples of natural numbers to natural numbers that we will denote by $(n,p)\mapsto\langle n,p\rangle$. For example set $\langle n,p\rangle = 2^n(2p+1) - 1$.

Remark: just as it was convenient but actually not necessary to choose p and q so that pp ^* + qq ^* = 1 it is actually not necessary to have a bijection, a one-to-one mapping from $\mathbb{N}^2$ into $\mathbb{N}$ would be sufficient for our purpose.

This bijection can be extended into a Hilbert space isomorphism $\Phi:H\tens H\rightarrow H$ by defining:

$e_n\tens e_p = e_{np} \mapsto e_{\langle n,p\rangle}$.

Now given an operator u on H we define the operator !u on H by:

$!u(e_{\langle n,p\rangle}) = \Phi(e_n\tens u(e_p))$.

Remark: The operator !u is defined by:

$!u = \Phi\circ (1\tens u)\circ \Phi^{-1}$

where $1\tens u$ denotes the operator on $H\tens H$ defined by $(1\tens u)(x\tens y) = x\tens u(y)$ for any x,y in H. However this notation must not be confused with the tensor of operators that was defined in the previous section in order to interpret the tensor rule of linear logic; we therefore will not use it.

One can check that given two operators u and v we have:

• !u!v = !(uv);
• !(u ^* ) = (!u) ^* .

Due to the fact that Φ is an isomorphism onto we also have !1 = 1; this however will not be used.

We therefore have that ! is a morphism on $\mathcal{B}(H)$; it is easily seen to be an iso (not onto though). As this is the crucial ingredient for interpreting the structural rules of linear logic, we will call it the copying iso.

Interpretation of exponentials

If we suppose that $u = u_\varphi$ is a p-isometry generated by the partial permutation $\varphi$ then we have:

$!u(e_{\langle n,p\rangle}) = \Phi(e_n\tens u(e_p)) = \Phi(e_n\tens e_{\varphi(p)}) = e_{\langle n,\varphi(p)\rangle}$.

Thus !u is itself a p-isometry and the proof space is stable under the copying iso.