# GoI for MELL: exponentials

# The tensor product of Hilbert spaces

Recall that we work in the Hilbert space endowed with its canonical hilbertian basis denoted by .

The space is the collection of sequences of complex numbers such that

∑ | | x_{np} | ^{2} |

n,p |

converges. The scalar product is defined just as before:

- .

If and are vectors in *H* then their tensor is the sequence:

- .

We define: so that *e*_{np} is the sequence of complex numbers given by *e*_{npij} = δ_{ni}δ_{pj}. By bilinearity of tensor we have:

Furthermore the system of vectors (*e*_{np}) is a hilbertian basis of : the sequence may be written:

- .

## An algebra isomorphism

Being both separable Hilbert spaces, *H* and 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 . For
example set . Conversely, given
we denote by *n*_{(1)} and
*n*_{(2)} the unique integers such that .

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

This bijection can be extended into a Hilbert space isomorphism by defining:

- .

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

- .

*Remark:*
The operator !*u* is defined by:

where denotes the operator on defined by 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*= !(*u**v*); - !(
*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 ; 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 is a *p*-isometry generated by the partial permutation then we have:

- .

Thus is itself a *p*-isometry generated by the
partial permutation , which shows that the proof space is stable under the copying iso.

Given a type *A* we define the type !*A* by: