Revision as of 20:26, 5 June 2010

The tensor product of Hilbert spaces

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

∑	\| x_np \| ²
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}}$ .

Recall that $(e_k)_{k\in\mathbb{N}}$ is the canonical hilbertian basis of $H=\ell^2(\mathbb{N})$ . We define: $e_{np} = e_n\tens e_p$ so that $e n p$ is the sequence $(e_{npij})_{i,j\in\mathbb{N}}$ of complex numbers given by $e n p i j = δ n i δ p j$ . 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 n p)$ 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 $p p * + q q * = 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 = !(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 $\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.

@@ Line 1: / Line 1: @@
 = 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>.
@@ Line 7: / Line 7: @@
 : <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) =
   \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.

GoI for MELL: exponentials

Revision as of 20:26, 5 June 2010

The tensor product of Hilbert spaces

An algebra isomorphism

Interpretation of exponentials

Views

Personal tools

Navigation

Search

Tools