# GoI for MELL: exponentials

(→The tensor product of Hilbert spaces: presentation) |
(The copying iso) |
||

Line 1: | Line 1: | ||

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

− | Recall that <math>(e_k)_{k\in\mathbb{N}}</math> is the canonical basis of <math>H=\ell^2(\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: |
+ | 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>. |
||

− | In particular if we define: <math>e_{np} = e_n\tens e_p</math> so that <math>e_{np}</math> is the (doubly indexed) sequence of complex numbers given by <math>e_{npij} = \delta_{ni}\delta_{pj}</math> then <math>(e_{np})</math> is a hilbertian basis of <math>H\tens H</math>: the sequence <math>x=(x_{np})</math> may be written: |
+ | 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: |

− | : <math>x = \sum_{n,p\in\mathbb{N}}x_{np}\,e_{np} |
||

− | = \sum_{n,p\in\mathbb{N}}x_{np}\,e_n\tens e_p</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> |
||

+ | |||

+ | Furthermore the system of vectors <math>(e_{np})</math> is a hilbertian basis of <math>H\tens H</math>: the sequence <math>x=(x_{np})_{n,p\in\mathbb{N}}</math> may be written: |
||

+ | : <math>x = \sum_{n,p\in\mathbb{N}}x_{np}\,e_{np} |
||

+ | = \sum_{n,p\in\mathbb{N}}x_{np}\,e_n\tens e_p</math>. |
||

+ | |||

+ | == An algebra isomorphism == |
||

+ | |||

+ | Being both separable Hilbert spaces, <math>H</math> and <math>H\tens H</math> 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 <math>(n,p)\mapsto\langle n,p\rangle</math>. For example set <math>\langle n,p\rangle = 2^n(2p+1) - 1</math>. |
||

+ | |||

+ | {{Remark| |
||

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

+ | }} |
||

+ | |||

+ | This bijection can be extended into a Hilbert space isomorphism <math>\Phi:H\tens H\rightarrow H</math> by defining: |
||

+ | : <math>e_n\tens e_p = e_{np} \mapsto e_{\langle n,p\rangle}</math>. |
||

+ | |||

+ | Now given an operator <math>u</math> on <math>H</math> we define the operator <math>!u</math> on <math>H</math> by: |
||

+ | : <math>!u(e_{\langle n,p\rangle}) = \Phi(e_n\tens u(e_p))</math>. |
||

+ | |||

+ | {{Remark| |
||

+ | The operator <math>!u</math> is defined by: |
||

+ | : <math>!u = \Phi\circ (1\tens u)\circ \Phi^{-1}</math> |
||

+ | where <math>1\tens u</math> denotes the operator on <math>H\tens H</math> defined by <math>(1\tens u)(x\tens y) = x\tens u(y)</math> for any <math>x,y</math> in <math>H</math>. However this notation must not be confused with the [[GoI for MELL: the *-autonomous structure#The tensor rule|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 <math>u</math> and <math>v</math> we have: |
||

+ | * <math>!u!v = {!(uv)}</math>; |
||

+ | * <math>!(u^*) = (!u)^*</math>. |
||

+ | |||

+ | Due to the fact that <math>\Phi</math> is an isomorphism ''onto'' we also have <math>!1=1</math>; this however will not be used. |
||

+ | |||

+ | We therefore have that <math>!</math> is a morphism on <math>\mathcal{B}(H)</math>; 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 <math>u = u_\varphi</math> is a <math>p</math>-isometry generated by the partial permutation <math>\varphi</math> then we have: |
||

+ | : <math>!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}</math>. |
||

+ | Thus <math>!u</math> is itself a <math>p</math>-isometry and the proof space is stable under the copying iso. |

## Revision as of 20:26, 5 June 2010

# The tensor product of Hilbert spaces

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:

- .

Recall that is the canonical hilbertian basis of . 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.