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
∑ | | xnp | 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 enp is the sequence of complex numbers given by enpij = δniδpj. By bilinearity of tensor we have:
Furthermore the system of vectors (enp) 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 pp * + qq * = 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 = !(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 ; 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.