冪対象に関する定理
定理 を示す
① 射の定義
評価写像を使った以下の図式が可換である。
また、以下の図式も可換である。
次に、2つの評価写像
と、以下の2つの可換図式を使って
2つの射
を定義する。
ここで、以下を可換にする唯一の射をと定義する。
すなわち、
が成り立つ。
② 射の定義
まず、以下の可換図式が成り立つ。
評価写像, を使った次の2つの図式も可換。
ここで、以下を可換にする唯一の射をと定義する。
すなわち、
が成り立つ。
射を以下の可換図式で定義する。
すなわち、
が成り立つ。
③ の計算
①の最後の2つの式の両辺に、右からを掛ける。
これら2つの式から、以下の可換図式が成り立つことがわかる。
積の普遍性から、2つの式
を示せば、
が言える。
②の最後の3つの式から
がわかる。
①の3番目、4番目の図式から
が成り立つので、代入して
評価写像がmonomorphismであることを使うと、上記2つの式から
が成り立つことがわかり、
が示せた。
④ の計算
可換図式
が成り立つこと、すなわち
を示せば
が言える。
の右からを掛けて
この式の左辺がであることを示す。
②の最初の式の右からを掛けて
①の最後の式から
①の3番目の図から
★
②の2番目の式の右からを掛けて
①の最後の式から
①の4番目の図から
★
★から、以下の図式において、が成り立つ。
よって、が示せた。
おまけ 可換図式を書くのに使ったtexソース
\documentclass[12pt]{ujarticle} \usepackage{amsmath,amsfonts,amsthm,amssymb,amscd} \usepackage[all]{xy} \def\objectstyle{\displaystyle} \begin{document} \[ \xymatrix@!C=150pt{ T\times (Y_1\times Y_2)^T \ar[r]^{1_T\times 1_{(Y_1\times Y_2)^T}} \ar[rd]_{e1} & T\times (Y_1\times Y_2)^T \ar[d]^{e1} \\ & Y_1\times Y_2 } \] \[ \xymatrix{ & T \times (Y_1 \times Y_2)^T \ar[ld]_{p_{Y_1} \circ e1} \ar@{.>}[d]^{e1} \ar[rd]^{p_{Y_2} \circ e1} & \\ Y_1 & Y_1 \times Y_2 \ar[l]_{p_{Y_1}} \ar[r]^{p_{Y_2}} & Y_2 } \] \[ \xymatrix@!C=150pt{ T \times (Y_1 \times Y_2)^T \ar[rd]_{p_{Y_1} \circ e1} \ar[r]^{1_T \times \widetilde{p_{Y_1} \circ e1}} & T \times Y_1^T \ar[d]^{e2} \\ & Y_1 } \] \[ \xymatrix@!C=150pt{ T \times (Y_1 \times Y_2)^T \ar[rd]_{p_{Y_2} \circ e1} \ar[r]^{1_T \times \widetilde{p_{Y_2} \circ e1}} & T \times Y_2^T \ar[d]^{e3} \\ & Y_2 } \] \[ \xymatrix{ & (Y_1 \times Y_2)^T \ar[ld]_{\widetilde{p_{Y_1} \circ e1}} \ar@{.>}[d]^{h} \ar[rd]^{\widetilde{p_{Y_2} \circ c1}} & \\ Y_1^T & Y_1^T \times Y_2^T \ar[l]_{p_{Y_1^T}} \ar[r]^{p_{Y_2^T}} & Y_2^T } \] \[ \xymatrix@!C=100pt{ & Y_1^T \times Y_2^T \ar[ld]_{p_{Y_1^T}} \ar@{.>}[d]^{1_{Y_1^T \times Y_2^T}} \ar[rd]^{p_{Y_2^T}} & \\ Y_1^T & Y_1^T \times Y_2^T \ar[l]_{p_{Y_1^T}} \ar[r]^{p_{Y_2^T}} & Y_2^T } \] \[ \xymatrix@!C=150pt{ T \times (Y_1^T \times Y_2^T) \ar[rd]_{e2 \circ (1_T \times p_{Y_1^T})} \ar[r]^{1_T \times p_{Y_1^T}} & T \times Y_1^T \ar[d]^{e2} \\ & Y_1 } \] \[ \xymatrix@!C=150pt{ T \times (Y_1^T \times Y_2^T) \ar[rd]_{e3 \circ (1_T \times p_{Y_2^T})} \ar[r]^{1_T \times p_{Y_2^T}} & T \times Y_2^T \ar[d]^{e3} \\ & Y_2 } \] \[ \xymatrix{ & T \times (Y_1^T \times Y_2^T) \ar[ld]_{e2 \circ (1_T \times p_{Y_1^T})} \ar@{.>}[d]^{g} \ar[rd]^{e3 \circ (1_T \times p_{Y_2^T})} & \\ Y_1 & Y_1 \times Y_2 \ar[l]_{p_{Y_1}} \ar[r]^{p_{Y_2}} & Y_2 } \] \[ \xymatrix@!C=150pt{ T \times (Y_1^T \times Y_2^T) \ar[rd]_{g} \ar[r]^{1_T \times \widetilde{g}} & T \times (Y_1 \times Y_2)^T \ar[d]^{e1} \\ & Y_1 \times Y_2 } \] \[ \xymatrix{ & Y_1^T \times Y_2^T \ar[ld]_{\widetilde{p_{Y_1} \circ e1} \circ \widetilde{g}} \ar@{.>}[d]^{h \circ \widetilde{g}} \ar[rd]^{\widetilde{p_{Y_2} \circ e1} \circ \widetilde{g}} & \\ Y_1^T & Y_1^T \times Y_2^T \ar[l]_{p_{Y_1^T}} \ar[r]^{p_{Y_2^T}} & Y_2^T } \] \[ \xymatrix{ T \times (Y_1 \times Y_2)^T \ar[rrd]_{e1?} \ar[r]^{1_T \times h} & T \times (Y_1^T \times Y_2^T) \ar[r]^{1_T \times \widetilde{g}} & T \times (Y_1 \times Y_2)^T \ar[d]^{e1} \\ & & Y_1 \times Y_2 } \] \[ \xymatrix@!C=100pt{ & T \times (Y_1 \times Y_2)^T \ar[ld]_{p_{Y_1} \circ e1} \ar@{.>}[d]^{e1 = g \circ (1_T \times h)} \ar[rd]^{p_{Y_2} \circ e1} & \\ Y_1 & Y_1 \times Y_2 \ar[l]_{p_{Y_1}} \ar[r]^{p_{Y_2}} & Y_2 } \] \end{document}