# GoI for MELL: exponentials

(The copying iso) |
m (style) |
||

Line 1: | Line 1: | ||

= The tensor product of Hilbert spaces = |
= The tensor product of Hilbert spaces = |
||

− | The space <math>H\tens H</math> is the collection of sequences <math>(x_{np})_{n,p\in\mathbb{N}}</math> of complex numbers such that: <math>\sum_{n,p}|x_{np}|^2</math> converges. The scalar product is defined just as before: |
+ | Recall that we work in the Hilbert space <math>H=\ell^2(\mathbb{N})</math> endowed with its canonical hilbertian basis denoted by <math>(e_k)_{k\in\mathbb{N}}</math>. |

+ | |||

+ | The space <math>H\tens H</math> is the collection of sequences <math>(x_{np})_{n,p\in\mathbb{N}}</math> of complex numbers such that <math>\sum_{n,p}|x_{np}|^2</math> converges. The scalar product is defined just as before: |
||

: <math>\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}</math>. |
: <math>\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}</math>. |
||

Line 7: | Line 7: | ||

: <math>x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}</math>. |
: <math>x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}</math>. |
||

− | Recall that <math>(e_k)_{k\in\mathbb{N}}</math> is the canonical hilbertian basis of <math>H=\ell^2(\mathbb{N})</math>. We define: <math>e_{np} = e_n\tens e_p</math> so that <math>e_{np}</math> is the sequence <math>(e_{npij})_{i,j\in\mathbb{N}}</math> of complex numbers given by <math>e_{npij} = \delta_{ni}\delta_{pj}</math>. By bilinearity of tensor we have: |
+ | We define: <math>e_{np} = e_n\tens e_p</math> so that <math>e_{np}</math> is the sequence <math>(e_{npij})_{i,j\in\mathbb{N}}</math> of complex numbers given by <math>e_{npij} = \delta_{ni}\delta_{pj}</math>. By bilinearity of tensor we have: |

: <math>x\tens y = \left(\sum_n x_ne_n\right)\tens\left(\sum_p y_pe_p\right) = |
: <math>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}</math> |
\sum_{n,p} x_ny_p\, e_n\tens e_p = \sum_{n,p} x_ny_p\,e_{np}</math> |

## Revision as of 11:55, 17 November 2010

# 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 .

*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 !*u* is itself a *p*-isometry and the proof space is stable under the copying iso.