/villagepump/双線型空間の普遍性

generated at 2/11/2025, 7:09:45 AM
双線型空間の普遍性
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{は線型写像である}
bにより、\underline U\times\underline V\to\underline Wから\underline T\to\underline Wへの一対一対応を構成できる
記法は線型空間の略記を参照
fを双線型写像に絞ると、bがtensor積になる
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).
\implies
左図式のWにT'を、右図式のWにTを代入した
あとで使うのでbの普遍性は残してある
\iff\forall W\in{\cal L}(K)\exists! \bar f,\bar f'\text{ are linear}.
図式を合体しただけ
記号がかぶらないよう、右図式の\bar fを\bar f''に変えた
\implies
左図式の上矢印を合成し、真ん中の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

この定理から、どのようにテンソル積を定義しても、実質同じだとわかる
テンソル積を、基底を使わずに定義できたということ
数カ月ぶりにこのページに書き込んだが、当時はこの定理の意味を全然わかってなかったのだと思う
わかってなかったということがわかるのも成長か

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) -- node[swap] {$\forall f$} (W);
\draw[dashed] (V) -- node {$\exists! \bar{f}\textrm{ is linear}$} (W);
\end{tikzpicture}
\end{document}

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) -- node[swap] {$\forall f$} (W);
\draw[dashed] (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) -- node[swap] {$\forall f$} (W);
\draw[dashed] (V) -- node {$\exists! \bar{f}\textrm{ is linear}$} (W);
\end{tikzpicture}
\end{document}

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) -- node[swap] {$b'$} (W);
\draw[dashed] (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) -- node[swap] {$b$} (W);
\draw[dashed] (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) -- node[swap] {$\forall f$} (W);
\draw[dashed] (V) -- node {$\exists! \bar{f}\textrm{ is linear}$} (W);
\end{tikzpicture}
\(\textrm{.for }\forall W\in{\cal L}(K)\)
\end{document}

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) -- node[swap] {$b$} (T2);
\draw (UV) -- node[swap] {$b'$} (T');
\draw[dashed] (T) -- node {$\bar f$} (T');
\draw[dashed] (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) -- node[swap] {$\forall f$} (W);
\draw[dashed] (V) -- node {$\exists! \bar f''\textrm{ is linear}$} (W);
\end{tikzpicture}
\end{document}

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) -- node[swap] {$b$} (T2);
\draw[dashed] (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) -- node[swap] {$\forall f$} (W);
\draw[dashed] (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) -- node[swap] {$b$} (T2);
\draw[dashed] (T) -- node {${\rm id}_T$} (T2);
\end{tikzpicture}
\end{document}