双線型空間の普遍性
from そこそこまあまあ精密に読む『ベーシック圏論 普遍性からの速習コース』
双線型空間の普遍性
$ \forall K\in{\cal B}\forall U,V\in{\cal L}(K)に対し、$ T\in{\cal L}(K)と「普遍的な双線型写像」$ b:\underline U\times\underline V\to\underline Tが存在する
$ bが普遍的であることは、以下と同値である
$ \forall W\in{\cal L}(K)\forall f:\underline U\times\underline V\to\underline W\exists!\bar f:\underline T\to\underline W.f=\bar f\circ b\land\bar f\text{は線型写像である}
https://scrapbox.io/files/65c6ea2fd411da00259aa3e9.svg
$ bにより、$ \underline U\times\underline V\to\underline Wから$ \underline T\to\underline Wへの一対一対応を構成できる
記法は線型空間の略記を参照
fを双線型写像に絞ると、bがtensor積になるtakker.icon
https://manabitimes.jp/math/1845#3-4
$ \forall K\in{\cal B}\forall U,V\in{\cal L}(K)\forall b:\underline U\times\underline V\to\underline T\forall b':\underline U\times\underline V\to\underline T'.b,b'\text{が普遍性を満たす}\implies T\cong T'
ここで
$ T\cong T':\iff\exist\phi:T\to T'.\phi\text{は同型写像である}
同型写像は集合論の場合全単射と同一だと思っていい
同型写像は全単射があるだけではなくて構造を維持する写像であることが必要
証明
$ \forall K\in{\cal B}\forall U,V\in{\cal L}(K)\forall b:\underline U\times\underline V\to\underline T\forall b':\underline U\times\underline V\to\underline T'にて
$ b,b'\text{が普遍性を満たす}
$ \iff\forall W\in{\cal L}(K).
https://scrapbox.io/files/65c6ee651d64320024a9b569.svg
$ \implies
https://scrapbox.io/files/65c6ee7814f8450024d79665.svg
左図式の$ Wに$ T'を、右図式の$ Wに$ Tを代入した
あとで使うので$ bの普遍性は残してある
$ \iff\forall W\in{\cal L}(K)\exists! \bar f,\bar f'\text{ are linear}.
https://scrapbox.io/files/65c6ee9a73a5a20025f2a291.svg
図式を合体しただけ
記号がかぶらないよう、右図式の$ \bar fを$ \bar f''に変えた
$ \implies
https://scrapbox.io/files/65c6eeb33244aa0024786647.svg
左図式の上矢印を合成し、真ん中の$ b'を削った
右に恒等写像$ {\rm id}_T:T\to Tの図式を加えた
これは恒等式なので常に成り立つ
$ \implies\exists! \bar f,\bar f'\text{ are linear}.\bar f'\circ\bar f={\rm id}_T
ここが証明の核心
真ん中の図式即ち$ bの普遍性が示す一意性より、左図式の点線上の写像$ \bar f'\circ fと右図式の点線上の写像$ {\rm id}_Tが等しくなる
$ \implies \exist f:T\to T'.f\text{は同型写像である}
さっきも書いたが、同型写像は全単射と等しいはず
$ \iff T\cong T'
$ \underline{\therefore\forall K\in{\cal B}\forall U,V\in{\cal L}(K)\forall b:\underline U\times\underline V\to\underline T\forall b':\underline U\times\underline V\to\underline T'.b,b'\text{が普遍性を満たす}\implies T\cong T'\quad}_\blacksquare
この定理から、どのようにテンソル積を定義しても、実質同じだとわかる
テンソル積を、基底を使わずに定義できたということ
数カ月ぶりにこのページに書き込んだが、当時はこの定理の意味を全然わかってなかったのだと思う
わかってなかったということがわかるのも成長か
code:eg0.6.tikz(tex)
\begin{document}
\begin{tikzpicture}auto,->
\node (S) at (2,0) {$\underbar U\times\underbar V$};
\node (V) at (0,0) {$\underbar T$};
\node (W) at (0,2) {$\underbar W$};
\draw (S) -- node {$b$} (V);
\draw (S) -- nodeswap {$\forall f$} (W);
\drawdashed (V) -- node {$\exists! \bar{f}\textrm{ is linear}$} (W);
\end{tikzpicture}
\end{document}
code:lemma0.7.tikz(tex)
\begin{document}
\begin{tikzpicture}auto,->
\node (S) at (2,0) {$\underbar U\times\underbar V$};
\node (V) at (0,0) {$\underbar T$};
\node (W) at (0,2) {$\underbar W$};
\draw (S) -- node {$b$} (V);
\draw (S) -- nodeswap {$\forall f$} (W);
\drawdashed (V) -- node {$\exists! \bar{f}\textrm{ is linear}$} (W);
\end{tikzpicture}
\begin{tikzpicture}auto,->
\node (S) at (2,0) {$\underbar U\times\underbar V$};
\node (V) at (0,0) {$\underbar T'$};
\node (W) at (0,2) {$\underbar W$};
\draw (S) -- node {$b'$} (V);
\draw (S) -- nodeswap {$\forall f$} (W);
\drawdashed (V) -- node {$\exists! \bar{f}\textrm{ is linear}$} (W);
\end{tikzpicture}
\end{document}
code:lemma0.7-2.tikz(tex)
\begin{document}
\begin{tikzpicture}auto,->
\node (S) at (2,0) {$\underbar U\times\underbar V$};
\node (V) at (0,0) {$\underbar T$};
\node (W) at (0,2) {$\underbar T'$};
\draw (S) -- node {$b$} (V);
\draw (S) -- nodeswap {$b'$} (W);
\drawdashed (V) -- node {$\exists! \bar{f}\textrm{ is linear}$} (W);
\end{tikzpicture}
\begin{tikzpicture}auto,->
\node (S) at (2,0) {$\underbar U\times\underbar V$};
\node (V) at (0,0) {$\underbar T'$};
\node (W) at (0,2) {$\underbar T$};
\draw (S) -- node {$b'$} (V);
\draw (S) -- nodeswap {$b$} (W);
\drawdashed (V) -- node {$\exists! \bar{f}\textrm{ is linear}$} (W);
\end{tikzpicture}
\begin{tikzpicture}auto,->
\node (S) at (2,0) {$\underbar U\times\underbar V$};
\node (V) at (0,0) {$\underbar T$};
\node (W) at (0,2) {$\underbar W$};
\draw (S) -- node {$b$} (V);
\draw (S) -- nodeswap {$\forall f$} (W);
\drawdashed (V) -- node {$\exists! \bar{f}\textrm{ is linear}$} (W);
\end{tikzpicture}
\(\textrm{.for }\forall W\in{\cal L}(K)\)
\end{document}
code:lemma0.7-3.tikz(tex)
\begin{document}
\begin{tikzpicture}auto,->
\node (UV) at (2,0) {$\underbar U\times\underbar V$};
\node (T) at (0,-2) {$\underbar T$};
\node (T') at (0,0) {$\underbar T'$};
\node (T2) at (0,2) {$\underbar T$};
\draw (UV) -- node {$b$} (T);
\draw (UV) -- nodeswap {$b$} (T2);
\draw (UV) -- nodeswap {$b'$} (T');
\drawdashed (T) -- node {$\bar f$} (T');
\drawdashed (T') -- node {$\bar f'$} (T2);
\end{tikzpicture}
\begin{tikzpicture}auto,->
\node (S) at (2,0) {$\underbar U\times\underbar V$};
\node (V) at (0,0) {$\underbar T$};
\node (W) at (0,2) {$\underbar W$};
\draw (S) -- node {$b$} (V);
\draw (S) -- nodeswap {$\forall f$} (W);
\drawdashed (V) -- node {$\exists! \bar f''\textrm{ is linear}$} (W);
\end{tikzpicture}
\end{document}
code:lemma0.7-4.tikz(tex)
\begin{document}
\begin{tikzpicture}auto,->
\node (UV) at (2,0) {$\underbar U\times\underbar V$};
\node (T) at (0,0) {$\underbar T$};
\node (T2) at (0,2) {$\underbar T$};
\draw (UV) -- node {$b$} (T);
\draw (UV) -- nodeswap {$b$} (T2);
\drawdashed (T) -- node {$\bar f'\circ\bar f$} (T2);
\end{tikzpicture}
\begin{tikzpicture}auto,->
\node (S) at (2,0) {$\underbar U\times\underbar V$};
\node (V) at (0,0) {$\underbar T$};
\node (W) at (0,2) {$\underbar W$};
\draw (S) -- node {$b$} (V);
\draw (S) -- nodeswap {$\forall f$} (W);
\drawdashed (V) -- node {$\exists! \bar f''\textrm{ is linear}$} (W);
\end{tikzpicture}
\begin{tikzpicture}auto,->
\node (UV) at (2,0) {$\underbar U\times\underbar V$};
\node (T) at (0,0) {$\underbar T$};
\node (T2) at (0,2) {$\underbar T$};
\draw (UV) -- node {$b$} (T);
\draw (UV) -- nodeswap {$b$} (T2);
\drawdashed (T) -- node {${\rm id}_T$} (T2);
\end{tikzpicture}
\end{document}