Latest revision as of 12:29, 17 November 2010

[edit] The tensor product of Hilbert spaces

Recall that we work in the Hilbert space $H=\ell^2(\mathbb{N})$ endowed with its canonical hilbertian basis denoted by $(e_k)_{k\in\mathbb{N}}$ .

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}}$ .

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

[edit] 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$ . Conversely, given $n\in\mathbb{N}$ we denote by $n (1)$ and $n (2)$ the unique integers such that $\langle n_{(1)}, n_{(2)}\rangle = n$ .

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.

[edit] 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_\varphi$ is itself a $p$ -isometry generated by the partial permutation $!\varphi:n\mapsto \langle n_{(1)}, \varphi(n_{(2)})\rangle$ , which shows that the proof space is stable under the copying iso.

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

$!A = \{!u, u\in A\}\biorth$

@@ Line 1: / Line 1: @@
-= The tensor product of Hilbert spaces</math> =
+= 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:
+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>.
-The canonical basis of <math>H\tens H</math> is denoted <math>(e_{ij})_{i,j\in\mathbb{N}}</math> where <math>e_{ij}</math> is the (doubly indexed) sequence <math>(e_{ijnp})_{n,p\in\mathbb{N}}</math> defined by:
-: <math>e_{ijnp} = \delta_{in}\delta_{jp}</math> (all terms are null but the one at index <math>(i,j)</math> which is 1).
 If <math>x = (x_n)_{n\in\mathbb{N}}</math> and <math>y = (y_p)_{p\in\mathbb{N}}</math> are vectors in <math>H</math> then their tensor is the sequence:
 : <math>x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}</math>.
-In particular we have: <math>e_{ij} = e_i\tens e_j</math> and we can write:
+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)\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>. Conversely, given
+<math>n\in\mathbb{N}</math> we denote by <math>n_{(1)}</math> and
+<math>n_{(2)}</math> the unique integers such that <math>\langle n_{(1)},
+n_{(2)}\rangle = n</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_\varphi</math> is itself a <math>p</math>-isometry generated by the
+partial permutation <math>!\varphi:n\mapsto \langle n_{(1)}, \varphi(n_{(2)})\rangle</math>, which shows that the proof space is stable under the copying iso.
+Given a type <math>A</math> we define the type <math>!A</math> by:
+: <math>!A = \{!u, u\in A\}\biorth</math>

GoI for MELL: exponentials

Latest revision as of 12:29, 17 November 2010

[edit] The tensor product of Hilbert spaces

[edit] An algebra isomorphism

[edit] Interpretation of exponentials

Views

Personal tools

Navigation

Search

Tools