http://llwiki.ens-lyon.fr/mediawiki/index.php?title=GoI_for_MELL:_exponentials&feed=atom&action=history
GoI for MELL: exponentials - Revision history
2024-03-28T15:42:33Z
Revision history for this page on the wiki
MediaWiki 1.19.20+dfsg-0+deb7u3
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=GoI_for_MELL:_exponentials&diff=487&oldid=prev
Laurent Regnier: definition of type !A
2010-11-17T11:29:15Z
<p>definition of type !A</p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 11:29, 17 November 2010</td>
</tr><tr>
<td colspan="2" class="diff-lineno">Line 21:</td>
<td colspan="2" class="diff-lineno">Line 21:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>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.</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>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.</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>We fix, once for all, a bijection from couples of natural numbers to natural<span class="diffchange diffchange-inline"> 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>.</span></div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>We fix, once for all, a bijection from couples of natural numbers to natural</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>numbers that we will denote by <math>(n,p)\mapsto\langle n,p\rangle</math>. For</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>example set <math>\langle n,p\rangle = 2^n(2p+1) - 1</math>. Conversely, given</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div><math>n\in\mathbb{N}</math> we denote by <math>n_{(1)}</math> and</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div><math>n_{(2)}</math> the unique integers such that <math>\langle n_{(1)},</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>n_{(2)}\rangle = n</math>.</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>{{Remark|</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>{{Remark|</div></td>
</tr>
<tr>
<td colspan="2" class="diff-lineno">Line 51:</td>
<td colspan="2" class="diff-lineno">Line 51:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>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:</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>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:</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <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>.</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <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>.</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>Thus <math>!<span class="diffchange diffchange-inline">u</span></math> is itself a <math>p</math>-isometry <span class="diffchange diffchange-inline">and</span> <span class="diffchange diffchange-inline">the proof space is stable under</span> the<span class="diffchange diffchange-inline"> copying iso.</span></div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>Thus <math>!<span class="diffchange diffchange-inline">u_\varphi</span></math> is itself a <math>p</math>-isometry <span class="diffchange diffchange-inline">generated</span> <span class="diffchange diffchange-inline">by</span> the</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>Given a type <math>A</math> we define the type <math>!A</math> by:</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>: <math>!A = \{!u, u\in A\}\biorth</math></div></td>
</tr>
</table>
Laurent Regnier
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=GoI_for_MELL:_exponentials&diff=486&oldid=prev
Laurent Regnier: style
2010-11-17T10:55:50Z
<p>style</p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 10:55, 17 November 2010</td>
</tr><tr>
<td colspan="2" class="diff-lineno">Line 1:</td>
<td colspan="2" class="diff-lineno">Line 1:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>= The tensor product of Hilbert spaces =</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>= The tensor product of Hilbert spaces =</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><span class="diffchange diffchange-inline">The</span> <span class="diffchange diffchange-inline">space</span> <span class="diffchange diffchange-inline"><math>H\tens</span> <span class="diffchange diffchange-inline">H</math></span> <span class="diffchange diffchange-inline">is</span> the <span class="diffchange diffchange-inline">collection</span> <span class="diffchange diffchange-inline">of sequences</span> <math>(<span class="diffchange diffchange-inline">x_{np})_{n,p\in</span>\mathbb{N}<span class="diffchange diffchange-inline">}</span></math> <span class="diffchange diffchange-inline">of</span> <span class="diffchange diffchange-inline">complex</span> <span class="diffchange diffchange-inline">numbers</span> <span class="diffchange diffchange-inline">such</span> <span class="diffchange diffchange-inline">that:</span> <math>\<span class="diffchange diffchange-inline">sum_</span>{<span class="diffchange diffchange-inline">n,p</span>}<span class="diffchange diffchange-inline">|x_{np</span>}<span class="diffchange diffchange-inline">|^2</span></math><span class="diffchange diffchange-inline"> converges</span>.<span class="diffchange diffchange-inline"> The scalar product is defined just as before:</span></div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div><span class="diffchange diffchange-inline">Recall</span> <span class="diffchange diffchange-inline">that</span> <span class="diffchange diffchange-inline">we</span> <span class="diffchange diffchange-inline">work</span> <span class="diffchange diffchange-inline">in</span> the <span class="diffchange diffchange-inline">Hilbert</span> <span class="diffchange diffchange-inline">space</span> <math><span class="diffchange diffchange-inline">H=\ell^2</span>(\mathbb{N}<span class="diffchange diffchange-inline">)</span></math> <span class="diffchange diffchange-inline">endowed</span> <span class="diffchange diffchange-inline">with</span> <span class="diffchange diffchange-inline">its</span> <span class="diffchange diffchange-inline">canonical</span> <span class="diffchange diffchange-inline">hilbertian basis denoted by</span> <math><span class="diffchange diffchange-inline">(e_k)_{k</span>\<span class="diffchange diffchange-inline">in\mathbb</span>{<span class="diffchange diffchange-inline">N</span>}}</math>.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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:</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}</math>.</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}</math>.</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-lineno">Line 7:</td>
<td colspan="2" class="diff-lineno">Line 7:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}</math>.</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}</math>.</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><span class="diffchange diffchange-inline">Recall that <math>(e_k)_{k\in\mathbb{N}}</math> is the canonical hilbertian basis of <math>H=\ell^2(\mathbb{N})</math>. </span>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:</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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:</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>x\tens y = \left(\sum_n x_ne_n\right)\tens\left(\sum_p y_pe_p\right) = </div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>x\tens y = \left(\sum_n x_ne_n\right)\tens\left(\sum_p y_pe_p\right) = </div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> \sum_{n,p} x_ny_p\, e_n\tens e_p = \sum_{n,p} x_ny_p\,e_{np}</math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> \sum_{n,p} x_ny_p\, e_n\tens e_p = \sum_{n,p} x_ny_p\,e_{np}</math></div></td>
</tr>
</table>
Laurent Regnier
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=GoI_for_MELL:_exponentials&diff=485&oldid=prev
Laurent Regnier: The copying iso
2010-06-05T18:26:05Z
<p>The copying iso</p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 18:26, 5 June 2010</td>
</tr><tr>
<td colspan="2" class="diff-lineno">Line 1:</td>
<td colspan="2" class="diff-lineno">Line 1:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>= The tensor product of Hilbert spaces =</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>= The tensor product of Hilbert spaces =</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><span class="diffchange diffchange-inline">Recall that <math>(e_k)_{k\in\mathbb{N}}</math> is the canonical basis of <math>H=\ell^2(\mathbb{N})</math>. </span>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:</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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:</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}</math>.</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}</math>.</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-lineno">Line 7:</td>
<td colspan="2" class="diff-lineno">Line 7:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}</math>.</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}</math>.</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><span class="diffchange diffchange-inline">In</span> <span class="diffchange diffchange-inline">particular</span> <span class="diffchange diffchange-inline">if</span> <span class="diffchange diffchange-inline">we</span> define: <math>e_{np} = e_n\tens e_p</math> so that <math>e_{np}</math> is the <span class="diffchange diffchange-inline">(doubly</span> <span class="diffchange diffchange-inline">indexed</span>)<span class="diffchange diffchange-inline"> sequence</span> of complex numbers given by <math>e_{npij} = \delta_{ni}\delta_{pj}</math> <span class="diffchange diffchange-inline">then</span> <span class="diffchange diffchange-inline"><math>(e_{np})</math> is a hilbertian basis</span> of <span class="diffchange diffchange-inline"><math>H\tens</span> <span class="diffchange diffchange-inline">H</math>: the sequence <math>x=(x_{np})</math> may be</span> <span class="diffchange diffchange-inline">written</span>:</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div><span class="diffchange diffchange-inline">Recall</span> <span class="diffchange diffchange-inline">that</span> <span class="diffchange diffchange-inline"><math>(e_k)_{k\in\mathbb{N}}</math></span> <span class="diffchange diffchange-inline">is the canonical hilbertian basis of <math>H=\ell^2(\mathbb{N})</math>. We</span> define: <math>e_{np} = e_n\tens e_p</math> so that <math>e_{np}</math> is the <span class="diffchange diffchange-inline">sequence</span> <span class="diffchange diffchange-inline"><math>(e_{npij}</span>)<span class="diffchange diffchange-inline">_{i,j\in\mathbb{N}}</math></span> of complex numbers given by <math>e_{npij} = \delta_{ni}\delta_{pj}</math><span class="diffchange diffchange-inline">.</span> <span class="diffchange diffchange-inline">By</span> <span class="diffchange diffchange-inline">bilinearity</span> of <span class="diffchange diffchange-inline">tensor</span> <span class="diffchange diffchange-inline">we</span> <span class="diffchange diffchange-inline">have</span>:</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>: <math>x = \sum_{n,p\in\mathbb{N}}x_{np}\,e_{np}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> = \sum_{n,p\in\mathbb{N}}x_{np}\,e_n\tens e_p</math>. </div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>By bilinearity of tensor we have:</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>x\tens y = \left(\sum_n x_ne_n\right)\tens\left(\sum_p y_pe_p\right) = </div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>x\tens y = \left(\sum_n x_ne_n\right)\tens\left(\sum_p y_pe_p\right) = </div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> \sum_{n,p} x_ny_p\, e_n\tens e_p = \sum_{n,p} x_ny_p\,e_{np}</math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> \sum_{n,p} x_ny_p\, e_n\tens e_p = \sum_{n,p} x_ny_p\,e_{np}</math></div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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:</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>: <math>x = \sum_{n,p\in\mathbb{N}}x_{np}\,e_{np}</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> = \sum_{n,p\in\mathbb{N}}x_{np}\,e_n\tens e_p</math>.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>== An algebra isomorphism ==</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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>.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>{{Remark|</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>}}</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>This bijection can be extended into a Hilbert space isomorphism <math>\Phi:H\tens H\rightarrow H</math> by defining:</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>: <math>e_n\tens e_p = e_{np} \mapsto e_{\langle n,p\rangle}</math>.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>Now given an operator <math>u</math> on <math>H</math> we define the operator <math>!u</math> on <math>H</math> by:</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>: <math>!u(e_{\langle n,p\rangle}) = \Phi(e_n\tens u(e_p))</math>.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>{{Remark|</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>The operator <math>!u</math> is defined by:</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>: <math>!u = \Phi\circ (1\tens u)\circ \Phi^{-1}</math></div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>}}</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>One can check that given two operators <math>u</math> and <math>v</math> we have:</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>* <math>!u!v = {!(uv)}</math>;</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>* <math>!(u^*) = (!u)^*</math>.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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''.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>== Interpretation of exponentials ==</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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:</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>: <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>.</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>Thus <math>!u</math> is itself a <math>p</math>-isometry and the proof space is stable under the copying iso.</div></td>
</tr>
</table>
Laurent Regnier
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=GoI_for_MELL:_exponentials&diff=484&oldid=prev
Laurent Regnier: /* The tensor product of Hilbert spaces */ presentation
2010-06-05T10:20:44Z
<p><span dir="auto"><span class="autocomment">The tensor product of Hilbert spaces: </span> presentation</span></p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 10:20, 5 June 2010</td>
</tr><tr>
<td colspan="2" class="diff-lineno">Line 1:</td>
<td colspan="2" class="diff-lineno">Line 1:</td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>= The tensor product of Hilbert spaces<span class="diffchange diffchange-inline"></math></span> =</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>= The tensor product of Hilbert spaces =</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>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:</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>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:</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}</math>.</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}</math>.</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>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:</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>: <math>e_{ijnp} = \delta_{in}\delta_{jp}</math> (all terms are null but the one at index <math>(i,j)</math> which is 1).</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>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:</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>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:</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}</math>.</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>: <math>x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}</math>.</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>In particular we <span class="diffchange diffchange-inline">have</span>: <math>e_{<span class="diffchange diffchange-inline">ij</span>} = <span class="diffchange diffchange-inline">e_i</span>\tens <span class="diffchange diffchange-inline">e_j</span></math> <span class="diffchange diffchange-inline">and</span> <span class="diffchange diffchange-inline">we</span> <span class="diffchange diffchange-inline">can</span> <span class="diffchange diffchange-inline">write</span>:</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>In particular<span class="diffchange diffchange-inline"> if</span> we <span class="diffchange diffchange-inline">define</span>: <math>e_{<span class="diffchange diffchange-inline">np</span>} = <span class="diffchange diffchange-inline">e_n</span>\tens <span class="diffchange diffchange-inline">e_p</span></math> <span class="diffchange diffchange-inline">so</span> <span class="diffchange diffchange-inline">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</span> <span class="diffchange diffchange-inline">be</span> <span class="diffchange diffchange-inline">written</span>:</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>: <math>x<span class="diffchange diffchange-inline">\tens y</span> = \<span class="diffchange diffchange-inline">left(</span>\<span class="diffchange diffchange-inline">sum_n x_ne_n</span>\<span class="diffchange diffchange-inline">right)</span>\<span class="diffchange diffchange-inline">left(\sum_p y_pe_p\right) = </span></div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>: <math>x = \<span class="diffchange diffchange-inline">sum_{n,p</span>\<span class="diffchange diffchange-inline">in</span>\<span class="diffchange diffchange-inline">mathbb{N}}x_{np}</span>\<span class="diffchange diffchange-inline">,e_{np}</span></div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> <span class="diffchange diffchange-inline">\sum_{n,p}</span> <span class="diffchange diffchange-inline">x_ny_p</span> <span class="diffchange diffchange-inline">e_n\tens</span> <span class="diffchange diffchange-inline">e_p</span> = \sum_{n,p}<span class="diffchange diffchange-inline"> x_ny_p e_</span>{np}</math></div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> <span class="diffchange diffchange-inline"> </span> = \sum_{n,p<span class="diffchange diffchange-inline">\in\mathbb{N</span>}<span class="diffchange diffchange-inline">}x_</span>{np}<span class="diffchange diffchange-inline">\,e_n\tens e_p</span></math><span class="diffchange diffchange-inline">. </span></div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>By bilinearity of tensor we have:</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>: <math>x\tens y = \left(\sum_n x_ne_n\right)\tens\left(\sum_p y_pe_p\right) = </div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> \sum_{n,p} x_ny_p\, e_n\tens e_p = \sum_{n,p} x_ny_p\,e_{np}</math></div></td>
</tr>
</table>
Laurent Regnier
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=GoI_for_MELL:_exponentials&diff=483&oldid=prev
Laurent Regnier: Creation of the page : generalities on Hilbert spaces tensor product
2010-05-25T08:28:09Z
<p>Creation of the page : generalities on Hilbert spaces tensor product</p>
<p><b>New page</b></p><div>= The tensor product of Hilbert spaces</math> =<br />
<br />
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:<br />
: <math>\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}</math>.<br />
<br />
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:<br />
: <math>e_{ijnp} = \delta_{in}\delta_{jp}</math> (all terms are null but the one at index <math>(i,j)</math> which is 1).<br />
<br />
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:<br />
: <math>x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}</math>.<br />
<br />
In particular we have: <math>e_{ij} = e_i\tens e_j</math> and we can write:<br />
: <math>x\tens y = \left(\sum_n x_ne_n\right)\left(\sum_p y_pe_p\right) = <br />
\sum_{n,p} x_ny_p e_n\tens e_p = \sum_{n,p} x_ny_p e_{np}</math></div>
Laurent Regnier