数学: ていへんかけるたかさわるに

- 1 2 3 4 5 .. >>

2023年09月12日

数学: モナド $(T,\eta,\mu)$ 上の随伴の圏 $\mathbf{Adj}_T$

モナド ── 定義と随伴により引き起こされるモナド ,
随伴から導かれるモナドの例 ── maybe モナド
モナドから導かれる随伴 (1) ── Eilenberg-Moore 圏
モナドから導かれる随伴 (2) ── Kleisli 圏
モナド ── Kleisli 圏の例 (続き) の続き.

圏 $\mathrm{C}$ 上の与えられたモナド $(T,\eta,\mu)$ に対して, $T$ 上の随伴のなす圏 $\mathbf{Adj}_T$ を次のように定義する.
$\mathbf{Adj}_T$ の対象は, 随伴
\begin{equation*}
\DeclareMathOperator{\Aff}{Aff}
\DeclareMathOperator{\Ar}{Ar}
\DeclareMathOperator{\Arccos}{Arccos}
\DeclareMathOperator{\Arcsin}{Arcsin}
\DeclareMathOperator{\Arr}{Arr}
\DeclareMathOperator{\arr}{arr}
\DeclareMathOperator{\Aut}{Aut}
\DeclareMathOperator{\Auto}{Auto}
\DeclareMathOperator{\Axiom}{Axiom}
\DeclareMathOperator{\Bilin}{Bilin}
\DeclareMathOperator{\card}{card}
\DeclareMathOperator{\Catelem}{\int}
\DeclareMathOperator{\Cocone}{Cocone}
\DeclareMathOperator{\Cod}{cod}
\DeclareMathOperator{\Codomain}{cod}
\DeclareMathOperator{\Coin}{coin}
\DeclareMathOperator{\coker}{coker}
\DeclareMathOperator{\Colim}{colim}
\DeclareMathOperator{\comp}{comp}
\DeclareMathOperator{\Conf}{Conf}
\DeclareMathOperator{\Conj}{Conj}
\DeclareMathOperator{\Dom}{dom}
\DeclareMathOperator{\Domain}{dom}
\DeclareMathOperator{\Edge}{Edge}
\DeclareMathOperator{\Ev}{ev}
\DeclareMathOperator{\GCD}{gcd}
\DeclareMathOperator{\Gr}{Gr}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Id}{id}
\DeclareMathOperator{\IM}{Im}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\Ind}{ind}
\DeclareMathOperator{\INIT}{init}
\DeclareMathOperator{\iso}{iso}
\DeclareMathOperator{\LCM}{lcm}
\DeclareMathOperator{\Map}{Map}
\DeclareMathOperator{\mor}{arr}
\DeclareMathOperator{\Nat}{Nat}
\DeclareMathOperator{\Ob}{Ob}
\DeclareMathOperator{\ob}{ob}
\DeclareMathOperator{\ord}{ord}
\DeclareMathOperator{\Path}{Path}
\DeclareMathOperator{\PConf}{PConf}
\DeclareMathOperator{\Point}{Point}
\DeclareMathOperator{\Prob}{Prob}
\DeclareMathOperator{\RE}{Re}
\DeclareMathOperator{\Res}{res}
\DeclareMathOperator{\Sect}{Sect}
\DeclareMathOperator{\SF}{SF}
\DeclareMathOperator{\SkelCat}{sk}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Sq}{Sq}
\DeclareMathOperator{\Struct}{Struct}
\DeclareMathOperator{\Sub}{Sub}
\DeclareMathOperator{\Sym}{Sym}
\DeclareMathOperator{\TERM}{term}
\DeclareMathOperator{\Vertex}{Vert}
\newcommand{\Abs}[1]{\lvert{#1}\rvert}
\newcommand{\Bs}{\backslash}
\newcommand{\Cdot}{\,\cdot^{\mathrm{op}}}
\newcommand{\Comma}[2]{{{#1}\!\downarrow\!{#2}}}
\newcommand{\CommaCat}[2]{(#1/#2)}
\newcommand{\Complement}[1]{{\smash[t]{\mathstrut #1}}^{\mathrm{c}}}
\newcommand{\Emph}[1]{\textit{#1}}
\newcommand{\Eqclass}[4]{{#1#2#3}_{#4}}
\newcommand{\EqCls}[2]{{\left[#1\right]}_{#2}}
\newcommand{\Eqcls}[1]{\left[#1\right]}
\newcommand{\Expt}[2]{{\smash[t]{\mathstrut #1}}^{\mathstrut #2}}
\newcommand{\FnRest}[2]{{#1}|{#2}}
\newcommand{\Func}[2]{\mathrm{Func}(#1,#2)}
\newcommand{\g}{\varg}
\newcommand{\Inc}[2]{\mathrm{incl}\left(#1,#2\right)}
\newcommand{\Incl}[2]{\mathrm{incl}_{#1}^{#2}}
\newcommand{\InclArrow}[2]{\morphism(0,0)/>->/45<\0\,>[\Incl{#1}{#2} : {#1}\,\,`{#2};]}
\newcommand{\Ip}{\amalg}
\newcommand{\Lb}[1]{\mathrm{lb}(#1)}
\newcommand{\LH}{\mathrm{LH}}
\newcommand{\Lowerset}[1]{\downarrow\!\!{#1}}
\newcommand{\Leadsto}{\quad\leadsto\quad}
\newcommand{\Lrsquigarrow}{\quad\leftrightsquigarrow\quad}
\newcommand{\Mb}[1]{\mathbf{#1}}
\newcommand{\Mbb}[1]{\mathbb{#1}}
\newcommand{\Mi}[1]{\mathit{#1}}
\newcommand{\Mlb}[1]{\mathrm{mlb}(#1)}
\newcommand{\Mr}[1]{\mathrm{#1}}
\newcommand{\Ms}[1]{\mathscr{#1}}
\newcommand{\Mt}[1]{\mathtt{#1}}
\newcommand{\Mub}[1]{\mathrm{mub}(#1)}
\newcommand{\newinf}{\mathop{\mathrm{inf}\vphantom{\mathrm{sup}}}}
\newcommand{\newsup}{\mathop{\smash{\mathrm{sup}}}}
\newcommand{\Opp}[1]{#1^{\mathrm{op}}}
\newcommand{\Prj}[2]{\mathrm{proj}\left(#1,#2\right)}
\newcommand{\Proj}[2]{\mathrm{proj}^{#1}_{#2}}
\newcommand{\Pw}{\mathbf{P}}
\newcommand{\Rn}[1]{{\bmdefine{R}}^{#1}}
\newcommand{\q}{\hspace{1em}}
\newcommand{\qq}{\hspace{0.5em}}
\newcommand{\Rel}[1]{\langle{#1}\rangle}
\newcommand{\Rest}[2]{{#1}|{#2}}
\newcommand{\Slash}[1]{{\ooalign{\hfil/\hfil\crcr$#1$}}}
\newcommand{\SliCat}[2]{{#1}\,\big/\,{#2}}
\newcommand{\Src}{d^{0,\mathrm{op}}}
\newcommand{\ssqrt}[1]{\sqrt{\smash[b]{\mathstrut #1}}}
\newcommand{\Tgt}{d^{1,\mathrm{op}}}
\newcommand{\TwArCat}[1]{\mathrm{Tw}(#1)}
\newcommand{\Ub}[1]{\mathrm{ub}(#1)}
\newcommand{\Un}[1]{{1}_{#1}}
\newcommand{\Upperset}[1]{\uparrow\!\!{#1}}
\newcommand{\VectCat}[1]{#1 \mathchar`- \mathbf{Vect}}
\newcommand{\VS}{\vspace*{-1ex}}
\newcommand{\Wbar}[1]{\widebar{#1}}
\newcommand{\Ab}{\mathbf{Ab}}
\newcommand{\Adj}{\mathbf{Adj}}
\newcommand{\Affine}{\mathbf{Affine}}
\newcommand{\Ban}{\mathbf{Ban}}
\newcommand{\bbDelta}{\Delta\mkern-12mu\Delta}
\newcommand{\Card}{\mathbf{Card}}
\newcommand{\CAT}{\mathbf{CAT}}
\newcommand{\Cat}{\mathbf{Cat}}
\newcommand{\cgHaus}{\mathbf{cgHaus}}
\newcommand{\Ch}{\mathbf{Ch}}
\newcommand{\cHaus}{\mathbf{cHaus}}
\newcommand{\Cluster}{\mathbf{Cluster}}
\newcommand{\CMonoid}{\mathbf{CMonoid}}
\newcommand{\CRing}{\mathbf{CRing}}
\newcommand{\DirGraph}{\mathbf{DirGraph}}
\newcommand{\End}{\mathbf{End}}
\newcommand{\Euclid}{\mathbf{Euclid}}
\newcommand{\Field}{\mathbf{Field}}
\newcommand{\Fin}{\mathbf{Fin}}
\newcommand{\FinMetric}{\mathbf{FinMetric}}
\newcommand{\Four}{\mathbbm{4}}
\newcommand{\Graph}{\mathbf{Graph}}
\newcommand{\GrMod}{\mathbf{GrMod}}
\newcommand{\Grp}{\mathbf{Grp}}
\newcommand{\Group}{\mathbf{Group}}
\newcommand{\Groupoid}{\mathbf{Groupoid}}
\newcommand{\Haus}{\mathbf{Haus}}
\newcommand{\Htpy}{\mathbf{Htpy}}
\newcommand{\Man}{\mathbf{Man}}
\newcommand{\Mapsdown}{\rotatebox{270}{$\mapsto$}}
\newcommand{\Mapsup}{\rotatebox{90}{$\mapsto$}}
\newcommand{\Mat}{\mathbf{Mat}}
\newcommand{\Meas}{\mathbf{Meas}}
\newcommand{\Measure}{\mathbf{Measure}}
\newcommand{\Mod}{\mathbf{Mod}}
\newcommand{\Model}{\mathbf{Model}}
\newcommand{\Mon}{\mathbf{Mon}}
\newcommand{\Monoid}{\mathbf{Monoid}}
\newcommand{\oMega}{\bbomega}
\newcommand{\One}{\mymathbb{1}}
\newcommand{\Ord}{\mathrm{Ord}}
\newcommand{\PCluster}{\mathbf{PCluster}}
\newcommand{\POs}{\mathbf{Poset}}
\newcommand{\Poset}{\mathbf{Poset}}
\newcommand{\PROJ}{\mathbf{Proj}}
\newcommand{\Psh}{\mathbf{Psh}}
\newcommand{\Ring}{\mathbf{Ring}}
\newcommand{\Rng}{\mathbf{Rng}}
\newcommand{\SET}{\mathbf{SET}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\setmid}{\mathrel{}\middle|\mathrel{}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Shv}{\mathbf{Shv}}
\newcommand{\Three}{\mymathbb{3}}
\renewcommand{\Top}{\mathbf{Top}}
\newcommand{\Two}{\mymathbb{2}}
\newcommand{\Vect}{\mathbf{Vect}}
\newcommand{\Zero}{\mymathbb{0}}
\newcommand{\sA}{\mathscr{A}}
\newcommand{\sB}{\mathscr{B}}
\newcommand{\sC}{\mathscr{C}}
\newcommand{\sD}{\mathscr{D}}
\newcommand{\sE}{\mathscr{E}}
\newcommand{\sF}{\mathscr{F}}
\newcommand{\sG}{\mathscr{G}}
\newcommand{\sH}{\mathscr{H}}
\newcommand{\sI}{\mathscr{I}}
\newcommand{\sJ}{\mathscr{J}}
\newcommand{\sK}{\mathscr{K}}
\newcommand{\sL}{\mathscr{L}}
\newcommand{\sM}{\mathscr{M}}
\newcommand{\sN}{\mathscr{N}}
\newcommand{\sO}{\mathscr{O}}
\newcommand{\sP}{\mathscr{P}}
\newcommand{\sQ}{\mathscr{Q}}
\newcommand{\sR}{\mathscr{R}}
\newcommand{\sS}{\mathscr{S}}
\newcommand{\sT}{\mathscr{T}}
\newcommand{\sU}{\mathscr{U}}
\newcommand{\sV}{\mathscr{V}}
\newcommand{\sW}{\mathscr{W}}
\newcommand{\sX}{\mathscr{X}}
\newcommand{\sY}{\mathscr{Y}}
\newcommand{\sZ}{\mathscr{Z}}
\newcommand{\bfA}{\mathbf{A}}
\newcommand{\bfB}{\mathbf{B}}
\newcommand{\bfC}{\mathbf{C}}
\newcommand{\bfD}{\mathbf{D}}
\newcommand{\bfE}{\mathbf{E}}
\newcommand{\bfF}{\mathbf{F}}
\newcommand{\bfG}{\mathbf{G}}
\newcommand{\bfH}{\mathbf{H}}
\newcommand{\bfI}{\mathbf{I}}
\newcommand{\bfJ}{\mathbf{J}}
\newcommand{\bfK}{\mathbf{K}}
\newcommand{\bfL}{\mathbf{L}}
\newcommand{\bfM}{\mathbf{M}}
\newcommand{\bfN}{\mathbf{N}}
\newcommand{\bfO}{\mathbf{O}}
\newcommand{\bfP}{\mathbf{P}}
\newcommand{\bfQ}{\mathbf{Q}}
\newcommand{\bfR}{\mathbf{R}}
\newcommand{\bfS}{\mathbf{S}}
\newcommand{\bfT}{\mathbf{T}}
\newcommand{\bfU}{\mathbf{U}}
\newcommand{\bfV}{\mathbf{V}}
\newcommand{\bfW}{\mathbf{W}}
\newcommand{\bfX}{\mathbf{X}}
\newcommand{\bfY}{\mathbf{Y}}
\newcommand{\bfZ}{\mathbf{Z}}
\newcommand{\bfa}{\mathbf{a}}
\newcommand{\bfb}{\mathbf{b}}
\newcommand{\bfc}{\mathbf{c}}
\newcommand{\bfd}{\mathbf{d}}
\newcommand{\bfe}{\mathbf{e}}
\newcommand{\bff}{\mathbf{f}}
\newcommand{\bfg}{\mathbf{g}}
\newcommand{\bfh}{\mathbf{h}}
\newcommand{\bfi}{\mathbf{i}}
\newcommand{\bfj}{\mathbf{j}}
\newcommand{\bfk}{\mathbf{k}}
\newcommand{\bfl}{\mathbf{l}}
\newcommand{\bfm}{\mathbf{m}}
\newcommand{\bfn}{\mathbf{n}}
\newcommand{\bfo}{\mathbf{o}}
\newcommand{\bfp}{\mathbf{p}}
\newcommand{\bfq}{\mathbf{q}}
\newcommand{\bfr}{\mathbf{r}}
\newcommand{\bfs}{\mathbf{s}}
\newcommand{\bft}{\mathbf{t}}
\newcommand{\bfu}{\mathbf{u}}
\newcommand{\bfv}{\mathbf{v}}
\newcommand{\bfw}{\mathbf{w}}
\newcommand{\bfx}{\mathbf{x}}
\newcommand{\bfy}{\mathbf{y}}
\newcommand{\bfz}{\mathbf{z}}
\newcommand{\frA}{\mathfrak{A}}
\newcommand{\frB}{\mathfrak{B}}
\newcommand{\frC}{\mathfrak{C}}
\newcommand{\frD}{\mathfrak{D}}
\newcommand{\frE}{\mathfrak{E}}
\newcommand{\frF}{\mathfrak{F}}
\newcommand{\frG}{\mathfrak{G}}
\newcommand{\frH}{\mathfrak{H}}
\newcommand{\frI}{\mathfrak{I}}
\newcommand{\frJ}{\mathfrak{J}}
\newcommand{\frK}{\mathfrak{K}}
\newcommand{\frL}{\mathfrak{L}}
\newcommand{\frM}{\mathfrak{M}}
\newcommand{\frN}{\mathfrak{N}}
\newcommand{\frO}{\mathfrak{O}}
\newcommand{\frP}{\mathfrak{P}}
\newcommand{\frQ}{\mathfrak{Q}}
\newcommand{\frR}{\mathfrak{R}}
\newcommand{\frS}{\mathfrak{S}}
\newcommand{\frT}{\mathfrak{T}}
\newcommand{\frU}{\mathfrak{U}}
\newcommand{\frV}{\mathfrak{V}}
\newcommand{\frW}{\mathfrak{W}}
\newcommand{\frX}{\mathfrak{X}}
\newcommand{\frY}{\mathfrak{Y}}
\newcommand{\frZ}{\mathfrak{Z}}
\newcommand{\Fra}{\mathfrak{a}}
\newcommand{\Frb}{\mathfrak{b}}
\newcommand{\Frc}{\mathfrak{c}}
\newcommand{\Frd}{\mathfrak{d}}
\newcommand{\Fre}{\mathfrak{e}}
\newcommand{\Frf}{\mathfrak{f}}
\newcommand{\Frg}{\mathfrak{g}}
\newcommand{\Frh}{\mathfrak{h}}
\newcommand{\Fri}{\mathfrak{i}}
\newcommand{\Frj}{\mathfrak{j}}
\newcommand{\Frk}{\mathfrak{k}}
\newcommand{\Frl}{\mathfrak{l}}
\newcommand{\Frm}{\mathfrak{m}}
\newcommand{\Frn}{\mathfrak{n}}
\newcommand{\Fro}{\mathfrak{o}}
\newcommand{\Frp}{\mathfrak{p}}
\newcommand{\Frq}{\mathfrak{q}}
\newcommand{\Frr}{\mathfrak{r}}
\newcommand{\Frs}{\mathfrak{s}}
\newcommand{\Frt}{\mathfrak{t}}
\newcommand{\Fru}{\mathfrak{u}}
\newcommand{\Frv}{\mathfrak{v}}
\newcommand{\Frw}{\mathfrak{w}}
\newcommand{\Frx}{\mathfrak{x}}
\newcommand{\Fry}{\mathfrak{y}}
\newcommand{\Frz}{\mathfrak{z}}
\newcommand{\rA}{\mathrm{A}}
\newcommand{\rB}{\mathrm{B}}
\newcommand{\rC}{\mathrm{C}}
\newcommand{\rD}{\mathrm{D}}
\newcommand{\rE}{\mathrm{E}}
\newcommand{\rF}{\mathrm{F}}
\newcommand{\rG}{\mathrm{G}}
\newcommand{\rH}{\mathrm{H}}
\newcommand{\rI}{\mathrm{I}}
\newcommand{\rJ}{\mathrm{J}}
\newcommand{\rK}{\mathrm{K}}
\newcommand{\rL}{\mathrm{L}}
\newcommand{\rM}{\mathrm{M}}
\newcommand{\rN}{\mathrm{N}}
\newcommand{\rO}{\mathrm{O}}
\newcommand{\rP}{\mathrm{P}}
\newcommand{\rQ}{\mathrm{Q}}
\newcommand{\rR}{\mathrm{R}}
\newcommand{\rS}{\mathrm{S}}
\newcommand{\rT}{\mathrm{T}}
\newcommand{\rU}{\mathrm{U}}
\newcommand{\rV}{\mathrm{V}}
\newcommand{\rW}{\mathrm{W}}
\newcommand{\rX}{\mathrm{X}}
\newcommand{\rY}{\mathrm{Y}}
\newcommand{\rZ}{\mathrm{Z}}
\newcommand{\sfA}{\mathsf{A}}
\newcommand{\sfB}{\mathsf{B}}
\newcommand{\sfC}{\mathsf{C}}
\newcommand{\sfD}{\mathsf{D}}
\newcommand{\sfE}{\mathsf{E}}
\newcommand{\sfF}{\mathsf{F}}
\newcommand{\sfG}{\mathsf{G}}
\newcommand{\sfH}{\mathsf{H}}
\newcommand{\sfI}{\mathsf{I}}
\newcommand{\sfJ}{\mathsf{J}}
\newcommand{\sfK}{\mathsf{K}}
\newcommand{\sfL}{\mathsf{L}}
\newcommand{\sfM}{\mathsf{M}}
\newcommand{\sfN}{\mathsf{N}}
\newcommand{\sfO}{\mathsf{O}}
\newcommand{\sfP}{\mathsf{P}}
\newcommand{\sfQ}{\mathsf{Q}}
\newcommand{\sfR}{\mathsf{R}}
\newcommand{\sfS}{\mathsf{S}}
\newcommand{\sfT}{\mathsf{T}}
\newcommand{\sfU}{\mathsf{U}}
\newcommand{\sfV}{\mathsf{V}}
\newcommand{\sfW}{\mathsf{W}}
\newcommand{\sfX}{\mathsf{X}}
\newcommand{\sfY}{\mathsf{Y}}
\newcommand{\sfZ}{\mathsf{Z}}
\newcommand{\bbA}{\mathbbm{A}}
\newcommand{\bbB}{\mathbbm{B}}
\newcommand{\bbC}{\mathbbm{C}}
\newcommand{\bbD}{\mathbbm{D}}
\newcommand{\bbE}{\mathbbm{E}}
\newcommand{\bbF}{\mathbbm{F}}
\newcommand{\bbG}{\mathbbm{G}}
\newcommand{\bbH}{\mathbbm{H}}
\newcommand{\bbI}{\mathbbm{I}}
\newcommand{\bbJ}{\mathbbm{J}}
\newcommand{\bbK}{\mathbbm{K}}
\newcommand{\bbL}{\mathbbm{L}}
\newcommand{\bbM}{\mathbbm{M}}
\newcommand{\bbN}{\mathbbm{N}}
\newcommand{\bbO}{\mathbbm{O}}
\newcommand{\bbP}{\mathbbm{P}}
\newcommand{\bbQ}{\mathbbm{Q}}
\newcommand{\bbR}{\mathbbm{R}}
\newcommand{\bbS}{\mathbbm{S}}
\newcommand{\bbT}{\mathbbm{T}}
\newcommand{\bbU}{\mathbbm{U}}
\newcommand{\bbV}{\mathbbm{V}}
\newcommand{\bbW}{\mathbbm{W}}
\newcommand{\bbX}{\mathbbm{X}}
\newcommand{\bbY}{\mathbbm{Y}}
\newcommand{\bbZ}{\mathbbm{Z}}
\newcommand{\bba}{\mathbbm{a}}
\newcommand{\bbb}{\mathbbm{b}}
\newcommand{\bbc}{\mathbbm{c}}
\newcommand{\bbd}{\mathbbm{d}}
\newcommand{\bbe}{\mathbbm{e}}
\newcommand{\bbf}{\mathbbm{f}}
\newcommand{\bbg}{\mathbbm{g}}
\newcommand{\bbh}{\mathbbm{h}}
\newcommand{\bbi}{\mathbbm{i}}
\newcommand{\bbj}{\mathbbm{j}}
\newcommand{\bbk}{\mathbbm{k}}
\newcommand{\bbl}{\mathbbm{l}}
\newcommand{\bbm}{\mathbbm{m}}
\newcommand{\bbn}{\mathbbm{n}}
\newcommand{\bbo}{\mathbbm{o}}
\newcommand{\bbp}{\mathbbm{p}}
\newcommand{\bbq}{\mathbbm{q}}
\newcommand{\bbr}{\mathbbm{r}}
\newcommand{\bbs}{\mathbbm{s}}
\newcommand{\bbt}{\mathbbm{t}}
\newcommand{\bbu}{\mathbbm{u}}
\newcommand{\bbv}{\mathbbm{v}}
\newcommand{\bbw}{\mathbbm{w}}
\newcommand{\bbx}{\mathbbm{x}}
\newcommand{\bby}{\mathbbm{y}}
\newcommand{\bbz}{\mathbbm{z}}
\newdir{ >}{{ }*!/-5pt/@{>}}
\begin{xy}
\xymatrix@=32pt {
\rC \ar@<1ex>[r]^F \ar@{}[r]|{\bot} & \rD \ar@<1ex>[l]^U
}
\end{xy}
\qquad
\eta : \Un{\rC} \Rightarrow UF,
\quad
\epsilon : FU \Rightarrow \Un{\rD}
\end{equation*}
で, モナド $(T,\eta,\mu)$ を導くもの ($T=UF, \mu = U \epsilon F$) の全体とする.
そのような 2 つの随伴
\begin{equation*}
\begin{xy}
\xymatrix@=32pt {
\rC \ar@<1ex>[r]^F \ar@{}[r]|{\bot} & \rD \ar@<1ex>[l]^U
}
\end{xy}
\qquad
\eta : \Un{\rC} \Rightarrow UF,
\quad
\epsilon : FU \Rightarrow \Un{\rD}
\end{equation*} \begin{equation*}
\begin{xy}
\xymatrix@=32pt {
\rC \ar@<1ex>[r]^{F'} \ar@{}[r]|{\bot} & \rD' \ar@<1ex>[l]^{U'}
}
\end{xy}
\qquad
\eta' : \Un{\rC} \Rightarrow U'F',
\quad
\epsilon' : F'U' \Rightarrow \Un{\rD'}
\end{equation*} の間の射 $K : F \dashv U \rightarrow F' \dashv U'$ は関手 $K : \rD \rightarrow \rD'$ で, 左随伴と右随伴に対して共に可換, つまり $KF=F'$, $U'K=U$ を満たすものとする:
\begin{equation*}
\begin{xy}
\xymatrix@=32pt {
\rD \ar@<1ex>[dr]^U \ar[rr]^K
\ar@{}[dr]|{\style{display: inline-block; transform: rotate(45deg)}{\dashv}}
&
& {\rD'} \ar@<1.8ex>[dl]^{U'}
\ar@{}[dl]|{\style{display: inline-block; transform: rotate(-45deg)}{\dashv}}
\\
& \rC \ar@<1.2ex>[ul]^F \ar@<0.4ex>[ur]^{F'} &
}
\end{xy}
\end{equation*}
$\Adj_T$ に対して, 次が成り立つ.
命題.$(T,\eta,\mu)$ を圏 $\rC$ 上のモナドとする. このとき, Kleisli 圏 $\rC_T$ は随伴の圏 $\Adj_T$ の始対象であり, Eelenberg-Moore 圏 $\rC^T$ は $\Adj_T$ の終対象である. すなわち, $\rC$ 上でモナド $(T,\eta,\mu)$ を導く任意の随伴 $F \dashv U$ に対して, 一意的な関手 $J : \rC_T \rightarrow \rD$, $K : \rD \rightarrow \rC^T$ が存在して, それぞれ左随伴関手, 右随伴関手と可換になる.
\begin{equation*}
\begin{xy}
\xymatrix@=32pt {
\rC_T \ar@{-->}[r]^J_{\exists!}
\ar[dr]|(.3){U_T}
\ar@{}@<-0.9ex>[dr]|{\style{display: inline-block; transform: rotate(45deg)}{\dashv}}
& \rD \ar@{-->}[r]^K_{\exists!}
\ar@<1ex>[d]^U
\ar@{}[d]|{\dashv}
& \rC^T \ar@<2.2ex>[dl]^{U^T} \\
& \rC \ar@<1ex>[u]^F
\ar@<2.2ex>[ul]^{F_T}
\ar[ur]|(.6){F^T}
\ar@{}@<-0.6ex>[ur]|{\style{display: inline-block; transform: rotate(-45deg)}{\dashv}}
&
}
\end{xy}
\end{equation*} 証明は省略するが, 以下のことが成り立つ.
・ $JF_T = F$, $U^TK=U$.
・関手 $J : \rC_T \rightarrow \rD$ は $\rC_T$ の対象 $c$ に対して
\begin{equation*}
Jc = Fc
\end{equation*} と定義され, $\rC_T$ の射 $f : c \rightsquigarrow c'$, つまり $\rC$ の射 $f : c \rightarrow Tc'$ に対して
\begin{equation*}
\begin{xy}
\xymatrix@=32pt {
Jf := Fc \ar[r]^(.4){Ff} & FTc'=FUFc' \ar[r]^(.65){\epsilon_{Fc'}} & Fc'
}
\end{xy}
\end{equation*} と定義される.
・関手 $K : \rD \rightarrow \rC^T$ は, $\rD$ の対象 $d$ に対して
\begin{equation*}
Kd = (Ud,U{\epsilon_d})
\end{equation*} と定義され, $\rD$ の射 $f : d \rightarrow d'$ に対して
\begin{equation*}
Kf := Uf : (Ud,U\epsilon_d) \rightarrow (Ud',U{\epsilon_{d'}})
\end{equation*} と定義される.

この結果によれば, 圏 $\rC$ 上の Kleisli 圏 $\rC_T$ から Eilenberg-Moore 圏 $\rC^T$ への一意的な関手 $K : \rC_T \rightarrow \rC^T$ が存在することになるが, これは次のように定まる.
Kleisli 圏 $\rC_T$ の対象 $c\in\rC_T$ (つまり $c\in\rC$) に対して,
\begin{equation*}
Kc = (U^TF^Tc,U^T\epsilon_{F^Tc}) = (Tc,U^T\epsilon_{F^Tc}) = (Tc,\mu_c)
\end{equation*}
であり, $\rC_T$ の射 $f : c \rightsquigarrow c'$ つまり $\rC$ の射 $f : c \rightarrow Tc'$ に対して
\begin{equation*}
\begin{xy}
\xymatrix@=32pt {
Kf := (Tc,\mu_{c}) \ar[r]^{Tf} & (T^2c',\mu_{Tc'}) \ar[r]^{\mu_{c'}} & (Tc'\mu_{c'})
}
\end{xy}
\end{equation*} である.
この関手 $K : \rC_T \rightarrow \rC^T$ について, 次の命題が成り立つ.
命題.圏 $\rC$ 上の随伴からなる圏 $\Adj_T$ における, 一意的な関手 $K : \rC_T \rightarrow \rC^T$ は充満忠実 (full and faithful) であり, $K$ は $\rC_T$ とその $\rC^T$ における像の間の圏同型を与える. すなわち, Kleisli 圏 $\rC_T$ は Eilenberg-Moore 圏 $\rC^T$ に埋め込まれる.

タグ：モナド圏論随伴の圏 Kleisli 圏 Eilenberg-Moore 圏

posted by 底彦 at 08:50 | Comment(0) | TrackBack(0) | 数学

2023年07月21日

数学: モナド ── Kleisli 圏の例 (続き)

数学: モナドから導かれる随伴の圏 (3)$
モナド ── 定義と随伴により引き起こされるモナド ,
随伴から導かれるモナドの例 ── maybe モナド
モナドから導かれる随伴 (1) ── Eilenberg-Moore 圏
モナドから導かれる随伴 (2) ── Kleisli 圏の続き.

集合 $S$ を固定する. $S$ の各元を「状態」と呼ぶことにする.
与えられた集合に対して, 状態 $S$ との直積を与える関手 $S\times- : \mathbf{Set} \rightarrow \mathbf{Set}$ と, $S$ から集合 $A$ への関数の集合 (これを $A^S$ と記す) を与える関手 $(-)^S : \mathbf{Set} \rightarrow \mathbf{Set}$ は随伴関係 $S\times- \dashv (-)^S$ をなす.

この随伴からモナド $((S\times-)^S,\eta,\mu)$ が導かれる.
単位 (unit) $\eta : 1_{\mathbf{Set}} \Rightarrow (S\times-)^S$ は各集合 $A$ に対して
\begin{equation*}
\DeclareMathOperator{\Aff}{Aff}
\DeclareMathOperator{\Ar}{Ar}
\DeclareMathOperator{\Arccos}{Arccos}
\DeclareMathOperator{\Arcsin}{Arcsin}
\DeclareMathOperator{\Arr}{Arr}
\DeclareMathOperator{\arr}{arr}
\DeclareMathOperator{\Aut}{Aut}
\DeclareMathOperator{\Auto}{Auto}
\DeclareMathOperator{\Axiom}{Axiom}
\DeclareMathOperator{\Bilin}{Bilin}
\DeclareMathOperator{\card}{card}
\DeclareMathOperator{\Catelem}{\int}
\DeclareMathOperator{\Cocone}{Cocone}
\DeclareMathOperator{\Cod}{cod}
\DeclareMathOperator{\Codomain}{cod}
\DeclareMathOperator{\Coin}{coin}
\DeclareMathOperator{\coker}{coker}
\DeclareMathOperator{\Colim}{colim}
\DeclareMathOperator{\comp}{comp}
\DeclareMathOperator{\Conf}{Conf}
\DeclareMathOperator{\Conj}{Conj}
\DeclareMathOperator{\Dom}{dom}
\DeclareMathOperator{\Domain}{dom}
\DeclareMathOperator{\Edge}{Edge}
\DeclareMathOperator{\Ev}{ev}
\DeclareMathOperator{\GCD}{gcd}
\DeclareMathOperator{\Gr}{Gr}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Id}{id}
\DeclareMathOperator{\IM}{Im}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\Ind}{ind}
\DeclareMathOperator{\INIT}{init}
\DeclareMathOperator{\iso}{iso}
\DeclareMathOperator{\LCM}{lcm}
\DeclareMathOperator{\Map}{Map}
\DeclareMathOperator{\mor}{arr}
\DeclareMathOperator{\Nat}{Nat}
\DeclareMathOperator{\Ob}{Ob}
\DeclareMathOperator{\ob}{ob}
\DeclareMathOperator{\ord}{ord}
\DeclareMathOperator{\Path}{Path}
\DeclareMathOperator{\PConf}{PConf}
\DeclareMathOperator{\Point}{Point}
\DeclareMathOperator{\Prob}{Prob}
\DeclareMathOperator{\RE}{Re}
\DeclareMathOperator{\Res}{res}
\DeclareMathOperator{\Sect}{Sect}
\DeclareMathOperator{\SF}{SF}
\DeclareMathOperator{\SkelCat}{sk}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Sq}{Sq}
\DeclareMathOperator{\Struct}{Struct}
\DeclareMathOperator{\Sub}{Sub}
\DeclareMathOperator{\Sym}{Sym}
\DeclareMathOperator{\TERM}{term}
\DeclareMathOperator{\Vertex}{Vert}
\newcommand{\Abs}[1]{\lvert{#1}\rvert}
\newcommand{\Bs}{\backslash}
\newcommand{\Cdot}{\,\cdot^{\mathrm{op}}}
\newcommand{\Comma}[2]{{{#1}\!\downarrow\!{#2}}}
\newcommand{\CommaCat}[2]{(#1/#2)}
\newcommand{\Complement}[1]{{\smash[t]{\mathstrut #1}}^{\mathrm{c}}}
\newcommand{\Emph}[1]{\textit{#1}}
\newcommand{\Eqclass}[4]{{#1#2#3}_{#4}}
\newcommand{\EqCls}[2]{{\left[#1\right]}_{#2}}
\newcommand{\Eqcls}[1]{\left[#1\right]}
\newcommand{\Expt}[2]{{\smash[t]{\mathstrut #1}}^{\mathstrut #2}}
\newcommand{\FnRest}[2]{{#1}|{#2}}
\newcommand{\Func}[2]{\mathrm{Func}(#1,#2)}
\newcommand{\g}{\varg}
\newcommand{\Inc}[2]{\mathrm{incl}\left(#1,#2\right)}
\newcommand{\Incl}[2]{\mathrm{incl}_{#1}^{#2}}
\newcommand{\InclArrow}[2]{\morphism(0,0)/>->/<450,0>[\Incl{#1}{#2} : {#1}\,\,`{#2};]}
\newcommand{\Ip}{\amalg}
\newcommand{\Lb}[1]{\mathrm{lb}(#1)}
\newcommand{\LH}{\mathrm{LH}}
\newcommand{\Lowerset}[1]{\downarrow\!\!{#1}}
\newcommand{\Leadsto}{\quad\leadsto\quad}
\newcommand{\Lrsquigarrow}{\quad\leftrightsquigarrow\quad}
\newcommand{\Mb}[1]{\mathbf{#1}}
\newcommand{\Mbb}[1]{\mathbb{#1}}
\newcommand{\Mi}[1]{\mathit{#1}}
\newcommand{\Mlb}[1]{\mathrm{mlb}(#1)}
\newcommand{\Mr}[1]{\mathrm{#1}}
\newcommand{\Ms}[1]{\mathscr{#1}}
\newcommand{\Mt}[1]{\mathtt{#1}}
\newcommand{\Mub}[1]{\mathrm{mub}(#1)}
\newcommand{\newinf}{\mathop{\mathrm{inf}\vphantom{\mathrm{sup}}}}
\newcommand{\newsup}{\mathop{\smash{\mathrm{sup}}}}
\newcommand{\Opp}[1]{#1^{\mathrm{op}}}
\newcommand{\Prj}[2]{\mathrm{proj}\left(#1,#2\right)}
\newcommand{\Proj}[2]{\mathrm{proj}^{#1}_{#2}}
\newcommand{\Pw}{\mathbf{P}}
\newcommand{\Rn}[1]{{\bmdefine{R}}^{#1}}
\newcommand{\q}{\hspace{1em}}
\newcommand{\qq}{\hspace{0.5em}}
\newcommand{\Rel}[1]{\langle{#1}\rangle}
\newcommand{\Rest}[2]{{#1}|{#2}}
\newcommand{\Slash}[1]{{\ooalign{\hfil/\hfil\crcr$#1$}}}
\newcommand{\SliCat}[2]{{#1}\,\big/\,{#2}}
\newcommand{\Src}{d^{0,\mathrm{op}}}
\newcommand{\ssqrt}[1]{\sqrt{\smash[b]{\mathstrut #1}}}
\newcommand{\Tgt}{d^{1,\mathrm{op}}}
\newcommand{\TwArCat}[1]{\mathrm{Tw}(#1)}
\newcommand{\Ub}[1]{\mathrm{ub}(#1)}
\newcommand{\Un}[1]{{1}_{#1}}
\newcommand{\Upperset}[1]{\uparrow\!\!{#1}}
\newcommand{\VectCat}[1]{#1 \mathchar`- \mathbf{Vect}}
\newcommand{\VS}{\vspace*{-1ex}}
\newcommand{\Wbar}[1]{\widebar{#1}}
\newcommand{\Ab}{\mathbf{Ab}}
\newcommand{\Adj}{\mathbf{Adj}}
\newcommand{\Affine}{\mathbf{Affine}}
\newcommand{\Ban}{\mathbf{Ban}}
\newcommand{\bbDelta}{\Delta\mkern-12mu\Delta}
\newcommand{\Card}{\mathbf{Card}}
\newcommand{\CAT}{\mathbf{CAT}}
\newcommand{\Cat}{\mathbf{Cat}}
\newcommand{\cgHaus}{\mathbf{cgHaus}}
\newcommand{\Ch}{\mathbf{Ch}}
\newcommand{\cHaus}{\mathbf{cHaus}}
\newcommand{\Cluster}{\mathbf{Cluster}}
\newcommand{\CMonoid}{\mathbf{CMonoid}}
\newcommand{\CRing}{\mathbf{CRing}}
\newcommand{\DirGraph}{\mathbf{DirGraph}}
\newcommand{\End}{\mathbf{End}}
\newcommand{\Euclid}{\mathbf{Euclid}}
\newcommand{\Field}{\mathbf{Field}}
\newcommand{\Fin}{\mathbf{Fin}}
\newcommand{\FinMetric}{\mathbf{FinMetric}}
\newcommand{\Four}{\mathbbm{4}}
\newcommand{\Graph}{\mathbf{Graph}}
\newcommand{\GrMod}{\mathbf{GrMod}}
\newcommand{\Grp}{\mathbf{Grp}}
\newcommand{\Group}{\mathbf{Group}}
\newcommand{\Groupoid}{\mathbf{Groupoid}}
\newcommand{\Haus}{\mathbf{Haus}}
\newcommand{\Htpy}{\mathbf{Htpy}}
\newcommand{\Man}{\mathbf{Man}}
\newcommand{\Mapsdown}{\rotatebox{270}{$\mapsto$}}
\newcommand{\Mapsup}{\rotatebox{90}{$\mapsto$}}
\newcommand{\Mat}{\mathbf{Mat}}
\newcommand{\Meas}{\mathbf{Meas}}
\newcommand{\Measure}{\mathbf{Measure}}
\newcommand{\Mod}{\mathbf{Mod}}
\newcommand{\Model}{\mathbf{Model}}
\newcommand{\Mon}{\mathbf{Mon}}
\newcommand{\Monoid}{\mathbf{Monoid}}
\newcommand{\oMega}{\bbomega}
\newcommand{\One}{\mymathbb{1}}
\newcommand{\Ord}{\mathrm{Ord}}
\newcommand{\PCluster}{\mathbf{PCluster}}
\newcommand{\POs}{\mathbf{Poset}}
\newcommand{\Poset}{\mathbf{Poset}}
\newcommand{\PROJ}{\mathbf{Proj}}
\newcommand{\Psh}{\mathbf{Psh}}
\newcommand{\Ring}{\mathbf{Ring}}
\newcommand{\Rng}{\mathbf{Rng}}
\newcommand{\SET}{\mathbf{SET}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\setmid}{\mathrel{}\middle|\mathrel{}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Shv}{\mathbf{Shv}}
\newcommand{\Three}{\mymathbb{3}}
\renewcommand{\Top}{\mathbf{Top}}
\newcommand{\Two}{\mymathbb{2}}
\newcommand{\Vect}{\mathbf{Vect}}
\newcommand{\Zero}{\mymathbb{0}}
\newcommand{\sA}{\mathscr{A}}
\newcommand{\sB}{\mathscr{B}}
\newcommand{\sC}{\mathscr{C}}
\newcommand{\sD}{\mathscr{D}}
\newcommand{\sE}{\mathscr{E}}
\newcommand{\sF}{\mathscr{F}}
\newcommand{\sG}{\mathscr{G}}
\newcommand{\sH}{\mathscr{H}}
\newcommand{\sI}{\mathscr{I}}
\newcommand{\sJ}{\mathscr{J}}
\newcommand{\sK}{\mathscr{K}}
\newcommand{\sL}{\mathscr{L}}
\newcommand{\sM}{\mathscr{M}}
\newcommand{\sN}{\mathscr{N}}
\newcommand{\sO}{\mathscr{O}}
\newcommand{\sP}{\mathscr{P}}
\newcommand{\sQ}{\mathscr{Q}}
\newcommand{\sR}{\mathscr{R}}
\newcommand{\sS}{\mathscr{S}}
\newcommand{\sT}{\mathscr{T}}
\newcommand{\sU}{\mathscr{U}}
\newcommand{\sV}{\mathscr{V}}
\newcommand{\sW}{\mathscr{W}}
\newcommand{\sX}{\mathscr{X}}
\newcommand{\sY}{\mathscr{Y}}
\newcommand{\sZ}{\mathscr{Z}}
\newcommand{\bfA}{\mathbf{A}}
\newcommand{\bfB}{\mathbf{B}}
\newcommand{\bfC}{\mathbf{C}}
\newcommand{\bfD}{\mathbf{D}}
\newcommand{\bfE}{\mathbf{E}}
\newcommand{\bfF}{\mathbf{F}}
\newcommand{\bfG}{\mathbf{G}}
\newcommand{\bfH}{\mathbf{H}}
\newcommand{\bfI}{\mathbf{I}}
\newcommand{\bfJ}{\mathbf{J}}
\newcommand{\bfK}{\mathbf{K}}
\newcommand{\bfL}{\mathbf{L}}
\newcommand{\bfM}{\mathbf{M}}
\newcommand{\bfN}{\mathbf{N}}
\newcommand{\bfO}{\mathbf{O}}
\newcommand{\bfP}{\mathbf{P}}
\newcommand{\bfQ}{\mathbf{Q}}
\newcommand{\bfR}{\mathbf{R}}
\newcommand{\bfS}{\mathbf{S}}
\newcommand{\bfT}{\mathbf{T}}
\newcommand{\bfU}{\mathbf{U}}
\newcommand{\bfV}{\mathbf{V}}
\newcommand{\bfW}{\mathbf{W}}
\newcommand{\bfX}{\mathbf{X}}
\newcommand{\bfY}{\mathbf{Y}}
\newcommand{\bfZ}{\mathbf{Z}}
\newcommand{\bfa}{\mathbf{a}}
\newcommand{\bfb}{\mathbf{b}}
\newcommand{\bfc}{\mathbf{c}}
\newcommand{\bfd}{\mathbf{d}}
\newcommand{\bfe}{\mathbf{e}}
\newcommand{\bff}{\mathbf{f}}
\newcommand{\bfg}{\mathbf{g}}
\newcommand{\bfh}{\mathbf{h}}
\newcommand{\bfi}{\mathbf{i}}
\newcommand{\bfj}{\mathbf{j}}
\newcommand{\bfk}{\mathbf{k}}
\newcommand{\bfl}{\mathbf{l}}
\newcommand{\bfm}{\mathbf{m}}
\newcommand{\bfn}{\mathbf{n}}
\newcommand{\bfo}{\mathbf{o}}
\newcommand{\bfp}{\mathbf{p}}
\newcommand{\bfq}{\mathbf{q}}
\newcommand{\bfr}{\mathbf{r}}
\newcommand{\bfs}{\mathbf{s}}
\newcommand{\bft}{\mathbf{t}}
\newcommand{\bfu}{\mathbf{u}}
\newcommand{\bfv}{\mathbf{v}}
\newcommand{\bfw}{\mathbf{w}}
\newcommand{\bfx}{\mathbf{x}}
\newcommand{\bfy}{\mathbf{y}}
\newcommand{\bfz}{\mathbf{z}}
\newcommand{\frA}{\mathfrak{A}}
\newcommand{\frB}{\mathfrak{B}}
\newcommand{\frC}{\mathfrak{C}}
\newcommand{\frD}{\mathfrak{D}}
\newcommand{\frE}{\mathfrak{E}}
\newcommand{\frF}{\mathfrak{F}}
\newcommand{\frG}{\mathfrak{G}}
\newcommand{\frH}{\mathfrak{H}}
\newcommand{\frI}{\mathfrak{I}}
\newcommand{\frJ}{\mathfrak{J}}
\newcommand{\frK}{\mathfrak{K}}
\newcommand{\frL}{\mathfrak{L}}
\newcommand{\frM}{\mathfrak{M}}
\newcommand{\frN}{\mathfrak{N}}
\newcommand{\frO}{\mathfrak{O}}
\newcommand{\frP}{\mathfrak{P}}
\newcommand{\frQ}{\mathfrak{Q}}
\newcommand{\frR}{\mathfrak{R}}
\newcommand{\frS}{\mathfrak{S}}
\newcommand{\frT}{\mathfrak{T}}
\newcommand{\frU}{\mathfrak{U}}
\newcommand{\frV}{\mathfrak{V}}
\newcommand{\frW}{\mathfrak{W}}
\newcommand{\frX}{\mathfrak{X}}
\newcommand{\frY}{\mathfrak{Y}}
\newcommand{\frZ}{\mathfrak{Z}}
\newcommand{\Fra}{\mathfrak{a}}
\newcommand{\Frb}{\mathfrak{b}}
\newcommand{\Frc}{\mathfrak{c}}
\newcommand{\Frd}{\mathfrak{d}}
\newcommand{\Fre}{\mathfrak{e}}
\newcommand{\Frf}{\mathfrak{f}}
\newcommand{\Frg}{\mathfrak{g}}
\newcommand{\Frh}{\mathfrak{h}}
\newcommand{\Fri}{\mathfrak{i}}
\newcommand{\Frj}{\mathfrak{j}}
\newcommand{\Frk}{\mathfrak{k}}
\newcommand{\Frl}{\mathfrak{l}}
\newcommand{\Frm}{\mathfrak{m}}
\newcommand{\Frn}{\mathfrak{n}}
\newcommand{\Fro}{\mathfrak{o}}
\newcommand{\Frp}{\mathfrak{p}}
\newcommand{\Frq}{\mathfrak{q}}
\newcommand{\Frr}{\mathfrak{r}}
\newcommand{\Frs}{\mathfrak{s}}
\newcommand{\Frt}{\mathfrak{t}}
\newcommand{\Fru}{\mathfrak{u}}
\newcommand{\Frv}{\mathfrak{v}}
\newcommand{\Frw}{\mathfrak{w}}
\newcommand{\Frx}{\mathfrak{x}}
\newcommand{\Fry}{\mathfrak{y}}
\newcommand{\Frz}{\mathfrak{z}}
\newcommand{\rA}{\mathrm{A}}
\newcommand{\rB}{\mathrm{B}}
\newcommand{\rC}{\mathrm{C}}
\newcommand{\rD}{\mathrm{D}}
\newcommand{\rE}{\mathrm{E}}
\newcommand{\rF}{\mathrm{F}}
\newcommand{\rG}{\mathrm{G}}
\newcommand{\rH}{\mathrm{H}}
\newcommand{\rI}{\mathrm{I}}
\newcommand{\rJ}{\mathrm{J}}
\newcommand{\rK}{\mathrm{K}}
\newcommand{\rL}{\mathrm{L}}
\newcommand{\rM}{\mathrm{M}}
\newcommand{\rN}{\mathrm{N}}
\newcommand{\rO}{\mathrm{O}}
\newcommand{\rP}{\mathrm{P}}
\newcommand{\rQ}{\mathrm{Q}}
\newcommand{\rR}{\mathrm{R}}
\newcommand{\rS}{\mathrm{S}}
\newcommand{\rT}{\mathrm{T}}
\newcommand{\rU}{\mathrm{U}}
\newcommand{\rV}{\mathrm{V}}
\newcommand{\rW}{\mathrm{W}}
\newcommand{\rX}{\mathrm{X}}
\newcommand{\rY}{\mathrm{Y}}
\newcommand{\rZ}{\mathrm{Z}}
\newcommand{\sfA}{\mathsf{A}}
\newcommand{\sfB}{\mathsf{B}}
\newcommand{\sfC}{\mathsf{C}}
\newcommand{\sfD}{\mathsf{D}}
\newcommand{\sfE}{\mathsf{E}}
\newcommand{\sfF}{\mathsf{F}}
\newcommand{\sfG}{\mathsf{G}}
\newcommand{\sfH}{\mathsf{H}}
\newcommand{\sfI}{\mathsf{I}}
\newcommand{\sfJ}{\mathsf{J}}
\newcommand{\sfK}{\mathsf{K}}
\newcommand{\sfL}{\mathsf{L}}
\newcommand{\sfM}{\mathsf{M}}
\newcommand{\sfN}{\mathsf{N}}
\newcommand{\sfO}{\mathsf{O}}
\newcommand{\sfP}{\mathsf{P}}
\newcommand{\sfQ}{\mathsf{Q}}
\newcommand{\sfR}{\mathsf{R}}
\newcommand{\sfS}{\mathsf{S}}
\newcommand{\sfT}{\mathsf{T}}
\newcommand{\sfU}{\mathsf{U}}
\newcommand{\sfV}{\mathsf{V}}
\newcommand{\sfW}{\mathsf{W}}
\newcommand{\sfX}{\mathsf{X}}
\newcommand{\sfY}{\mathsf{Y}}
\newcommand{\sfZ}{\mathsf{Z}}
\newcommand{\bbA}{\mathbbm{A}}
\newcommand{\bbB}{\mathbbm{B}}
\newcommand{\bbC}{\mathbbm{C}}
\newcommand{\bbD}{\mathbbm{D}}
\newcommand{\bbE}{\mathbbm{E}}
\newcommand{\bbF}{\mathbbm{F}}
\newcommand{\bbG}{\mathbbm{G}}
\newcommand{\bbH}{\mathbbm{H}}
\newcommand{\bbI}{\mathbbm{I}}
\newcommand{\bbJ}{\mathbbm{J}}
\newcommand{\bbK}{\mathbbm{K}}
\newcommand{\bbL}{\mathbbm{L}}
\newcommand{\bbM}{\mathbbm{M}}
\newcommand{\bbN}{\mathbbm{N}}
\newcommand{\bbO}{\mathbbm{O}}
\newcommand{\bbP}{\mathbbm{P}}
\newcommand{\bbQ}{\mathbbm{Q}}
\newcommand{\bbR}{\mathbbm{R}}
\newcommand{\bbS}{\mathbbm{S}}
\newcommand{\bbT}{\mathbbm{T}}
\newcommand{\bbU}{\mathbbm{U}}
\newcommand{\bbV}{\mathbbm{V}}
\newcommand{\bbW}{\mathbbm{W}}
\newcommand{\bbX}{\mathbbm{X}}
\newcommand{\bbY}{\mathbbm{Y}}
\newcommand{\bbZ}{\mathbbm{Z}}
\newcommand{\bba}{\mathbbm{a}}
\newcommand{\bbb}{\mathbbm{b}}
\newcommand{\bbc}{\mathbbm{c}}
\newcommand{\bbd}{\mathbbm{d}}
\newcommand{\bbe}{\mathbbm{e}}
\newcommand{\bbf}{\mathbbm{f}}
\newcommand{\bbg}{\mathbbm{g}}
\newcommand{\bbh}{\mathbbm{h}}
\newcommand{\bbi}{\mathbbm{i}}
\newcommand{\bbj}{\mathbbm{j}}
\newcommand{\bbk}{\mathbbm{k}}
\newcommand{\bbl}{\mathbbm{l}}
\newcommand{\bbm}{\mathbbm{m}}
\newcommand{\bbn}{\mathbbm{n}}
\newcommand{\bbo}{\mathbbm{o}}
\newcommand{\bbp}{\mathbbm{p}}
\newcommand{\bbq}{\mathbbm{q}}
\newcommand{\bbr}{\mathbbm{r}}
\newcommand{\bbs}{\mathbbm{s}}
\newcommand{\bbt}{\mathbbm{t}}
\newcommand{\bbu}{\mathbbm{u}}
\newcommand{\bbv}{\mathbbm{v}}
\newcommand{\bbw}{\mathbbm{w}}
\newcommand{\bbx}{\mathbbm{x}}
\newcommand{\bby}{\mathbbm{y}}
\newcommand{\bbz}{\mathbbm{z}}
\newdir{ >}{{ }*!/-5pt/@{>}}
\eta_A : A \rightarrow (S \times A)^S, \qquad (\eta_A(a))(s) = (s,a)
\end{equation*} と定義される. 結果の $(s,a)$ を, 入力 $a \in A$ と現在の状態 $s \in S$ の対と考える.
また, 余単位 (counit) $\epsilon : S \times (-)^S \Rightarrow \Un{\Set}$ は状態 $s \in S$ と, 各状態における入力を与える関数 $f : S \rightarrow A$ とに対して,
\begin{equation*}
\epsilon_A : S \times A^S \rightarrow A, \qquad \epsilon_A(s,f) = f(s)
\end{equation*} と定義される. つまり, 各 $\epsilon_A : S \times A^S \rightarrow A$ は各状態における入力を与える評価関数 (evaluation function) と見なせる.
3 つ組 $((S\times-)^S,\eta,\mu)$ は図式に対する計算により
\begin{equation*}
\begin{xy}
\xymatrix@=36pt {
(S\times(S\times(S \times A)^S)^S)^S
\ar[r]^(.55){(S\times\mu_A)^S}
\ar[d]_{\mu_{(S \times A)^S}}
& (S\times(S \times A)^S)^S ->
\ar[d]^{\mu_A} \\
(S\times(S \times A)^S)^S
\ar[r]_{\mu_A}
& (S \times A)^S
}
\end{xy}
\qquad
\begin{xy}
\xymatrix@=36pt {
(S \times A)^S \ar[r]^(.4){\eta_{(S \times A)^S}} \ar[dr]_{\Un{(S \times A)^S}}
& (S\times(S \times A)^S)^S \ar[d]^{\mu_A}
& (S \times A)^S \ar[l]_(0.4){(S\times\eta_A)^S} \ar[dl]^{\Un{(S \times A)^S}} \\
& (S \times A)^S &
}
\end{xy}
\end{equation*}
を可換にし, 実際にモナドになっていることがわかる.
この余単位 $\epsilon$ を用いて, モナド $S\times(-)^S$ の積 (multiplication) $\mu : (S\times(S\times(-)^S))^S \Rightarrow (S\times-)^S$ を明示的に書き下してみる.
$\mu=(-)^S\epsilon(S\times-) : (S\times(S \times -)^S)^S \rightarrow (S\times-)^S$ である. $u \in (S\times(S \times A)^S)^S$ をとり, 状態 $s \in S$ に対して,
\begin{equation*}
u(s) = (u_1(s),u_2(s))
\end{equation*} とおく. $u_1(s) \in S$, $u_2(s) : S \rightarrow S \times A$ である.
$u_1(s)$ は状態 $s$ に対する新しい状態, $u_2(s)$ は状態 $s$ に対する新たな状態と入力の対を与える.
このとき,
\begin{equation*}
\mu_A(u)(s) = ((-)^S\epsilon(S\times-))_A(u))(s) = ((\epsilon_{S \times A})^S(u))(s) = \epsilon_{S \times A}(u(s)) = \epsilon_{S \times A}(u_1(s),u_2(s)) = u_2(s)(u_1(s))
\end{equation*} となる.

Kleisli 圏における対象は集合であり, この集合を状態の集まりであると考える.
Kleisli 圏 $\Set_{(S\times-)^S}$ における射 $f : A \rightsquigarrow B$ は $\rC$ における関数 $f : A \rightarrow (S \times B)^S$ であるが, この関数 $f$ は $f : A \times S \rightarrow B \times S$ と見なせる.
入力 $a$ と現在の状態 $s$ の対 $(a,s) \in A \times S$ に対して
\begin{equation*}
f(a,s) = (f_s(a), s'(a,s))
\end{equation*} とおく. このとき, $f_s(a)$ は入力と状態の対 $(a,s)$ によって決まる出力 $f_s(a) \in B$ と, アップデートされた状態 $s'(a,s) \in S$ の対と考えられる.
たとえば, 関数型プログラミング言語 Haskell においては, このアップデートされた状態 $s'(a,s)$ は計算 $f$ の「副作用 (side effect)」として扱われる.
**数学: モナドから導かれる随伴の圏 (3)$
モナド ── 定義と随伴により引き起こされるモナド ,
随伴から導かれるモナドの例 ── maybe モナド
モナドから導かれる随伴 (1) ── Eilenberg-Moore 圏
モナドから導かれる随伴 (2) ── Kleisli 圏の続き.

集合 $S$ を固定する. $S$ の各元を「状態」と呼ぶことにする.
与えられた集合に対して, 状態 $S$ との直積を与える関手 $S\times- : \mathbf{Set} \rightarrow \mathbf{Set}$ と, $S$ から集合 $A$ への関数の集合 (これを $A^S$ と記す) を与える関手 $(-)^S :z \mathbf{Set} \rightarrow \mathbf{Set}$ は随伴関係 $S\times- \dashv (-)^S$ をなす.

この随伴からモナド $((S\times-)^S,\eta,\mu)$ が導かれる.
単位 (unit) $\eta : 1_{\mathbf{Set}} \Rightarrow (S\times-)^S$ は各集合 $A$ に対して
\begin{equation*}
\DeclareMathOperator{\Aff}{Aff}
\DeclareMathOperator{\Ar}{Ar}
\DeclareMathOperator{\Arccos}{Arccos}
\DeclareMathOperator{\Arcsin}{Arcsin}
\DeclareMathOperator{\Arr}{Arr}
\DeclareMathOperator{\arr}{arr}
\DeclareMathOperator{\Aut}{Aut}
\DeclareMathOperator{\Auto}{Auto}
\DeclareMathOperator{\Axiom}{Axiom}
\DeclareMathOperator{\Bilin}{Bilin}
\DeclareMathOperator{\card}{card}
\DeclareMathOperator{\Catelem}{\int}
\DeclareMathOperator{\Cocone}{Cocone}
\DeclareMathOperator{\Cod}{cod}
\DeclareMathOperator{\Codomain}{cod}
\DeclareMathOperator{\Coin}{coin}
\DeclareMathOperator{\coker}{coker}
\DeclareMathOperator{\Colim}{colim}
\DeclareMathOperator{\comp}{comp}
\DeclareMathOperator{\Conf}{Conf}
\DeclareMathOperator{\Conj}{Conj}
\DeclareMathOperator{\Dom}{dom}
\DeclareMathOperator{\Domain}{dom}
\DeclareMathOperator{\Edge}{Edge}
\DeclareMathOperator{\Ev}{ev}
\DeclareMathOperator{\GCD}{gcd}
\DeclareMathOperator{\Gr}{Gr}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Id}{id}
\DeclareMathOperator{\IM}{Im}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\Ind}{ind}
\DeclareMathOperator{\INIT}{init}
\DeclareMathOperator{\iso}{iso}
\DeclareMathOperator{\LCM}{lcm}
\DeclareMathOperator{\Map}{Map}
\DeclareMathOperator{\mor}{arr}
\DeclareMathOperator{\Nat}{Nat}
\DeclareMathOperator{\Ob}{Ob}
\DeclareMathOperator{\ob}{ob}
\DeclareMathOperator{\ord}{ord}
\DeclareMathOperator{\Path}{Path}
\DeclareMathOperator{\PConf}{PConf}
\DeclareMathOperator{\Point}{Point}
\DeclareMathOperator{\Prob}{Prob}
\DeclareMathOperator{\RE}{Re}
\DeclareMathOperator{\Res}{res}
\DeclareMathOperator{\Sect}{Sect}
\DeclareMathOperator{\SF}{SF}
\DeclareMathOperator{\SkelCat}{sk}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Sq}{Sq}
\DeclareMathOperator{\Struct}{Struct}
\DeclareMathOperator{\Sub}{Sub}
\DeclareMathOperator{\Sym}{Sym}
\DeclareMathOperator{\TERM}{term}
\DeclareMathOperator{\Vertex}{Vert}
\newcommand{\Abs}[1]{\lvert{#1}\rvert}
\newcommand{\Bs}{\backslash}
\newcommand{\Cdot}{\,\cdot^{\mathrm{op}}}
\newcommand{\Comma}[2]{{{#1}\!\downarrow\!{#2}}}
\newcommand{\CommaCat}[2]{(#1/#2)}
\newcommand{\Complement}[1]{{\smash[t]{\mathstrut #1}}^{\mathrm{c}}}
\newcommand{\Emph}[1]{\textit{#1}}
\newcommand{\Eqclass}[4]{{#1#2#3}_{#4}}
\newcommand{\EqCls}[2]{{\left[#1\right]}_{#2}}
\newcommand{\Eqcls}[1]{\left[#1\right]}
\newcommand{\Expt}[2]{{\smash[t]{\mathstrut #1}}^{\mathstrut #2}}
\newcommand{\FnRest}[2]{{#1}|{#2}}
\newcommand{\Func}[2]{\mathrm{Func}(#1,#2)}
\newcommand{\g}{\varg}
\newcommand{\Inc}[2]{\mathrm{incl}\left(#1,#2\right)}
\newcommand{\Incl}[2]{\mathrm{incl}_{#1}^{#2}}
\newcommand{\InclArrow}[2]{\morphism(0,0)/>->/<450,0>[\Incl{#1}{#2} : {#1}\,\,`{#2};]}
\newcommand{\Ip}{\amalg}
\newcommand{\Lb}[1]{\mathrm{lb}(#1)}
\newcommand{\LH}{\mathrm{LH}}
\newcommand{\Lowerset}[1]{\downarrow\!\!{#1}}
\newcommand{\Leadsto}{\quad\leadsto\quad}
\newcommand{\Lrsquigarrow}{\quad\leftrightsquigarrow\quad}
\newcommand{\Mb}[1]{\mathbf{#1}}
\newcommand{\Mbb}[1]{\mathbb{#1}}
\newcommand{\Mi}[1]{\mathit{#1}}
\newcommand{\Mlb}[1]{\mathrm{mlb}(#1)}
\newcommand{\Mr}[1]{\mathrm{#1}}
\newcommand{\Ms}[1]{\mathscr{#1}}
\newcommand{\Mt}[1]{\mathtt{#1}}
\newcommand{\Mub}[1]{\mathrm{mub}(#1)}
\newcommand{\newinf}{\mathop{\mathrm{inf}\vphantom{\mathrm{sup}}}}
\newcommand{\newsup}{\mathop{\smash{\mathrm{sup}}}}
\newcommand{\Opp}[1]{#1^{\mathrm{op}}}
\newcommand{\Prj}[2]{\mathrm{proj}\left(#1,#2\right)}
\newcommand{\Proj}[2]{\mathrm{proj}^{#1}_{#2}}
\newcommand{\Pw}{\mathbf{P}}
\newcommand{\Rn}[1]{{\bmdefine{R}}^{#1}}
\newcommand{\q}{\hspace{1em}}
\newcommand{\qq}{\hspace{0.5em}}
\newcommand{\Rel}[1]{\langle{#1}\rangle}
\newcommand{\Rest}[2]{{#1}|{#2}}
\newcommand{\Slash}[1]{{\ooalign{\hfil/\hfil\crcr$#1$}}}
\newcommand{\SliCat}[2]{{#1}\,\big/\,{#2}}
\newcommand{\Src}{d^{0,\mathrm{op}}}
\newcommand{\ssqrt}[1]{\sqrt{\smash[b]{\mathstrut #1}}}
\newcommand{\Tgt}{d^{1,\mathrm{op}}}
\newcommand{\TwArCat}[1]{\mathrm{Tw}(#1)}
\newcommand{\Ub}[1]{\mathrm{ub}(#1)}
\newcommand{\Un}[1]{{1}_{#1}}
\newcommand{\Upperset}[1]{\uparrow\!\!{#1}}
\newcommand{\VectCat}[1]{#1 \mathchar`- \mathbf{Vect}}
\newcommand{\VS}{\vspace*{-1ex}}
\newcommand{\Wbar}[1]{\widebar{#1}}
\newcommand{\Ab}{\mathbf{Ab}}
\newcommand{\Adj}{\mathbf{Adj}}
\newcommand{\Affine}{\mathbf{Affine}}
\newcommand{\Ban}{\mathbf{Ban}}
\newcommand{\bbDelta}{\Delta\mkern-12mu\Delta}
\newcommand{\Card}{\mathbf{Card}}
\newcommand{\CAT}{\mathbf{CAT}}
\newcommand{\Cat}{\mathbf{Cat}}
\newcommand{\cgHaus}{\mathbf{cgHaus}}
\newcommand{\Ch}{\mathbf{Ch}}
\newcommand{\cHaus}{\mathbf{cHaus}}
\newcommand{\Cluster}{\mathbf{Cluster}}
\newcommand{\CMonoid}{\mathbf{CMonoid}}
\newcommand{\CRing}{\mathbf{CRing}}
\newcommand{\DirGraph}{\mathbf{DirGraph}}
\newcommand{\End}{\mathbf{End}}
\newcommand{\Euclid}{\mathbf{Euclid}}
\newcommand{\Field}{\mathbf{Field}}
\newcommand{\Fin}{\mathbf{Fin}}
\newcommand{\FinMetric}{\mathbf{FinMetric}}
\newcommand{\Four}{\mathbbm{4}}
\newcommand{\Graph}{\mathbf{Graph}}
\newcommand{\GrMod}{\mathbf{GrMod}}
\newcommand{\Grp}{\mathbf{Grp}}
\newcommand{\Group}{\mathbf{Group}}
\newcommand{\Groupoid}{\mathbf{Groupoid}}
\newcommand{\Haus}{\mathbf{Haus}}
\newcommand{\Htpy}{\mathbf{Htpy}}
\newcommand{\Man}{\mathbf{Man}}
\newcommand{\Mapsdown}{\rotatebox{270}{$\mapsto$}}
\newcommand{\Mapsup}{\rotatebox{90}{$\mapsto$}}
\newcommand{\Mat}{\mathbf{Mat}}
\newcommand{\Meas}{\mathbf{Meas}}
\newcommand{\Measure}{\mathbf{Measure}}
\newcommand{\Mod}{\mathbf{Mod}}
\newcommand{\Model}{\mathbf{Model}}
\newcommand{\Mon}{\mathbf{Mon}}
\newcommand{\Monoid}{\mathbf{Monoid}}
\newcommand{\oMega}{\bbomega}
\newcommand{\One}{\mymathbb{1}}
\newcommand{\Ord}{\mathrm{Ord}}
\newcommand{\PCluster}{\mathbf{PCluster}}
\newcommand{\POs}{\mathbf{Poset}}
\newcommand{\Poset}{\mathbf{Poset}}
\newcommand{\PROJ}{\mathbf{Proj}}
\newcommand{\Psh}{\mathbf{Psh}}
\newcommand{\Ring}{\mathbf{Ring}}
\newcommand{\Rng}{\mathbf{Rng}}
\newcommand{\SET}{\mathbf{SET}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\setmid}{\mathrel{}\middle|\mathrel{}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Shv}{\mathbf{Shv}}
\newcommand{\Three}{\mymathbb{3}}
\renewcommand{\Top}{\mathbf{Top}}
\newcommand{\Two}{\mymathbb{2}}
\newcommand{\Vect}{\mathbf{Vect}}
\newcommand{\Zero}{\mymathbb{0}}
\newcommand{\sA}{\mathscr{A}}
\newcommand{\sB}{\mathscr{B}}
\newcommand{\sC}{\mathscr{C}}
\newcommand{\sD}{\mathscr{D}}
\newcommand{\sE}{\mathscr{E}}
\newcommand{\sF}{\mathscr{F}}
\newcommand{\sG}{\mathscr{G}}
\newcommand{\sH}{\mathscr{H}}
\newcommand{\sI}{\mathscr{I}}
\newcommand{\sJ}{\mathscr{J}}
\newcommand{\sK}{\mathscr{K}}
\newcommand{\sL}{\mathscr{L}}
\newcommand{\sM}{\mathscr{M}}
\newcommand{\sN}{\mathscr{N}}
\newcommand{\sO}{\mathscr{O}}
\newcommand{\sP}{\mathscr{P}}
\newcommand{\sQ}{\mathscr{Q}}
\newcommand{\sR}{\mathscr{R}}
\newcommand{\sS}{\mathscr{S}}
\newcommand{\sT}{\mathscr{T}}
\newcommand{\sU}{\mathscr{U}}
\newcommand{\sV}{\mathscr{V}}
\newcommand{\sW}{\mathscr{W}}
\newcommand{\sX}{\mathscr{X}}
\newcommand{\sY}{\mathscr{Y}}
\newcommand{\sZ}{\mathscr{Z}}
\newcommand{\bfA}{\mathbf{A}}
\newcommand{\bfB}{\mathbf{B}}
\newcommand{\bfC}{\mathbf{C}}
\newcommand{\bfD}{\mathbf{D}}
\newcommand{\bfE}{\mathbf{E}}
\newcommand{\bfF}{\mathbf{F}}
\newcommand{\bfG}{\mathbf{G}}
\newcommand{\bfH}{\mathbf{H}}
\newcommand{\bfI}{\mathbf{I}}
\newcommand{\bfJ}{\mathbf{J}}
\newcommand{\bfK}{\mathbf{K}}
\newcommand{\bfL}{\mathbf{L}}
\newcommand{\bfM}{\mathbf{M}}
\newcommand{\bfN}{\mathbf{N}}
\newcommand{\bfO}{\mathbf{O}}
\newcommand{\bfP}{\mathbf{P}}
\newcommand{\bfQ}{\mathbf{Q}}
\newcommand{\bfR}{\mathbf{R}}
\newcommand{\bfS}{\mathbf{S}}
\newcommand{\bfT}{\mathbf{T}}
\newcommand{\bfU}{\mathbf{U}}
\newcommand{\bfV}{\mathbf{V}}
\newcommand{\bfW}{\mathbf{W}}
\newcommand{\bfX}{\mathbf{X}}
\newcommand{\bfY}{\mathbf{Y}}
\newcommand{\bfZ}{\mathbf{Z}}
\newcommand{\bfa}{\mathbf{a}}
\newcommand{\bfb}{\mathbf{b}}
\newcommand{\bfc}{\mathbf{c}}
\newcommand{\bfd}{\mathbf{d}}
\newcommand{\bfe}{\mathbf{e}}
\newcommand{\bff}{\mathbf{f}}
\newcommand{\bfg}{\mathbf{g}}
\newcommand{\bfh}{\mathbf{h}}
\newcommand{\bfi}{\mathbf{i}}
\newcommand{\bfj}{\mathbf{j}}
\newcommand{\bfk}{\mathbf{k}}
\newcommand{\bfl}{\mathbf{l}}
\newcommand{\bfm}{\mathbf{m}}
\newcommand{\bfn}{\mathbf{n}}
\newcommand{\bfo}{\mathbf{o}}
\newcommand{\bfp}{\mathbf{p}}
\newcommand{\bfq}{\mathbf{q}}
\newcommand{\bfr}{\mathbf{r}}
\newcommand{\bfs}{\mathbf{s}}
\newcommand{\bft}{\mathbf{t}}
\newcommand{\bfu}{\mathbf{u}}
\newcommand{\bfv}{\mathbf{v}}
\newcommand{\bfw}{\mathbf{w}}
\newcommand{\bfx}{\mathbf{x}}
\newcommand{\bfy}{\mathbf{y}}
\newcommand{\bfz}{\mathbf{z}}
\newcommand{\frA}{\mathfrak{A}}
\newcommand{\frB}{\mathfrak{B}}
\newcommand{\frC}{\mathfrak{C}}
\newcommand{\frD}{\mathfrak{D}}
\newcommand{\frE}{\mathfrak{E}}
\newcommand{\frF}{\mathfrak{F}}
\newcommand{\frG}{\mathfrak{G}}
\newcommand{\frH}{\mathfrak{H}}
\newcommand{\frI}{\mathfrak{I}}
\newcommand{\frJ}{\mathfrak{J}}
\newcommand{\frK}{\mathfrak{K}}
\newcommand{\frL}{\mathfrak{L}}
\newcommand{\frM}{\mathfrak{M}}
\newcommand{\frN}{\mathfrak{N}}
\newcommand{\frO}{\mathfrak{O}}
\newcommand{\frP}{\mathfrak{P}}
\newcommand{\frQ}{\mathfrak{Q}}
\newcommand{\frR}{\mathfrak{R}}
\newcommand{\frS}{\mathfrak{S}}
\newcommand{\frT}{\mathfrak{T}}
\newcommand{\frU}{\mathfrak{U}}
\newcommand{\frV}{\mathfrak{V}}
\newcommand{\frW}{\mathfrak{W}}
\newcommand{\frX}{\mathfrak{X}}
\newcommand{\frY}{\mathfrak{Y}}
\newcommand{\frZ}{\mathfrak{Z}}
\newcommand{\Fra}{\mathfrak{a}}
\newcommand{\Frb}{\mathfrak{b}}
\newcommand{\Frc}{\mathfrak{c}}
\newcommand{\Frd}{\mathfrak{d}}
\newcommand{\Fre}{\mathfrak{e}}
\newcommand{\Frf}{\mathfrak{f}}
\newcommand{\Frg}{\mathfrak{g}}
\newcommand{\Frh}{\mathfrak{h}}
\newcommand{\Fri}{\mathfrak{i}}
\newcommand{\Frj}{\mathfrak{j}}
\newcommand{\Frk}{\mathfrak{k}}
\newcommand{\Frl}{\mathfrak{l}}
\newcommand{\Frm}{\mathfrak{m}}
\newcommand{\Frn}{\mathfrak{n}}
\newcommand{\Fro}{\mathfrak{o}}
\newcommand{\Frp}{\mathfrak{p}}
\newcommand{\Frq}{\mathfrak{q}}
\newcommand{\Frr}{\mathfrak{r}}
\newcommand{\Frs}{\mathfrak{s}}
\newcommand{\Frt}{\mathfrak{t}}
\newcommand{\Fru}{\mathfrak{u}}
\newcommand{\Frv}{\mathfrak{v}}
\newcommand{\Frw}{\mathfrak{w}}
\newcommand{\Frx}{\mathfrak{x}}
\newcommand{\Fry}{\mathfrak{y}}
\newcommand{\Frz}{\mathfrak{z}}
\newcommand{\rA}{\mathrm{A}}
\newcommand{\rB}{\mathrm{B}}
\newcommand{\rC}{\mathrm{C}}
\newcommand{\rD}{\mathrm{D}}
\newcommand{\rE}{\mathrm{E}}
\newcommand{\rF}{\mathrm{F}}
\newcommand{\rG}{\mathrm{G}}
\newcommand{\rH}{\mathrm{H}}
\newcommand{\rI}{\mathrm{I}}
\newcommand{\rJ}{\mathrm{J}}
\newcommand{\rK}{\mathrm{K}}
\newcommand{\rL}{\mathrm{L}}
\newcommand{\rM}{\mathrm{M}}
\newcommand{\rN}{\mathrm{N}}
\newcommand{\rO}{\mathrm{O}}
\newcommand{\rP}{\mathrm{P}}
\newcommand{\rQ}{\mathrm{Q}}
\newcommand{\rR}{\mathrm{R}}
\newcommand{\rS}{\mathrm{S}}
\newcommand{\rT}{\mathrm{T}}
\newcommand{\rU}{\mathrm{U}}
\newcommand{\rV}{\mathrm{V}}
\newcommand{\rW}{\mathrm{W}}
\newcommand{\rX}{\mathrm{X}}
\newcommand{\rY}{\mathrm{Y}}
\newcommand{\rZ}{\mathrm{Z}}
\newcommand{\sfA}{\mathsf{A}}
\newcommand{\sfB}{\mathsf{B}}
\newcommand{\sfC}{\mathsf{C}}
\newcommand{\sfD}{\mathsf{D}}
\newcommand{\sfE}{\mathsf{E}}
\newcommand{\sfF}{\mathsf{F}}
\newcommand{\sfG}{\mathsf{G}}
\newcommand{\sfH}{\mathsf{H}}
\newcommand{\sfI}{\mathsf{I}}
\newcommand{\sfJ}{\mathsf{J}}
\newcommand{\sfK}{\mathsf{K}}
\newcommand{\sfL}{\mathsf{L}}
\newcommand{\sfM}{\mathsf{M}}
\newcommand{\sfN}{\mathsf{N}}
\newcommand{\sfO}{\mathsf{O}}
\newcommand{\sfP}{\mathsf{P}}
\newcommand{\sfQ}{\mathsf{Q}}
\newcommand{\sfR}{\mathsf{R}}
\newcommand{\sfS}{\mathsf{S}}
\newcommand{\sfT}{\mathsf{T}}
\newcommand{\sfU}{\mathsf{U}}
\newcommand{\sfV}{\mathsf{V}}
\newcommand{\sfW}{\mathsf{W}}
\newcommand{\sfX}{\mathsf{X}}
\newcommand{\sfY}{\mathsf{Y}}
\newcommand{\sfZ}{\mathsf{Z}}
\newcommand{\bbA}{\mathbbm{A}}
\newcommand{\bbB}{\mathbbm{B}}
\newcommand{\bbC}{\mathbbm{C}}
\newcommand{\bbD}{\mathbbm{D}}
\newcommand{\bbE}{\mathbbm{E}}
\newcommand{\bbF}{\mathbbm{F}}
\newcommand{\bbG}{\mathbbm{G}}
\newcommand{\bbH}{\mathbbm{H}}
\newcommand{\bbI}{\mathbbm{I}}
\newcommand{\bbJ}{\mathbbm{J}}
\newcommand{\bbK}{\mathbbm{K}}
\newcommand{\bbL}{\mathbbm{L}}
\newcommand{\bbM}{\mathbbm{M}}
\newcommand{\bbN}{\mathbbm{N}}
\newcommand{\bbO}{\mathbbm{O}}
\newcommand{\bbP}{\mathbbm{P}}
\newcommand{\bbQ}{\mathbbm{Q}}
\newcommand{\bbR}{\mathbbm{R}}
\newcommand{\bbS}{\mathbbm{S}}
\newcommand{\bbT}{\mathbbm{T}}
\newcommand{\bbU}{\mathbbm{U}}
\newcommand{\bbV}{\mathbbm{V}}
\newcommand{\bbW}{\mathbbm{W}}
\newcommand{\bbX}{\mathbbm{X}}
\newcommand{\bbY}{\mathbbm{Y}}
\newcommand{\bbZ}{\mathbbm{Z}}
\newcommand{\bba}{\mathbbm{a}}
\newcommand{\bbb}{\mathbbm{b}}
\newcommand{\bbc}{\mathbbm{c}}
\newcommand{\bbd}{\mathbbm{d}}
\newcommand{\bbe}{\mathbbm{e}}
\newcommand{\bbf}{\mathbbm{f}}
\newcommand{\bbg}{\mathbbm{g}}
\newcommand{\bbh}{\mathbbm{h}}
\newcommand{\bbi}{\mathbbm{i}}
\newcommand{\bbj}{\mathbbm{j}}
\newcommand{\bbk}{\mathbbm{k}}
\newcommand{\bbl}{\mathbbm{l}}
\newcommand{\bbm}{\mathbbm{m}}
\newcommand{\bbn}{\mathbbm{n}}
\newcommand{\bbo}{\mathbbm{o}}
\newcommand{\bbp}{\mathbbm{p}}
\newcommand{\bbq}{\mathbbm{q}}
\newcommand{\bbr}{\mathbbm{r}}
\newcommand{\bbs}{\mathbbm{s}}
\newcommand{\bbt}{\mathbbm{t}}
\newcommand{\bbu}{\mathbbm{u}}
\newcommand{\bbv}{\mathbbm{v}}
\newcommand{\bbw}{\mathbbm{w}}
\newcommand{\bbx}{\mathbbm{x}}
\newcommand{\bby}{\mathbbm{y}}
\newcommand{\bbz}{\mathbbm{z}}
\newdir{ >}{{ }*!/-5pt/@{>}}
\eta_A : A \rightarrow (S \times A)^S, \qquad (\eta_A(a))(s) = (s,a)
\end{equation*} と定義される. 結果の $(s,a)$ を, 入力 $a \in A$ と現在の状態 $s \in S$ の対と考える.
また, 余単位 (counit) $\epsilon : S \times (-)^S \Rightarrow \Un{\Set}$ は状態 $s \in S$ と, 各状態における入力を与える関数 $f : S \rightarrow A$ とに対して,
\begin{equation*}
\epsilon_A : S \times A^S \rightarrow A, \qquad \epsilon_A(s,f) = f(s)
\end{equation*} と定義される. つまり, 各 $\epsilon_A : S \times A^S \rightarrow A$ は各状態における入力を与える評価関数 (evaluation function) と見なせる.
3 つ組 $((S\times-)^S,\eta,\mu)$ は図式に対する計算により
\begin{equation*}
\begin{xy}
\xymatrix@=36pt {
(S\times(S\times(S \times A)^S)^S)^S
\ar[r]^(.55){(S\times\mu_A)^S}
\ar[d]_{\mu_{(S \times A)^S}}
& (S\times(S \times A)^S)^S ->
\ar[d]^{\mu_A} \\
(S\times(S \times A)^S)^S
\ar[r]_{\mu_A}
& (S \times A)^S
}
\end{xy}
\qquad
\begin{xy}
\xymatrix@=36pt {
(S \times A)^S \ar[r]^(.4){\eta_{(S \times A)^S}} \ar[dr]_{\Un{(S \times A)^S}}
& (S\times(S \times A)^S)^S \ar[d]^{\mu_A}
& (S \times A)^S \ar[l]_(0.4){(S\times\eta_A)^S} \ar[dl]^{\Un{(S \times A)^S}} \\
& (S \times A)^S &
}
\end{xy}
\end{equation*}
を可換にし, 実際にモナドになっていることがわかる.
この余単位 $\epsilon$ を用いて, モナド $S\times(-)^S$ の積 (multiplication) $\mu : (S\times(S\times(-)^S))^S \Rightarrow (S\times-)^S$ を明示的に書き下してみる.
$\mu=(-)^S\epsilon(S\times-) : (S\times(S \times -)^S)^S \rightarrow (S\times-)^S$ である. $u \in (S\times(S \times A)^S)^S$ をとり, 状態 $s \in S$ に対して,
\begin{equation*}
u(s) = (u_1(s),u_2(s))
\end{equation*} とおく. $u_1(s) \in S$, $u_2(s) : S \rightarrow S \times A$ である.
$u_1(s)$ は状態 $s$ に対する新しい状態, $u_2(s)$ は状態 $s$ に対する新たな状態と入力の対を与える.
このとき,
\begin{equation*}
\mu_A(u)(s) = ((-)^S\epsilon(S\times-))_A(u))(s) = ((\epsilon_{S \times A})^S(u))(s) = \epsilon_{S \times A}(u(s)) = \epsilon_{S \times A}(u_1(s),u_2(s)) = u_2(s)(u_1(s))
\end{equation*} となる.

Kleisli 圏における対象は集合であり, この集合を状態の集まりであると考える.
Kleisli 圏 $\Set_{(S\times-)^S}$ における射 $f : A \rightsquigarrow B$ は $\rC$ における関数 $f : A \rightarrow (S \times B)^S$ であるが, この関数 $f$ は $f : A \times S \rightarrow B \times S$ と見なせる.
入力 $a$ と現在の状態 $s$ の対 $(a,s) \in A \times S$ に対して
\begin{equation*}
f(a,s) = (f_s(a), s'(a,s))
\end{equation*} とおく. このとき, $f_s(a)$ は入力と状態の対 $(a,s)$ によって決まる出力 $f_s(a) \in B$ と, アップデートされた状態 $s'(a,s) \in S$ の対と考えられる.
たとえば, 関数型プログラミング言語 Haskell においては, このアップデートされた状態 $s'(a,s)$ は計算 $f$ の「副作用 (side effect)」として扱われる.

タグ：数学の勉強モナド Kleisli 圏

posted by 底彦 at 17:23 | Comment(0) | TrackBack(0) | 数学

2023年07月13日

数学: モナドから導かれる随伴 (2) ── Kleisli 圏

モナド ── 定義と随伴により引き起こされるモナド ,
随伴から導かれるモナドの例 ── maybe モナド
モナドから導かれる随伴 (1) ── Eilenberg-Moore 圏の続き.

与えられたモナド $(T,\eta,\mu)$ から導かれる随伴として Eilenberg-Moore 圏を取り上げた.
ここでは, $(T,\eta,\mu)$ から導かれる別の随伴として, Kleisli 圏を定義する.

定義.$\mathrm{C}$ をモナド $(T,\eta,\mu)$ を持つ圏とする. Kleisli 圏 (Kleisli category)$\mathrm{C}_T$ は次のように構成される.
・ $\mathrm{C}$ の対象を $\mathrm{C}_T$ の対象とする.
・ $A$, $B$ を $\mathrm{C}_T$ の対象 (つまり圏 $\mathrm{C}$ の対象) とする. $\mathrm{C}_T$ における $A$ から $B$ への射 $f : A \rightsquigarrow B$ は, $\mathrm{C}$ における射 $f : A \rightarrow TB$ と定義する.
・ $\mathrm{C}_T$ の各対象 $A$ 上の恒等写像 (identity) は, 単位 $\eta_A : A \rightarrow TA$ とする.
・ $\mathrm{C}_T$ の 2 つの射 $f : A \rightsquigarrow B$, $g : B \rightsquigarrow C$ の合成 (これを $g \circ f$ と記すことにする) $g \circ f : A \rightsquigarrow C$ は, $\mathrm{C}$ における射の合成
\begin{equation*}
\DeclareMathOperator{\Aff}{Aff}
\DeclareMathOperator{\Ar}{Ar}
\DeclareMathOperator{\Arccos}{Arccos}
\DeclareMathOperator{\Arcsin}{Arcsin}
\DeclareMathOperator{\Arr}{Arr}
\DeclareMathOperator{\arr}{arr}
\DeclareMathOperator{\Aut}{Aut}
\DeclareMathOperator{\Auto}{Auto}
\DeclareMathOperator{\Axiom}{Axiom}
\DeclareMathOperator{\Bilin}{Bilin}
\DeclareMathOperator{\card}{card}
\DeclareMathOperator{\Catelem}{\int}
\DeclareMathOperator{\Cocone}{Cocone}
\DeclareMathOperator{\Cod}{cod}
\DeclareMathOperator{\Codomain}{cod}
\DeclareMathOperator{\Coin}{coin}
\DeclareMathOperator{\coker}{coker}
\DeclareMathOperator{\Colim}{colim}
\DeclareMathOperator{\comp}{comp}
\DeclareMathOperator{\Conf}{Conf}
\DeclareMathOperator{\Conj}{Conj}
\DeclareMathOperator{\Dom}{dom}
\DeclareMathOperator{\Domain}{dom}
\DeclareMathOperator{\Edge}{Edge}
\DeclareMathOperator{\Ev}{ev}
\DeclareMathOperator{\GCD}{gcd}
\DeclareMathOperator{\Gr}{Gr}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Id}{id}
\DeclareMathOperator{\IM}{Im}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\Ind}{ind}
\DeclareMathOperator{\INIT}{init}
\DeclareMathOperator{\iso}{iso}
\DeclareMathOperator{\LCM}{lcm}
\DeclareMathOperator{\Map}{Map}
\DeclareMathOperator{\mor}{arr}
\DeclareMathOperator{\Nat}{Nat}
\DeclareMathOperator{\Ob}{Ob}
\DeclareMathOperator{\ob}{ob}
\DeclareMathOperator{\ord}{ord}
\DeclareMathOperator{\Path}{Path}
\DeclareMathOperator{\PConf}{PConf}
\DeclareMathOperator{\Point}{Point}
\DeclareMathOperator{\Prob}{Prob}
\DeclareMathOperator{\RE}{Re}
\DeclareMathOperator{\Res}{res}
\DeclareMathOperator{\Sect}{Sect}
\DeclareMathOperator{\SF}{SF}
\DeclareMathOperator{\SkelCat}{sk}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Sq}{Sq}
\DeclareMathOperator{\Struct}{Struct}
\DeclareMathOperator{\Sub}{Sub}
\DeclareMathOperator{\Sym}{Sym}
\DeclareMathOperator{\TERM}{term}
\DeclareMathOperator{\Vertex}{Vert}
\newcommand{\Abs}[1]{\lvert{#1}\rvert}
\newcommand{\Bs}{\backslash}
\newcommand{\Cdot}{\,\cdot^{\mathrm{op}}}
\newcommand{\Comma}[2]{{{#1}\!\downarrow\!{#2}}}
\newcommand{\CommaCat}[2]{(#1/#2)}
\newcommand{\Complement}[1]{{\smash[t]{\mathstrut #1}}^{\mathrm{c}}}
\newcommand{\Emph}[1]{\textit{#1}}
\newcommand{\Eqclass}[4]{{#1#2#3}_{#4}}
\newcommand{\EqCls}[2]{{\left[#1\right]}_{#2}}
\newcommand{\Eqcls}[1]{\left[#1\right]}
\newcommand{\Expt}[2]{{\smash[t]{\mathstrut #1}}^{\mathstrut #2}}
\newcommand{\FnRest}[2]{{#1}|{#2}}
\newcommand{\Func}[2]{\mathrm{Func}(#1,#2)}
\newcommand{\g}{\varg}
\newcommand{\Inc}[2]{\mathrm{incl}\left(#1,#2\right)}
\newcommand{\Incl}[2]{\mathrm{incl}_{#1}^{#2}}
\newcommand{\InclArrow}[2]{\morphism(0,0)/>->/<450,0>[\Incl{#1}{#2} : {#1}\,\,`{#2};]}
\newcommand{\Ip}{\amalg}
\newcommand{\Lb}[1]{\mathrm{lb}(#1)}
\newcommand{\LH}{\mathrm{LH}}
\newcommand{\Lowerset}[1]{\downarrow\!\!{#1}}
\newcommand{\Leadsto}{\quad\leadsto\quad}
\newcommand{\Lrsquigarrow}{\quad\leftrightsquigarrow\quad}
\newcommand{\Mb}[1]{\mathbf{#1}}
\newcommand{\Mbb}[1]{\mathbb{#1}}
\newcommand{\Mi}[1]{\mathit{#1}}
\newcommand{\Mlb}[1]{\mathrm{mlb}(#1)}
\newcommand{\Mr}[1]{\mathrm{#1}}
\newcommand{\Ms}[1]{\mathscr{#1}}
\newcommand{\Mt}[1]{\mathtt{#1}}
\newcommand{\Mub}[1]{\mathrm{mub}(#1)}
\newcommand{\newinf}{\mathop{\mathrm{inf}\vphantom{\mathrm{sup}}}}
\newcommand{\newsup}{\mathop{\smash{\mathrm{sup}}}}
\newcommand{\Opp}[1]{#1^{\mathrm{op}}}
\newcommand{\Prj}[2]{\mathrm{proj}\left(#1,#2\right)}
\newcommand{\Proj}[2]{\mathrm{proj}^{#1}_{#2}}
\newcommand{\Pw}{\mathbf{P}}
\newcommand{\Rn}[1]{{\bmdefine{R}}^{#1}}
\newcommand{\q}{\hspace{1em}}
\newcommand{\qq}{\hspace{0.5em}}
\newcommand{\Rel}[1]{\langle{#1}\rangle}
\newcommand{\Rest}[2]{{#1}|{#2}}
\newcommand{\Slash}[1]{{\ooalign{\hfil/\hfil\crcr$#1$}}}
\newcommand{\SliCat}[2]{{#1}\,\big/\,{#2}}
\newcommand{\Src}{d^{0,\mathrm{op}}}
\newcommand{\ssqrt}[1]{\sqrt{\smash[b]{\mathstrut #1}}}
\newcommand{\Tgt}{d^{1,\mathrm{op}}}
\newcommand{\TwArCat}[1]{\mathrm{Tw}(#1)}
\newcommand{\Ub}[1]{\mathrm{ub}(#1)}
\newcommand{\Un}[1]{{1}_{#1}}
\newcommand{\Upperset}[1]{\uparrow\!\!{#1}}
\newcommand{\VectCat}[1]{#1 \mathchar`- \mathbf{Vect}}
\newcommand{\VS}{\vspace*{-1ex}}
\newcommand{\Wbar}[1]{\widebar{#1}}
\newcommand{\Ab}{\mathbf{Ab}}
\newcommand{\Adj}{\mathbf{Adj}}
\newcommand{\Affine}{\mathbf{Affine}}
\newcommand{\Ban}{\mathbf{Ban}}
\newcommand{\bbDelta}{\Delta\mkern-12mu\Delta}
\newcommand{\Card}{\mathbf{Card}}
\newcommand{\CAT}{\mathbf{CAT}}
\newcommand{\Cat}{\mathbf{Cat}}
\newcommand{\cgHaus}{\mathbf{cgHaus}}
\newcommand{\Ch}{\mathbf{Ch}}
\newcommand{\cHaus}{\mathbf{cHaus}}
\newcommand{\Cluster}{\mathbf{Cluster}}
\newcommand{\CMonoid}{\mathbf{CMonoid}}
\newcommand{\CRing}{\mathbf{CRing}}
\newcommand{\DirGraph}{\mathbf{DirGraph}}
\newcommand{\End}{\mathbf{End}}
\newcommand{\Euclid}{\mathbf{Euclid}}
\newcommand{\Field}{\mathbf{Field}}
\newcommand{\Fin}{\mathbf{Fin}}
\newcommand{\FinMetric}{\mathbf{FinMetric}}
\newcommand{\Four}{\mathbbm{4}}
\newcommand{\Graph}{\mathbf{Graph}}
\newcommand{\GrMod}{\mathbf{GrMod}}
\newcommand{\Grp}{\mathbf{Grp}}
\newcommand{\Group}{\mathbf{Group}}
\newcommand{\Groupoid}{\mathbf{Groupoid}}
\newcommand{\Haus}{\mathbf{Haus}}
\newcommand{\Htpy}{\mathbf{Htpy}}
\newcommand{\Man}{\mathbf{Man}}
\newcommand{\Mapsdown}{\rotatebox{270}{$\mapsto$}}
\newcommand{\Mapsup}{\rotatebox{90}{$\mapsto$}}
\newcommand{\Mat}{\mathbf{Mat}}
\newcommand{\Meas}{\mathbf{Meas}}
\newcommand{\Measure}{\mathbf{Measure}}
\newcommand{\Mod}{\mathbf{Mod}}
\newcommand{\Model}{\mathbf{Model}}
\newcommand{\Mon}{\mathbf{Mon}}
\newcommand{\Monoid}{\mathbf{Monoid}}
\newcommand{\oMega}{\bbomega}
\newcommand{\One}{\mymathbb{1}}
\newcommand{\Ord}{\mathrm{Ord}}
\newcommand{\PCluster}{\mathbf{PCluster}}
\newcommand{\POs}{\mathbf{Poset}}
\newcommand{\Poset}{\mathbf{Poset}}
\newcommand{\PROJ}{\mathbf{Proj}}
\newcommand{\Psh}{\mathbf{Psh}}
\newcommand{\Ring}{\mathbf{Ring}}
\newcommand{\Rng}{\mathbf{Rng}}
\newcommand{\SET}{\mathbf{SET}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\setmid}{\mathrel{}\middle|\mathrel{}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Shv}{\mathbf{Shv}}
\newcommand{\Three}{\mymathbb{3}}
\renewcommand{\Top}{\mathbf{Top}}
\newcommand{\Two}{\mymathbb{2}}
\newcommand{\Vect}{\mathbf{Vect}}
\newcommand{\Zero}{\mymathbb{0}}
\newcommand{\sA}{\mathscr{A}}
\newcommand{\sB}{\mathscr{B}}
\newcommand{\sC}{\mathscr{C}}
\newcommand{\sD}{\mathscr{D}}
\newcommand{\sE}{\mathscr{E}}
\newcommand{\sF}{\mathscr{F}}
\newcommand{\sG}{\mathscr{G}}
\newcommand{\sH}{\mathscr{H}}
\newcommand{\sI}{\mathscr{I}}
\newcommand{\sJ}{\mathscr{J}}
\newcommand{\sK}{\mathscr{K}}
\newcommand{\sL}{\mathscr{L}}
\newcommand{\sM}{\mathscr{M}}
\newcommand{\sN}{\mathscr{N}}
\newcommand{\sO}{\mathscr{O}}
\newcommand{\sP}{\mathscr{P}}
\newcommand{\sQ}{\mathscr{Q}}
\newcommand{\sR}{\mathscr{R}}
\newcommand{\sS}{\mathscr{S}}
\newcommand{\sT}{\mathscr{T}}
\newcommand{\sU}{\mathscr{U}}
\newcommand{\sV}{\mathscr{V}}
\newcommand{\sW}{\mathscr{W}}
\newcommand{\sX}{\mathscr{X}}
\newcommand{\sY}{\mathscr{Y}}
\newcommand{\sZ}{\mathscr{Z}}
\newcommand{\bfA}{\mathbf{A}}
\newcommand{\bfB}{\mathbf{B}}
\newcommand{\bfC}{\mathbf{C}}
\newcommand{\bfD}{\mathbf{D}}
\newcommand{\bfE}{\mathbf{E}}
\newcommand{\bfF}{\mathbf{F}}
\newcommand{\bfG}{\mathbf{G}}
\newcommand{\bfH}{\mathbf{H}}
\newcommand{\bfI}{\mathbf{I}}
\newcommand{\bfJ}{\mathbf{J}}
\newcommand{\bfK}{\mathbf{K}}
\newcommand{\bfL}{\mathbf{L}}
\newcommand{\bfM}{\mathbf{M}}
\newcommand{\bfN}{\mathbf{N}}
\newcommand{\bfO}{\mathbf{O}}
\newcommand{\bfP}{\mathbf{P}}
\newcommand{\bfQ}{\mathbf{Q}}
\newcommand{\bfR}{\mathbf{R}}
\newcommand{\bfS}{\mathbf{S}}
\newcommand{\bfT}{\mathbf{T}}
\newcommand{\bfU}{\mathbf{U}}
\newcommand{\bfV}{\mathbf{V}}
\newcommand{\bfW}{\mathbf{W}}
\newcommand{\bfX}{\mathbf{X}}
\newcommand{\bfY}{\mathbf{Y}}
\newcommand{\bfZ}{\mathbf{Z}}
\newcommand{\bfa}{\mathbf{a}}
\newcommand{\bfb}{\mathbf{b}}
\newcommand{\bfc}{\mathbf{c}}
\newcommand{\bfd}{\mathbf{d}}
\newcommand{\bfe}{\mathbf{e}}
\newcommand{\bff}{\mathbf{f}}
\newcommand{\bfg}{\mathbf{g}}
\newcommand{\bfh}{\mathbf{h}}
\newcommand{\bfi}{\mathbf{i}}
\newcommand{\bfj}{\mathbf{j}}
\newcommand{\bfk}{\mathbf{k}}
\newcommand{\bfl}{\mathbf{l}}
\newcommand{\bfm}{\mathbf{m}}
\newcommand{\bfn}{\mathbf{n}}
\newcommand{\bfo}{\mathbf{o}}
\newcommand{\bfp}{\mathbf{p}}
\newcommand{\bfq}{\mathbf{q}}
\newcommand{\bfr}{\mathbf{r}}
\newcommand{\bfs}{\mathbf{s}}
\newcommand{\bft}{\mathbf{t}}
\newcommand{\bfu}{\mathbf{u}}
\newcommand{\bfv}{\mathbf{v}}
\newcommand{\bfw}{\mathbf{w}}
\newcommand{\bfx}{\mathbf{x}}
\newcommand{\bfy}{\mathbf{y}}
\newcommand{\bfz}{\mathbf{z}}
\newcommand{\frA}{\mathfrak{A}}
\newcommand{\frB}{\mathfrak{B}}
\newcommand{\frC}{\mathfrak{C}}
\newcommand{\frD}{\mathfrak{D}}
\newcommand{\frE}{\mathfrak{E}}
\newcommand{\frF}{\mathfrak{F}}
\newcommand{\frG}{\mathfrak{G}}
\newcommand{\frH}{\mathfrak{H}}
\newcommand{\frI}{\mathfrak{I}}
\newcommand{\frJ}{\mathfrak{J}}
\newcommand{\frK}{\mathfrak{K}}
\newcommand{\frL}{\mathfrak{L}}
\newcommand{\frM}{\mathfrak{M}}
\newcommand{\frN}{\mathfrak{N}}
\newcommand{\frO}{\mathfrak{O}}
\newcommand{\frP}{\mathfrak{P}}
\newcommand{\frQ}{\mathfrak{Q}}
\newcommand{\frR}{\mathfrak{R}}
\newcommand{\frS}{\mathfrak{S}}
\newcommand{\frT}{\mathfrak{T}}
\newcommand{\frU}{\mathfrak{U}}
\newcommand{\frV}{\mathfrak{V}}
\newcommand{\frW}{\mathfrak{W}}
\newcommand{\frX}{\mathfrak{X}}
\newcommand{\frY}{\mathfrak{Y}}
\newcommand{\frZ}{\mathfrak{Z}}
\newcommand{\Fra}{\mathfrak{a}}
\newcommand{\Frb}{\mathfrak{b}}
\newcommand{\Frc}{\mathfrak{c}}
\newcommand{\Frd}{\mathfrak{d}}
\newcommand{\Fre}{\mathfrak{e}}
\newcommand{\Frf}{\mathfrak{f}}
\newcommand{\Frg}{\mathfrak{g}}
\newcommand{\Frh}{\mathfrak{h}}
\newcommand{\Fri}{\mathfrak{i}}
\newcommand{\Frj}{\mathfrak{j}}
\newcommand{\Frk}{\mathfrak{k}}
\newcommand{\Frl}{\mathfrak{l}}
\newcommand{\Frm}{\mathfrak{m}}
\newcommand{\Frn}{\mathfrak{n}}
\newcommand{\Fro}{\mathfrak{o}}
\newcommand{\Frp}{\mathfrak{p}}
\newcommand{\Frq}{\mathfrak{q}}
\newcommand{\Frr}{\mathfrak{r}}
\newcommand{\Frs}{\mathfrak{s}}
\newcommand{\Frt}{\mathfrak{t}}
\newcommand{\Fru}{\mathfrak{u}}
\newcommand{\Frv}{\mathfrak{v}}
\newcommand{\Frw}{\mathfrak{w}}
\newcommand{\Frx}{\mathfrak{x}}
\newcommand{\Fry}{\mathfrak{y}}
\newcommand{\Frz}{\mathfrak{z}}
\newcommand{\rA}{\mathrm{A}}
\newcommand{\rB}{\mathrm{B}}
\newcommand{\rC}{\mathrm{C}}
\newcommand{\rD}{\mathrm{D}}
\newcommand{\rE}{\mathrm{E}}
\newcommand{\rF}{\mathrm{F}}
\newcommand{\rG}{\mathrm{G}}
\newcommand{\rH}{\mathrm{H}}
\newcommand{\rI}{\mathrm{I}}
\newcommand{\rJ}{\mathrm{J}}
\newcommand{\rK}{\mathrm{K}}
\newcommand{\rL}{\mathrm{L}}
\newcommand{\rM}{\mathrm{M}}
\newcommand{\rN}{\mathrm{N}}
\newcommand{\rO}{\mathrm{O}}
\newcommand{\rP}{\mathrm{P}}
\newcommand{\rQ}{\mathrm{Q}}
\newcommand{\rR}{\mathrm{R}}
\newcommand{\rS}{\mathrm{S}}
\newcommand{\rT}{\mathrm{T}}
\newcommand{\rU}{\mathrm{U}}
\newcommand{\rV}{\mathrm{V}}
\newcommand{\rW}{\mathrm{W}}
\newcommand{\rX}{\mathrm{X}}
\newcommand{\rY}{\mathrm{Y}}
\newcommand{\rZ}{\mathrm{Z}}
\newcommand{\sfA}{\mathsf{A}}
\newcommand{\sfB}{\mathsf{B}}
\newcommand{\sfC}{\mathsf{C}}
\newcommand{\sfD}{\mathsf{D}}
\newcommand{\sfE}{\mathsf{E}}
\newcommand{\sfF}{\mathsf{F}}
\newcommand{\sfG}{\mathsf{G}}
\newcommand{\sfH}{\mathsf{H}}
\newcommand{\sfI}{\mathsf{I}}
\newcommand{\sfJ}{\mathsf{J}}
\newcommand{\sfK}{\mathsf{K}}
\newcommand{\sfL}{\mathsf{L}}
\newcommand{\sfM}{\mathsf{M}}
\newcommand{\sfN}{\mathsf{N}}
\newcommand{\sfO}{\mathsf{O}}
\newcommand{\sfP}{\mathsf{P}}
\newcommand{\sfQ}{\mathsf{Q}}
\newcommand{\sfR}{\mathsf{R}}
\newcommand{\sfS}{\mathsf{S}}
\newcommand{\sfT}{\mathsf{T}}
\newcommand{\sfU}{\mathsf{U}}
\newcommand{\sfV}{\mathsf{V}}
\newcommand{\sfW}{\mathsf{W}}
\newcommand{\sfX}{\mathsf{X}}
\newcommand{\sfY}{\mathsf{Y}}
\newcommand{\sfZ}{\mathsf{Z}}
\newcommand{\bbA}{\mathbbm{A}}
\newcommand{\bbB}{\mathbbm{B}}
\newcommand{\bbC}{\mathbbm{C}}
\newcommand{\bbD}{\mathbbm{D}}
\newcommand{\bbE}{\mathbbm{E}}
\newcommand{\bbF}{\mathbbm{F}}
\newcommand{\bbG}{\mathbbm{G}}
\newcommand{\bbH}{\mathbbm{H}}
\newcommand{\bbI}{\mathbbm{I}}
\newcommand{\bbJ}{\mathbbm{J}}
\newcommand{\bbK}{\mathbbm{K}}
\newcommand{\bbL}{\mathbbm{L}}
\newcommand{\bbM}{\mathbbm{M}}
\newcommand{\bbN}{\mathbbm{N}}
\newcommand{\bbO}{\mathbbm{O}}
\newcommand{\bbP}{\mathbbm{P}}
\newcommand{\bbQ}{\mathbbm{Q}}
\newcommand{\bbR}{\mathbbm{R}}
\newcommand{\bbS}{\mathbbm{S}}
\newcommand{\bbT}{\mathbbm{T}}
\newcommand{\bbU}{\mathbbm{U}}
\newcommand{\bbV}{\mathbbm{V}}
\newcommand{\bbW}{\mathbbm{W}}
\newcommand{\bbX}{\mathbbm{X}}
\newcommand{\bbY}{\mathbbm{Y}}
\newcommand{\bbZ}{\mathbbm{Z}}
\newcommand{\bba}{\mathbbm{a}}
\newcommand{\bbb}{\mathbbm{b}}
\newcommand{\bbc}{\mathbbm{c}}
\newcommand{\bbd}{\mathbbm{d}}
\newcommand{\bbe}{\mathbbm{e}}
\newcommand{\bbf}{\mathbbm{f}}
\newcommand{\bbg}{\mathbbm{g}}
\newcommand{\bbh}{\mathbbm{h}}
\newcommand{\bbi}{\mathbbm{i}}
\newcommand{\bbj}{\mathbbm{j}}
\newcommand{\bbk}{\mathbbm{k}}
\newcommand{\bbl}{\mathbbm{l}}
\newcommand{\bbm}{\mathbbm{m}}
\newcommand{\bbn}{\mathbbm{n}}
\newcommand{\bbo}{\mathbbm{o}}
\newcommand{\bbp}{\mathbbm{p}}
\newcommand{\bbq}{\mathbbm{q}}
\newcommand{\bbr}{\mathbbm{r}}
\newcommand{\bbs}{\mathbbm{s}}
\newcommand{\bbt}{\mathbbm{t}}
\newcommand{\bbu}{\mathbbm{u}}
\newcommand{\bbv}{\mathbbm{v}}
\newcommand{\bbw}{\mathbbm{w}}
\newcommand{\bbx}{\mathbbm{x}}
\newcommand{\bby}{\mathbbm{y}}
\newcommand{\bbz}{\mathbbm{z}}
\newdir{ >}{{ }*!/-5pt/@{>}}
\begin{xy}
\xymatrix@=32pt {
A \ar[r]^f & TB \ar[r]^{Tg} & T^2C \ar[r]^{\mu_C} & TC
}
\end{xy}
\end{equation*} と定義する.

これで $\rC_T$ は圏になる.
たとえば実際に各 $\eta_A$ が $\rC_T$ の恒等射になっていることは以下のようにしてわかる.
$f : A \rightsquigarrow B$ を $\rC_T$ の任意の射とする. $\eta : \Un{\rC} \Rightarrow T$ が自然変換であることより, 図式
\begin{equation*}
\begin{xy}
\xymatrix@=32pt {
A \ar[r]^{\eta_A} \ar[d]_f & TA \ar[d]^{Tf} \\
TB \ar[r]_{\eta_{TB}} & T^2B
}
\end{xy}
\end{equation*} は可換である. また, モナドの定義から図式
\begin{equation*}
\begin{xy}
\xymatrix@=32pt {
TB \ar[r]^{\eta_{TB}} \ar[dr]_{\Un{TB}} & T^2B \ar[d]^{\mu_B} & TB \ar[l]_{T\eta_B} \ar[dl]^{\Un{TB}} \\
& TB &
}
\end{xy}
\end{equation*} は可換である. これらの図式の可換性により
\begin{gather*}
f \circ \eta_A = \mu_B \cdot Tf \cdot \eta_A = \mu_B \cdot \eta_{TB} \cdot f = \Un{TB} \cdot f = f, \\
\eta_B \circ f = \mu_B \cdot T\eta_B \cdot f = \Un{B} \cdot f = f
\end{gather*} が成り立つ. よって各 $\eta_A : A \rightarrow TA$ は Kleisli 圏 $\rC_T$ の恒等射である.

例.集合の圏 $\Set$ 上の maybe モナド $(T,\eta,\mu)=((-)_+,\eta,\mu)$ に対する Kleisli 圏 $\Set_{(-)_+}$を考える.
$\Set_{(-)_+}$ の対象は $\Set$ の対象, すなわち集合である.
$\Set_{(-)_+}$ の射 $f : A \rightsquigarrow B$ は $\Set$ の関数 $f : A \rightarrow B_+=B\amalg\{\bot_B\}$ である. この $f$ は, 次のようにして $A$ から $B$ への部分関数 (partial function), つまり $A$ の部分集合上で定義された関数と解釈することができる. $f$ を $A$ の部分集合
\begin{equation*}
A' = \{ a \in A \mid f(a) \in B \}
\end{equation*} 上でのみ定義された関数として考える. このとき補集合 $A \Bs A'$ の元は全て $\bot_B$ に移される. これらの元に対しては $f$ は未定義 (undefined) であると考える. これによって, $A'$ の元をプログラム $f$ への正常な入力, $A \Bs A'$ の元を $f$ への予期せぬ入力と見ることができる. 正常な入力 $a \in A'$ に対して $f$ は正常な出力 $f(a) \in B$ を返し, 予期せぬ入力 $a \in A \Bs A'$ に対して $f$ はエラー $\bot_B \in B_+$ を返す.
したがって, maybe モナドの Kleisli 圏は, 集合と部分関数からなる圏 $\Set^{\partial}$ と見なせる.

タグ：圏論モナド Kleisli 圏

posted by 底彦 at 17:46 | Comment(0) | TrackBack(0) | 数学

2023年06月24日

数学: モナドから導かれる随伴 (1) ── Eilenberg-Moore 圏

モナド ── 定義と随伴により引き起こされるモナド ,
随伴から導かれるモナドの例 ── maybe モナドの続き.

随伴が与えられたとき, そこからモナドが構成されることを見た.
ではその逆, つまりモナドが与えられたときに何らかの仕方でそのモナドを導くような随伴を構成できるかという問題が生じる.
これに対しては, 圏 $\mathrm{C}$ 上の与えられたモナドから少なくとも 2 種類の随伴を構成できることが示せる.
1 つは Eilenbert-Moore 圏と $\mathrm{C}$ の間の随伴であり, もう 1 つは Kleisli 圏と $\mathrm{C}$ の間の随伴である.
これらは, モナド $T$ を導く全ての随伴からなる圏 $\mathbf{Adj}_T$ を考えたときに, それぞれそこにおける終対象と始対象になっている.

Eilenberg-Moore 圏を定義する.

定義.$\mathrm{C}$ をモナド $(T,\eta,\mu)$ を持つような圏とする. $T$ 上の Eilenberg-Moore 圏 (Eilenberg-Moore category)または $T$-代数の圏 (category of $T$-algebras)$\mathrm{C}^T$ を次のように構成する.
・ $\mathrm{C}$ の対象 $A$ と射 $a : TA \rightarrow A$ で, 図式
\begin{equation*}
\label{Eilenberg-Moore-category}
\DeclareMathOperator{\Aff}{Aff}
\DeclareMathOperator{\Ar}{Ar}
\DeclareMathOperator{\Arccos}{Arccos}
\DeclareMathOperator{\Arcsin}{Arcsin}
\DeclareMathOperator{\Arr}{Arr}
\DeclareMathOperator{\arr}{arr}
\DeclareMathOperator{\Aut}{Aut}
\DeclareMathOperator{\Auto}{Auto}
\DeclareMathOperator{\Axiom}{Axiom}
\DeclareMathOperator{\Bilin}{Bilin}
\DeclareMathOperator{\card}{card}
\DeclareMathOperator{\Catelem}{\int}
\DeclareMathOperator{\Cocone}{Cocone}
\DeclareMathOperator{\Cod}{cod}
\DeclareMathOperator{\Codomain}{cod}
\DeclareMathOperator{\Coin}{coin}
\DeclareMathOperator{\coker}{coker}
\DeclareMathOperator{\Colim}{colim}
\DeclareMathOperator{\comp}{comp}
\DeclareMathOperator{\Conf}{Conf}
\DeclareMathOperator{\Conj}{Conj}
\DeclareMathOperator{\Dom}{dom}
\DeclareMathOperator{\Domain}{dom}
\DeclareMathOperator{\Edge}{Edge}
\DeclareMathOperator{\Ev}{ev}
\DeclareMathOperator{\GCD}{gcd}
\DeclareMathOperator{\Gr}{Gr}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Id}{id}
\DeclareMathOperator{\IM}{Im}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\Ind}{ind}
\DeclareMathOperator{\INIT}{init}
\DeclareMathOperator{\iso}{iso}
\DeclareMathOperator{\LCM}{lcm}
\DeclareMathOperator{\Map}{Map}
\DeclareMathOperator{\mor}{arr}
\DeclareMathOperator{\Nat}{Nat}
\DeclareMathOperator{\Ob}{Ob}
\DeclareMathOperator{\ob}{ob}
\DeclareMathOperator{\ord}{ord}
\DeclareMathOperator{\Path}{Path}
\DeclareMathOperator{\PConf}{PConf}
\DeclareMathOperator{\Point}{Point}
\DeclareMathOperator{\Prob}{Prob}
\DeclareMathOperator{\RE}{Re}
\DeclareMathOperator{\Res}{res}
\DeclareMathOperator{\Sect}{Sect}
\DeclareMathOperator{\SF}{SF}
\DeclareMathOperator{\SkelCat}{sk}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Sq}{Sq}
\DeclareMathOperator{\Struct}{Struct}
\DeclareMathOperator{\Sub}{Sub}
\DeclareMathOperator{\Sym}{Sym}
\DeclareMathOperator{\TERM}{term}
\DeclareMathOperator{\Vertex}{Vert}
\newcommand{\Abs}[1]{\lvert{#1}\rvert}
\newcommand{\Bs}{\backslash}
\newcommand{\Cdot}{\,\cdot^{\mathrm{op}}}
\newcommand{\Comma}[2]{{{#1}\!\downarrow\!{#2}}}
\newcommand{\CommaCat}[2]{(#1/#2)}
\newcommand{\Complement}[1]{{\smash[t]{\mathstrut #1}}^{\mathrm{c}}}
\newcommand{\Emph}[1]{\textit{#1}}
\newcommand{\Eqclass}[4]{{#1#2#3}_{#4}}
\newcommand{\EqCls}[2]{{\left[#1\right]}_{#2}}
\newcommand{\Eqcls}[1]{\left[#1\right]}
\newcommand{\Expt}[2]{{\smash[t]{\mathstrut #1}}^{\mathstrut #2}}
\newcommand{\FnRest}[2]{{#1}|{#2}}
\newcommand{\Func}[2]{\mathrm{Func}(#1,#2)}
\newcommand{\g}{\varg}
\newcommand{\Inc}[2]{\mathrm{incl}\left(#1,#2\right)}
\newcommand{\Incl}[2]{\mathrm{incl}_{#1}^{#2}}
\newcommand{\InclArrow}[2]{\morphism(0,0)/>->/<450,0>[\Incl{#1}{#2} : {#1}\,\,`{#2};]}
\newcommand{\Ip}{\amalg}
\newcommand{\Lb}[1]{\mathrm{lb}(#1)}
\newcommand{\LH}{\mathrm{LH}}
\newcommand{\Lowerset}[1]{\downarrow\!\!{#1}}
\newcommand{\Leadsto}{\quad\leadsto\quad}
\newcommand{\Lrsquigarrow}{\quad\leftrightsquigarrow\quad}
\newcommand{\Mb}[1]{\mathbf{#1}}
\newcommand{\Mbb}[1]{\mathbb{#1}}
\newcommand{\Mi}[1]{\mathit{#1}}
\newcommand{\Mlb}[1]{\mathrm{mlb}(#1)}
\newcommand{\Mr}[1]{\mathrm{#1}}
\newcommand{\Ms}[1]{\mathscr{#1}}
\newcommand{\Mt}[1]{\mathtt{#1}}
\newcommand{\Mub}[1]{\mathrm{mub}(#1)}
\newcommand{\newinf}{\mathop{\mathrm{inf}\vphantom{\mathrm{sup}}}}
\newcommand{\newsup}{\mathop{\smash{\mathrm{sup}}}}
\newcommand{\Opp}[1]{#1^{\mathrm{op}}}
\newcommand{\Prj}[2]{\mathrm{proj}\left(#1,#2\right)}
\newcommand{\Proj}[2]{\mathrm{proj}^{#1}_{#2}}
\newcommand{\Pw}{\mathbf{P}}
\newcommand{\Rn}[1]{{\bmdefine{R}}^{#1}}
\newcommand{\q}{\hspace{1em}}
\newcommand{\qq}{\hspace{0.5em}}
\newcommand{\Rel}[1]{\langle{#1}\rangle}
\newcommand{\Rest}[2]{{#1}|{#2}}
\newcommand{\Slash}[1]{{\ooalign{\hfil/\hfil\crcr$#1$}}}
\newcommand{\SliCat}[2]{{#1}\,\big/\,{#2}}
\newcommand{\Src}{d^{0,\mathrm{op}}}
\newcommand{\ssqrt}[1]{\sqrt{\smash[b]{\mathstrut #1}}}
\newcommand{\Tgt}{d^{1,\mathrm{op}}}
\newcommand{\TwArCat}[1]{\mathrm{Tw}(#1)}
\newcommand{\Ub}[1]{\mathrm{ub}(#1)}
\newcommand{\Un}[1]{{1}_{#1}}
\newcommand{\Upperset}[1]{\uparrow\!\!{#1}}
\newcommand{\VectCat}[1]{#1 \mathchar`- \mathbf{Vect}}
\newcommand{\VS}{\vspace*{-1ex}}
\newcommand{\Wbar}[1]{\widebar{#1}}
\newcommand{\Ab}{\mathbf{Ab}}
\newcommand{\Adj}{\mathbf{Adj}}
\newcommand{\Affine}{\mathbf{Affine}}
\newcommand{\Ban}{\mathbf{Ban}}
\newcommand{\bbDelta}{\Delta\mkern-12mu\Delta}
\newcommand{\Card}{\mathbf{Card}}
\newcommand{\CAT}{\mathbf{CAT}}
\newcommand{\Cat}{\mathbf{Cat}}
\newcommand{\cgHaus}{\mathbf{cgHaus}}
\newcommand{\Ch}{\mathbf{Ch}}
\newcommand{\cHaus}{\mathbf{cHaus}}
\newcommand{\Cluster}{\mathbf{Cluster}}
\newcommand{\CMonoid}{\mathbf{CMonoid}}
\newcommand{\CRing}{\mathbf{CRing}}
\newcommand{\DirGraph}{\mathbf{DirGraph}}
\newcommand{\End}{\mathbf{End}}
\newcommand{\Euclid}{\mathbf{Euclid}}
\newcommand{\Field}{\mathbf{Field}}
\newcommand{\Fin}{\mathbf{Fin}}
\newcommand{\FinMetric}{\mathbf{FinMetric}}
\newcommand{\Four}{\mathbbm{4}}
\newcommand{\Graph}{\mathbf{Graph}}
\newcommand{\GrMod}{\mathbf{GrMod}}
\newcommand{\Grp}{\mathbf{Grp}}
\newcommand{\Group}{\mathbf{Group}}
\newcommand{\Groupoid}{\mathbf{Groupoid}}
\newcommand{\Haus}{\mathbf{Haus}}
\newcommand{\Htpy}{\mathbf{Htpy}}
\newcommand{\Man}{\mathbf{Man}}
\newcommand{\Mapsdown}{\rotatebox{270}{$\mapsto$}}
\newcommand{\Mapsup}{\rotatebox{90}{$\mapsto$}}
\newcommand{\Mat}{\mathbf{Mat}}
\newcommand{\Meas}{\mathbf{Meas}}
\newcommand{\Measure}{\mathbf{Measure}}
\newcommand{\Mod}{\mathbf{Mod}}
\newcommand{\Model}{\mathbf{Model}}
\newcommand{\Mon}{\mathbf{Mon}}
\newcommand{\Monoid}{\mathbf{Monoid}}
\newcommand{\oMega}{\bbomega}
\newcommand{\One}{\mymathbb{1}}
\newcommand{\Ord}{\mathrm{Ord}}
\newcommand{\PCluster}{\mathbf{PCluster}}
\newcommand{\POs}{\mathbf{Poset}}
\newcommand{\Poset}{\mathbf{Poset}}
\newcommand{\PROJ}{\mathbf{Proj}}
\newcommand{\Psh}{\mathbf{Psh}}
\newcommand{\Ring}{\mathbf{Ring}}
\newcommand{\Rng}{\mathbf{Rng}}
\newcommand{\SET}{\mathbf{SET}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\setmid}{\mathrel{}\middle|\mathrel{}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Shv}{\mathbf{Shv}}
\newcommand{\Three}{\mymathbb{3}}
\renewcommand{\Top}{\mathbf{Top}}
\newcommand{\Two}{\mymathbb{2}}
\newcommand{\Vect}{\mathbf{Vect}}
\newcommand{\Zero}{\mymathbb{0}}
\newcommand{\sA}{\mathscr{A}}
\newcommand{\sB}{\mathscr{B}}
\newcommand{\sC}{\mathscr{C}}
\newcommand{\sD}{\mathscr{D}}
\newcommand{\sE}{\mathscr{E}}
\newcommand{\sF}{\mathscr{F}}
\newcommand{\sG}{\mathscr{G}}
\newcommand{\sH}{\mathscr{H}}
\newcommand{\sI}{\mathscr{I}}
\newcommand{\sJ}{\mathscr{J}}
\newcommand{\sK}{\mathscr{K}}
\newcommand{\sL}{\mathscr{L}}
\newcommand{\sM}{\mathscr{M}}
\newcommand{\sN}{\mathscr{N}}
\newcommand{\sO}{\mathscr{O}}
\newcommand{\sP}{\mathscr{P}}
\newcommand{\sQ}{\mathscr{Q}}
\newcommand{\sR}{\mathscr{R}}
\newcommand{\sS}{\mathscr{S}}
\newcommand{\sT}{\mathscr{T}}
\newcommand{\sU}{\mathscr{U}}
\newcommand{\sV}{\mathscr{V}}
\newcommand{\sW}{\mathscr{W}}
\newcommand{\sX}{\mathscr{X}}
\newcommand{\sY}{\mathscr{Y}}
\newcommand{\sZ}{\mathscr{Z}}
\newcommand{\bfA}{\mathbf{A}}
\newcommand{\bfB}{\mathbf{B}}
\newcommand{\bfC}{\mathbf{C}}
\newcommand{\bfD}{\mathbf{D}}
\newcommand{\bfE}{\mathbf{E}}
\newcommand{\bfF}{\mathbf{F}}
\newcommand{\bfG}{\mathbf{G}}
\newcommand{\bfH}{\mathbf{H}}
\newcommand{\bfI}{\mathbf{I}}
\newcommand{\bfJ}{\mathbf{J}}
\newcommand{\bfK}{\mathbf{K}}
\newcommand{\bfL}{\mathbf{L}}
\newcommand{\bfM}{\mathbf{M}}
\newcommand{\bfN}{\mathbf{N}}
\newcommand{\bfO}{\mathbf{O}}
\newcommand{\bfP}{\mathbf{P}}
\newcommand{\bfQ}{\mathbf{Q}}
\newcommand{\bfR}{\mathbf{R}}
\newcommand{\bfS}{\mathbf{S}}
\newcommand{\bfT}{\mathbf{T}}
\newcommand{\bfU}{\mathbf{U}}
\newcommand{\bfV}{\mathbf{V}}
\newcommand{\bfW}{\mathbf{W}}
\newcommand{\bfX}{\mathbf{X}}
\newcommand{\bfY}{\mathbf{Y}}
\newcommand{\bfZ}{\mathbf{Z}}
\newcommand{\bfa}{\mathbf{a}}
\newcommand{\bfb}{\mathbf{b}}
\newcommand{\bfc}{\mathbf{c}}
\newcommand{\bfd}{\mathbf{d}}
\newcommand{\bfe}{\mathbf{e}}
\newcommand{\bff}{\mathbf{f}}
\newcommand{\bfg}{\mathbf{g}}
\newcommand{\bfh}{\mathbf{h}}
\newcommand{\bfi}{\mathbf{i}}
\newcommand{\bfj}{\mathbf{j}}
\newcommand{\bfk}{\mathbf{k}}
\newcommand{\bfl}{\mathbf{l}}
\newcommand{\bfm}{\mathbf{m}}
\newcommand{\bfn}{\mathbf{n}}
\newcommand{\bfo}{\mathbf{o}}
\newcommand{\bfp}{\mathbf{p}}
\newcommand{\bfq}{\mathbf{q}}
\newcommand{\bfr}{\mathbf{r}}
\newcommand{\bfs}{\mathbf{s}}
\newcommand{\bft}{\mathbf{t}}
\newcommand{\bfu}{\mathbf{u}}
\newcommand{\bfv}{\mathbf{v}}
\newcommand{\bfw}{\mathbf{w}}
\newcommand{\bfx}{\mathbf{x}}
\newcommand{\bfy}{\mathbf{y}}
\newcommand{\bfz}{\mathbf{z}}
\newcommand{\frA}{\mathfrak{A}}
\newcommand{\frB}{\mathfrak{B}}
\newcommand{\frC}{\mathfrak{C}}
\newcommand{\frD}{\mathfrak{D}}
\newcommand{\frE}{\mathfrak{E}}
\newcommand{\frF}{\mathfrak{F}}
\newcommand{\frG}{\mathfrak{G}}
\newcommand{\frH}{\mathfrak{H}}
\newcommand{\frI}{\mathfrak{I}}
\newcommand{\frJ}{\mathfrak{J}}
\newcommand{\frK}{\mathfrak{K}}
\newcommand{\frL}{\mathfrak{L}}
\newcommand{\frM}{\mathfrak{M}}
\newcommand{\frN}{\mathfrak{N}}
\newcommand{\frO}{\mathfrak{O}}
\newcommand{\frP}{\mathfrak{P}}
\newcommand{\frQ}{\mathfrak{Q}}
\newcommand{\frR}{\mathfrak{R}}
\newcommand{\frS}{\mathfrak{S}}
\newcommand{\frT}{\mathfrak{T}}
\newcommand{\frU}{\mathfrak{U}}
\newcommand{\frV}{\mathfrak{V}}
\newcommand{\frW}{\mathfrak{W}}
\newcommand{\frX}{\mathfrak{X}}
\newcommand{\frY}{\mathfrak{Y}}
\newcommand{\frZ}{\mathfrak{Z}}
\newcommand{\Fra}{\mathfrak{a}}
\newcommand{\Frb}{\mathfrak{b}}
\newcommand{\Frc}{\mathfrak{c}}
\newcommand{\Frd}{\mathfrak{d}}
\newcommand{\Fre}{\mathfrak{e}}
\newcommand{\Frf}{\mathfrak{f}}
\newcommand{\Frg}{\mathfrak{g}}
\newcommand{\Frh}{\mathfrak{h}}
\newcommand{\Fri}{\mathfrak{i}}
\newcommand{\Frj}{\mathfrak{j}}
\newcommand{\Frk}{\mathfrak{k}}
\newcommand{\Frl}{\mathfrak{l}}
\newcommand{\Frm}{\mathfrak{m}}
\newcommand{\Frn}{\mathfrak{n}}
\newcommand{\Fro}{\mathfrak{o}}
\newcommand{\Frp}{\mathfrak{p}}
\newcommand{\Frq}{\mathfrak{q}}
\newcommand{\Frr}{\mathfrak{r}}
\newcommand{\Frs}{\mathfrak{s}}
\newcommand{\Frt}{\mathfrak{t}}
\newcommand{\Fru}{\mathfrak{u}}
\newcommand{\Frv}{\mathfrak{v}}
\newcommand{\Frw}{\mathfrak{w}}
\newcommand{\Frx}{\mathfrak{x}}
\newcommand{\Fry}{\mathfrak{y}}
\newcommand{\Frz}{\mathfrak{z}}
\newcommand{\rA}{\mathrm{A}}
\newcommand{\rB}{\mathrm{B}}
\newcommand{\rC}{\mathrm{C}}
\newcommand{\rD}{\mathrm{D}}
\newcommand{\rE}{\mathrm{E}}
\newcommand{\rF}{\mathrm{F}}
\newcommand{\rG}{\mathrm{G}}
\newcommand{\rH}{\mathrm{H}}
\newcommand{\rI}{\mathrm{I}}
\newcommand{\rJ}{\mathrm{J}}
\newcommand{\rK}{\mathrm{K}}
\newcommand{\rL}{\mathrm{L}}
\newcommand{\rM}{\mathrm{M}}
\newcommand{\rN}{\mathrm{N}}
\newcommand{\rO}{\mathrm{O}}
\newcommand{\rP}{\mathrm{P}}
\newcommand{\rQ}{\mathrm{Q}}
\newcommand{\rR}{\mathrm{R}}
\newcommand{\rS}{\mathrm{S}}
\newcommand{\rT}{\mathrm{T}}
\newcommand{\rU}{\mathrm{U}}
\newcommand{\rV}{\mathrm{V}}
\newcommand{\rW}{\mathrm{W}}
\newcommand{\rX}{\mathrm{X}}
\newcommand{\rY}{\mathrm{Y}}
\newcommand{\rZ}{\mathrm{Z}}
\newcommand{\sfA}{\mathsf{A}}
\newcommand{\sfB}{\mathsf{B}}
\newcommand{\sfC}{\mathsf{C}}
\newcommand{\sfD}{\mathsf{D}}
\newcommand{\sfE}{\mathsf{E}}
\newcommand{\sfF}{\mathsf{F}}
\newcommand{\sfG}{\mathsf{G}}
\newcommand{\sfH}{\mathsf{H}}
\newcommand{\sfI}{\mathsf{I}}
\newcommand{\sfJ}{\mathsf{J}}
\newcommand{\sfK}{\mathsf{K}}
\newcommand{\sfL}{\mathsf{L}}
\newcommand{\sfM}{\mathsf{M}}
\newcommand{\sfN}{\mathsf{N}}
\newcommand{\sfO}{\mathsf{O}}
\newcommand{\sfP}{\mathsf{P}}
\newcommand{\sfQ}{\mathsf{Q}}
\newcommand{\sfR}{\mathsf{R}}
\newcommand{\sfS}{\mathsf{S}}
\newcommand{\sfT}{\mathsf{T}}
\newcommand{\sfU}{\mathsf{U}}
\newcommand{\sfV}{\mathsf{V}}
\newcommand{\sfW}{\mathsf{W}}
\newcommand{\sfX}{\mathsf{X}}
\newcommand{\sfY}{\mathsf{Y}}
\newcommand{\sfZ}{\mathsf{Z}}
\newcommand{\bbA}{\mathbbm{A}}
\newcommand{\bbB}{\mathbbm{B}}
\newcommand{\bbC}{\mathbbm{C}}
\newcommand{\bbD}{\mathbbm{D}}
\newcommand{\bbE}{\mathbbm{E}}
\newcommand{\bbF}{\mathbbm{F}}
\newcommand{\bbG}{\mathbbm{G}}
\newcommand{\bbH}{\mathbbm{H}}
\newcommand{\bbI}{\mathbbm{I}}
\newcommand{\bbJ}{\mathbbm{J}}
\newcommand{\bbK}{\mathbbm{K}}
\newcommand{\bbL}{\mathbbm{L}}
\newcommand{\bbM}{\mathbbm{M}}
\newcommand{\bbN}{\mathbbm{N}}
\newcommand{\bbO}{\mathbbm{O}}
\newcommand{\bbP}{\mathbbm{P}}
\newcommand{\bbQ}{\mathbbm{Q}}
\newcommand{\bbR}{\mathbbm{R}}
\newcommand{\bbS}{\mathbbm{S}}
\newcommand{\bbT}{\mathbbm{T}}
\newcommand{\bbU}{\mathbbm{U}}
\newcommand{\bbV}{\mathbbm{V}}
\newcommand{\bbW}{\mathbbm{W}}
\newcommand{\bbX}{\mathbbm{X}}
\newcommand{\bbY}{\mathbbm{Y}}
\newcommand{\bbZ}{\mathbbm{Z}}
\newcommand{\bba}{\mathbbm{a}}
\newcommand{\bbb}{\mathbbm{b}}
\newcommand{\bbc}{\mathbbm{c}}
\newcommand{\bbd}{\mathbbm{d}}
\newcommand{\bbe}{\mathbbm{e}}
\newcommand{\bbf}{\mathbbm{f}}
\newcommand{\bbg}{\mathbbm{g}}
\newcommand{\bbh}{\mathbbm{h}}
\newcommand{\bbi}{\mathbbm{i}}
\newcommand{\bbj}{\mathbbm{j}}
\newcommand{\bbk}{\mathbbm{k}}
\newcommand{\bbl}{\mathbbm{l}}
\newcommand{\bbm}{\mathbbm{m}}
\newcommand{\bbn}{\mathbbm{n}}
\newcommand{\bbo}{\mathbbm{o}}
\newcommand{\bbp}{\mathbbm{p}}
\newcommand{\bbq}{\mathbbm{q}}
\newcommand{\bbr}{\mathbbm{r}}
\newcommand{\bbs}{\mathbbm{s}}
\newcommand{\bbt}{\mathbbm{t}}
\newcommand{\bbu}{\mathbbm{u}}
\newcommand{\bbv}{\mathbbm{v}}
\newcommand{\bbw}{\mathbbm{w}}
\newcommand{\bbx}{\mathbbm{x}}
\newcommand{\bby}{\mathbbm{y}}
\newcommand{\bbz}{\mathbbm{z}}
\newdir{ >}{{ }*!/-5pt/@{>}}
\begin{xy}
\xymatrix@=24pt {
A \ar[r]^{\eta_A} \ar[dr]_{\Un{A}} & TA \ar[d]^a \\
& A
}
\qquad
\xymatrix@=24pt {
T^2A \ar[r]^{\mu_A} \ar[d]_{Ta} & TA \ar[d]^a \\
TA \ar[r]_a & A
}
\end{xy} \tag{1}
\end{equation*} を可換にするものの対 $(A,a)$ を $\rC^T$ における対象とする.
$(A,a)$, $(B,b)$ を $\rC^T$ の 2 つの対象とするとき, $\rC$ の射 $f : A \rightarrow B$ で, 図式
\begin{equation*}
\begin{xy}
\xymatrix@=24pt {
TA \ar[r]^{Tf} \ar[d]_a & TB \ar[d]^b \\
A \ar[r]_f & B
}
\end{xy}
\end{equation*} を可換にするものを圏 $\rC^T$ における射 $f : (A,a) \rightarrow (B,b)$ とする.

例.集合の圏 $\Set$ 上の maybe モナド $(T,\eta,\mu)=((-)_+,\eta,\mu)$ を考える. 簡単のために
\begin{equation*}
TA=A_+=A \amalg \{\bot_A\}
\end{equation*} と記すことにする. ここで $\bot_A$ は $A$ の元以外の元である. 具体的にはたとえば集合 $A$ 自体を考えればよい ($A_+ = A \amalg \{A\}$). このモナドから構成される Eilenberg-Moore 圏 $\Set^T$ において, 対象 $(A,a)$ は, $\rC$ の対象 $A$ と, 図式 (\ref{Eilenberg-Moore-category}) を可換にする $\rC$ の射 $a : A+ \rightarrow A$ により構成される. (\ref{Eilenberg-Moore-category}) の左の三角形の図式は, $a$ が $A \subset A_+$ 上では恒等写像であることを示している.
また, $a$ による $\bot_A \in A_+$ の移り先は $A$ のいずれかの点であり, $(A,a(\bot_A)) \in \Set_+$, より簡潔に $(A,a)$ と記すことができる.
$\Set^T$ における射 $f : (A,a) \rightarrow (B,b)$ は $\Set$ における関数 $f : A \rightarrow B$ で図式
\begin{equation*}
\begin{xy}
\xymatrix@=24pt {
A_+ \ar[r]^{f_+} \ar[d]_a & B_+ \ar[d]^b \\
A \ar[r]_f & B
}
\end{xy}
\end{equation*} を可換にするものである. したがって $f(\bot_A) = \bot_B$ であり, $a(\bot_A$), $b(\bot_B)$, を単に $a,b$ と書けば $f(a) = b$ となる.
つまり, meybe モナド $(T,\eta,\mu)$ 上の Eilenberg-Moore 圏 $\Set^T$ は点付き集合の圏 $\Set_+$ と同一視できる.

Eilenberg-Moore 圏において次の補題が成り立つ.

補題.圏 $\rC$ 上の任意のモナド $(T,\eta,\mu)$ に対して, $\rC$ と Eilenberg-Moore 圏の間の随伴
\begin{equation*}
\begin{xy}
\xymatrix@=32pt {
\rC \ar@<1ex>[r]^{F^T} \ar@{}[r]|{\bot} & \rC^T \ar@<1ex>[l]^{U^T}
}
\end{xy}
\end{equation*} が存在し, この随伴から導かれるモナドは $(T,\eta,\mu)$ である.

証明は省略するが, $U^T : \rC^T \rightarrow \rC$ は忘却関手 (forgetful functor) として定まり, $F^T : \rC \rightarrow \rC^T$ は $\rC$ の対象 $A$ に対してその像を
\begin{equation*}
F^TA := (TA,\mu_A : T^2A \rightarrow TA)
\end{equation*} として, $\rC$ の射 $f : A \rightarrow B$ に対して
\begin{equation*}
F^Tf := (TA,\mu_A) \xrightarrow{Tf} (TB,\mu_B)
\end{equation*} として定まる.
定義より
\begin{equation*}
U^T F^T A = TA,
\end{equation*} すなわち $U^T F^T = T$ である.
この随伴における単位 (unit) $\eta : \Un{\rC} \Rightarrow U^T F^T$ は, モナド $(T,\eta,\mu)$ における $\eta$ そのものであり, 余単位 (counit) $\epsilon : F^T U^T \Rightarrow \Un{\rC^T}$ は $\rC^T$ の各対象 $(A,a)$ に対して
\begin{equation*}
\epsilon_{(A,a)} := a : F^T U^T A = TA \rightarrow A
\end{equation*} である. この $\epsilon$ に対して $U^T \epsilon F^T = \mu : T^2 \Rightarrow T$ が成り立つ.

タグ： Eilenberg-Moore 圏圏論モナド

posted by 底彦 at 20:43 | Comment(0) | TrackBack(0) | 数学

2023年06月06日

数学: 随伴から導かれるモナドの例 ── maybe モナド

モナド ── 定義と随伴により引き起こされるモナドでは, 任意の随伴からモナドが構成されることを見た.
そのようなモナドの例として maybe モナドについて簡単にまとめる.

$\mathbf{Set}_*$ を点付き集合 (pointed set) のなす圏とする.
忘却関手 (forgetful functor) $U : \mathbf{Set}_* \rightarrow \mathbf{Set}$ は左随伴
\begin{equation}
\DeclareMathOperator{\Aff}{Aff}
\DeclareMathOperator{\Ar}{Ar}
\DeclareMathOperator{\Arccos}{Arccos}
\DeclareMathOperator{\Arcsin}{Arcsin}
\DeclareMathOperator{\Arr}{Arr}
\DeclareMathOperator{\arr}{arr}
\DeclareMathOperator{\Aut}{Aut}
\DeclareMathOperator{\Auto}{Auto}
\DeclareMathOperator{\Axiom}{Axiom}
\DeclareMathOperator{\Bilin}{Bilin}
\DeclareMathOperator{\card}{card}
\DeclareMathOperator{\Catelem}{\int}
\DeclareMathOperator{\Cocone}{Cocone}
\DeclareMathOperator{\Cod}{cod}
\DeclareMathOperator{\Codomain}{cod}
\DeclareMathOperator{\Coin}{coin}
\DeclareMathOperator{\coker}{coker}
\DeclareMathOperator{\Colim}{colim}
\DeclareMathOperator{\comp}{comp}
\DeclareMathOperator{\Conf}{Conf}
\DeclareMathOperator{\Conj}{Conj}
\DeclareMathOperator{\Dom}{dom}
\DeclareMathOperator{\Domain}{dom}
\DeclareMathOperator{\Edge}{Edge}
\DeclareMathOperator{\Ev}{ev}
\DeclareMathOperator{\GCD}{gcd}
\DeclareMathOperator{\Gr}{Gr}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Id}{id}
\DeclareMathOperator{\IM}{Im}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\Ind}{ind}
\DeclareMathOperator{\INIT}{init}
\DeclareMathOperator{\iso}{iso}
\DeclareMathOperator{\LCM}{lcm}
\DeclareMathOperator{\Map}{Map}
\DeclareMathOperator{\mor}{arr}
\DeclareMathOperator{\Nat}{Nat}
\DeclareMathOperator{\Ob}{Ob}
\DeclareMathOperator{\ob}{ob}
\DeclareMathOperator{\ord}{ord}
\DeclareMathOperator{\Path}{Path}
\DeclareMathOperator{\PConf}{PConf}
\DeclareMathOperator{\Point}{Point}
\DeclareMathOperator{\Prob}{Prob}
\DeclareMathOperator{\RE}{Re}
\DeclareMathOperator{\Res}{res}
\DeclareMathOperator{\Sect}{Sect}
\DeclareMathOperator{\SF}{SF}
\DeclareMathOperator{\SkelCat}{sk}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Sq}{Sq}
\DeclareMathOperator{\Struct}{Struct}
\DeclareMathOperator{\Sub}{Sub}
\DeclareMathOperator{\Sym}{Sym}
\DeclareMathOperator{\TERM}{term}
\DeclareMathOperator{\Vertex}{Vert}
\newcommand{\Abs}[1]{\lvert{#1}\rvert}
\newcommand{\Bs}{\backslash}
\newcommand{\Cdot}{\,\cdot^{\mathrm{op}}}
\newcommand{\Comma}[2]{{{#1}\!\downarrow\!{#2}}}
\newcommand{\CommaCat}[2]{(#1/#2)}
\newcommand{\Complement}[1]{{\smash[t]{\mathstrut #1}}^{\mathrm{c}}}
\newcommand{\Emph}[1]{\textit{#1}}
\newcommand{\Eqclass}[4]{{#1#2#3}_{#4}}
\newcommand{\EqCls}[2]{{\left[#1\right]}_{#2}}
\newcommand{\Eqcls}[1]{\left[#1\right]}
\newcommand{\Expt}[2]{{\smash[t]{\mathstrut #1}}^{\mathstrut #2}}
\newcommand{\FnRest}[2]{{#1}|{#2}}
\newcommand{\Func}[2]{\mathrm{Func}(#1,#2)}
\newcommand{\g}{\varg}
\newcommand{\Inc}[2]{\mathrm{incl}\left(#1,#2\right)}
\newcommand{\Incl}[2]{\mathrm{incl}_{#1}^{#2}}
\newcommand{\InclArrow}[2]{\morphism(0,0)/>->/<450,0>[\Incl{#1}{#2} : {#1}\,\,`{#2};]}
\newcommand{\Ip}{\amalg}
\newcommand{\Lb}[1]{\mathrm{lb}(#1)}
\newcommand{\LH}{\mathrm{LH}}
\newcommand{\Lowerset}[1]{\downarrow\!\!{#1}}
\newcommand{\Leadsto}{\quad\leadsto\quad}
\newcommand{\Lrsquigarrow}{\quad\leftrightsquigarrow\quad}
\newcommand{\Mb}[1]{\mathbf{#1}}
\newcommand{\Mbb}[1]{\mathbb{#1}}
\newcommand{\Mi}[1]{\mathit{#1}}
\newcommand{\Mlb}[1]{\mathrm{mlb}(#1)}
\newcommand{\Mr}[1]{\mathrm{#1}}
\newcommand{\Ms}[1]{\mathscr{#1}}
\newcommand{\Mt}[1]{\mathtt{#1}}
\newcommand{\Mub}[1]{\mathrm{mub}(#1)}
\newcommand{\newinf}{\mathop{\mathrm{inf}\vphantom{\mathrm{sup}}}}
\newcommand{\newsup}{\mathop{\smash{\mathrm{sup}}}}
\newcommand{\Opp}[1]{#1^{\mathrm{op}}}
\newcommand{\Prj}[2]{\mathrm{proj}\left(#1,#2\right)}
\newcommand{\Proj}[2]{\mathrm{proj}^{#1}_{#2}}
\newcommand{\Pw}{\mathbf{P}}
\newcommand{\Rn}[1]{{\bmdefine{R}}^{#1}}
\newcommand{\q}{\hspace{1em}}
\newcommand{\qq}{\hspace{0.5em}}
\newcommand{\Rel}[1]{\langle{#1}\rangle}
\newcommand{\Rest}[2]{{#1}|{#2}}
\newcommand{\Slash}[1]{{\ooalign{\hfil/\hfil\crcr$#1$}}}
\newcommand{\SliCat}[2]{{#1}\,\big/\,{#2}}
\newcommand{\Src}{d^{0,\mathrm{op}}}
\newcommand{\ssqrt}[1]{\sqrt{\smash[b]{\mathstrut #1}}}
\newcommand{\Tgt}{d^{1,\mathrm{op}}}
\newcommand{\TwArCat}[1]{\mathrm{Tw}(#1)}
\newcommand{\Ub}[1]{\mathrm{ub}(#1)}
\newcommand{\Un}[1]{{1}_{#1}}
\newcommand{\Upperset}[1]{\uparrow\!\!{#1}}
\newcommand{\VectCat}[1]{#1 \mathchar`- \mathbf{Vect}}
\newcommand{\VS}{\vspace*{-1ex}}
\newcommand{\Wbar}[1]{\widebar{#1}}
\newcommand{\Ab}{\mathbf{Ab}}
\newcommand{\Adj}{\mathbf{Adj}}
\newcommand{\Affine}{\mathbf{Affine}}
\newcommand{\Ban}{\mathbf{Ban}}
\newcommand{\bbDelta}{\Delta\mkern-12mu\Delta}
\newcommand{\Card}{\mathbf{Card}}
\newcommand{\CAT}{\mathbf{CAT}}
\newcommand{\Cat}{\mathbf{Cat}}
\newcommand{\cgHaus}{\mathbf{cgHaus}}
\newcommand{\Ch}{\mathbf{Ch}}
\newcommand{\cHaus}{\mathbf{cHaus}}
\newcommand{\Cluster}{\mathbf{Cluster}}
\newcommand{\CMonoid}{\mathbf{CMonoid}}
\newcommand{\CRing}{\mathbf{CRing}}
\newcommand{\DirGraph}{\mathbf{DirGraph}}
\newcommand{\End}{\mathbf{End}}
\newcommand{\Euclid}{\mathbf{Euclid}}
\newcommand{\Field}{\mathbf{Field}}
\newcommand{\Fin}{\mathbf{Fin}}
\newcommand{\FinMetric}{\mathbf{FinMetric}}
\newcommand{\Four}{\mathbbm{4}}
\newcommand{\Graph}{\mathbf{Graph}}
\newcommand{\GrMod}{\mathbf{GrMod}}
\newcommand{\Grp}{\mathbf{Grp}}
\newcommand{\Group}{\mathbf{Group}}
\newcommand{\Groupoid}{\mathbf{Groupoid}}
\newcommand{\Haus}{\mathbf{Haus}}
\newcommand{\Htpy}{\mathbf{Htpy}}
\newcommand{\Man}{\mathbf{Man}}
\newcommand{\Mapsdown}{\rotatebox{270}{$\mapsto$}}
\newcommand{\Mapsup}{\rotatebox{90}{$\mapsto$}}
\newcommand{\Mat}{\mathbf{Mat}}
\newcommand{\Meas}{\mathbf{Meas}}
\newcommand{\Measure}{\mathbf{Measure}}
\newcommand{\Mod}{\mathbf{Mod}}
\newcommand{\Model}{\mathbf{Model}}
\newcommand{\Mon}{\mathbf{Mon}}
\newcommand{\Monoid}{\mathbf{Monoid}}
\newcommand{\oMega}{\bbomega}
\newcommand{\One}{\mymathbb{1}}
\newcommand{\Ord}{\mathrm{Ord}}
\newcommand{\PCluster}{\mathbf{PCluster}}
\newcommand{\POs}{\mathbf{Poset}}
\newcommand{\Poset}{\mathbf{Poset}}
\newcommand{\PROJ}{\mathbf{Proj}}
\newcommand{\Psh}{\mathbf{Psh}}
\newcommand{\Ring}{\mathbf{Ring}}
\newcommand{\Rng}{\mathbf{Rng}}
\newcommand{\SET}{\mathbf{SET}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\setmid}{\mathrel{}\middle|\mathrel{}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Shv}{\mathbf{Shv}}
\newcommand{\Three}{\mymathbb{3}}
\renewcommand{\Top}{\mathbf{Top}}
\newcommand{\Two}{\mymathbb{2}}
\newcommand{\Vect}{\mathbf{Vect}}
\newcommand{\Zero}{\mymathbb{0}}
\newcommand{\sA}{\mathscr{A}}
\newcommand{\sB}{\mathscr{B}}
\newcommand{\sC}{\mathscr{C}}
\newcommand{\sD}{\mathscr{D}}
\newcommand{\sE}{\mathscr{E}}
\newcommand{\sF}{\mathscr{F}}
\newcommand{\sG}{\mathscr{G}}
\newcommand{\sH}{\mathscr{H}}
\newcommand{\sI}{\mathscr{I}}
\newcommand{\sJ}{\mathscr{J}}
\newcommand{\sK}{\mathscr{K}}
\newcommand{\sL}{\mathscr{L}}
\newcommand{\sM}{\mathscr{M}}
\newcommand{\sN}{\mathscr{N}}
\newcommand{\sO}{\mathscr{O}}
\newcommand{\sP}{\mathscr{P}}
\newcommand{\sQ}{\mathscr{Q}}
\newcommand{\sR}{\mathscr{R}}
\newcommand{\sS}{\mathscr{S}}
\newcommand{\sT}{\mathscr{T}}
\newcommand{\sU}{\mathscr{U}}
\newcommand{\sV}{\mathscr{V}}
\newcommand{\sW}{\mathscr{W}}
\newcommand{\sX}{\mathscr{X}}
\newcommand{\sY}{\mathscr{Y}}
\newcommand{\sZ}{\mathscr{Z}}
\newcommand{\bfA}{\mathbf{A}}
\newcommand{\bfB}{\mathbf{B}}
\newcommand{\bfC}{\mathbf{C}}
\newcommand{\bfD}{\mathbf{D}}
\newcommand{\bfE}{\mathbf{E}}
\newcommand{\bfF}{\mathbf{F}}
\newcommand{\bfG}{\mathbf{G}}
\newcommand{\bfH}{\mathbf{H}}
\newcommand{\bfI}{\mathbf{I}}
\newcommand{\bfJ}{\mathbf{J}}
\newcommand{\bfK}{\mathbf{K}}
\newcommand{\bfL}{\mathbf{L}}
\newcommand{\bfM}{\mathbf{M}}
\newcommand{\bfN}{\mathbf{N}}
\newcommand{\bfO}{\mathbf{O}}
\newcommand{\bfP}{\mathbf{P}}
\newcommand{\bfQ}{\mathbf{Q}}
\newcommand{\bfR}{\mathbf{R}}
\newcommand{\bfS}{\mathbf{S}}
\newcommand{\bfT}{\mathbf{T}}
\newcommand{\bfU}{\mathbf{U}}
\newcommand{\bfV}{\mathbf{V}}
\newcommand{\bfW}{\mathbf{W}}
\newcommand{\bfX}{\mathbf{X}}
\newcommand{\bfY}{\mathbf{Y}}
\newcommand{\bfZ}{\mathbf{Z}}
\newcommand{\bfa}{\mathbf{a}}
\newcommand{\bfb}{\mathbf{b}}
\newcommand{\bfc}{\mathbf{c}}
\newcommand{\bfd}{\mathbf{d}}
\newcommand{\bfe}{\mathbf{e}}
\newcommand{\bff}{\mathbf{f}}
\newcommand{\bfg}{\mathbf{g}}
\newcommand{\bfh}{\mathbf{h}}
\newcommand{\bfi}{\mathbf{i}}
\newcommand{\bfj}{\mathbf{j}}
\newcommand{\bfk}{\mathbf{k}}
\newcommand{\bfl}{\mathbf{l}}
\newcommand{\bfm}{\mathbf{m}}
\newcommand{\bfn}{\mathbf{n}}
\newcommand{\bfo}{\mathbf{o}}
\newcommand{\bfp}{\mathbf{p}}
\newcommand{\bfq}{\mathbf{q}}
\newcommand{\bfr}{\mathbf{r}}
\newcommand{\bfs}{\mathbf{s}}
\newcommand{\bft}{\mathbf{t}}
\newcommand{\bfu}{\mathbf{u}}
\newcommand{\bfv}{\mathbf{v}}
\newcommand{\bfw}{\mathbf{w}}
\newcommand{\bfx}{\mathbf{x}}
\newcommand{\bfy}{\mathbf{y}}
\newcommand{\bfz}{\mathbf{z}}
\newcommand{\frA}{\mathfrak{A}}
\newcommand{\frB}{\mathfrak{B}}
\newcommand{\frC}{\mathfrak{C}}
\newcommand{\frD}{\mathfrak{D}}
\newcommand{\frE}{\mathfrak{E}}
\newcommand{\frF}{\mathfrak{F}}
\newcommand{\frG}{\mathfrak{G}}
\newcommand{\frH}{\mathfrak{H}}
\newcommand{\frI}{\mathfrak{I}}
\newcommand{\frJ}{\mathfrak{J}}
\newcommand{\frK}{\mathfrak{K}}
\newcommand{\frL}{\mathfrak{L}}
\newcommand{\frM}{\mathfrak{M}}
\newcommand{\frN}{\mathfrak{N}}
\newcommand{\frO}{\mathfrak{O}}
\newcommand{\frP}{\mathfrak{P}}
\newcommand{\frQ}{\mathfrak{Q}}
\newcommand{\frR}{\mathfrak{R}}
\newcommand{\frS}{\mathfrak{S}}
\newcommand{\frT}{\mathfrak{T}}
\newcommand{\frU}{\mathfrak{U}}
\newcommand{\frV}{\mathfrak{V}}
\newcommand{\frW}{\mathfrak{W}}
\newcommand{\frX}{\mathfrak{X}}
\newcommand{\frY}{\mathfrak{Y}}
\newcommand{\frZ}{\mathfrak{Z}}
\newcommand{\Fra}{\mathfrak{a}}
\newcommand{\Frb}{\mathfrak{b}}
\newcommand{\Frc}{\mathfrak{c}}
\newcommand{\Frd}{\mathfrak{d}}
\newcommand{\Fre}{\mathfrak{e}}
\newcommand{\Frf}{\mathfrak{f}}
\newcommand{\Frg}{\mathfrak{g}}
\newcommand{\Frh}{\mathfrak{h}}
\newcommand{\Fri}{\mathfrak{i}}
\newcommand{\Frj}{\mathfrak{j}}
\newcommand{\Frk}{\mathfrak{k}}
\newcommand{\Frl}{\mathfrak{l}}
\newcommand{\Frm}{\mathfrak{m}}
\newcommand{\Frn}{\mathfrak{n}}
\newcommand{\Fro}{\mathfrak{o}}
\newcommand{\Frp}{\mathfrak{p}}
\newcommand{\Frq}{\mathfrak{q}}
\newcommand{\Frr}{\mathfrak{r}}
\newcommand{\Frs}{\mathfrak{s}}
\newcommand{\Frt}{\mathfrak{t}}
\newcommand{\Fru}{\mathfrak{u}}
\newcommand{\Frv}{\mathfrak{v}}
\newcommand{\Frw}{\mathfrak{w}}
\newcommand{\Frx}{\mathfrak{x}}
\newcommand{\Fry}{\mathfrak{y}}
\newcommand{\Frz}{\mathfrak{z}}
\newcommand{\rA}{\mathrm{A}}
\newcommand{\rB}{\mathrm{B}}
\newcommand{\rC}{\mathrm{C}}
\newcommand{\rD}{\mathrm{D}}
\newcommand{\rE}{\mathrm{E}}
\newcommand{\rF}{\mathrm{F}}
\newcommand{\rG}{\mathrm{G}}
\newcommand{\rH}{\mathrm{H}}
\newcommand{\rI}{\mathrm{I}}
\newcommand{\rJ}{\mathrm{J}}
\newcommand{\rK}{\mathrm{K}}
\newcommand{\rL}{\mathrm{L}}
\newcommand{\rM}{\mathrm{M}}
\newcommand{\rN}{\mathrm{N}}
\newcommand{\rO}{\mathrm{O}}
\newcommand{\rP}{\mathrm{P}}
\newcommand{\rQ}{\mathrm{Q}}
\newcommand{\rR}{\mathrm{R}}
\newcommand{\rS}{\mathrm{S}}
\newcommand{\rT}{\mathrm{T}}
\newcommand{\rU}{\mathrm{U}}
\newcommand{\rV}{\mathrm{V}}
\newcommand{\rW}{\mathrm{W}}
\newcommand{\rX}{\mathrm{X}}
\newcommand{\rY}{\mathrm{Y}}
\newcommand{\rZ}{\mathrm{Z}}
\newcommand{\sfA}{\mathsf{A}}
\newcommand{\sfB}{\mathsf{B}}
\newcommand{\sfC}{\mathsf{C}}
\newcommand{\sfD}{\mathsf{D}}
\newcommand{\sfE}{\mathsf{E}}
\newcommand{\sfF}{\mathsf{F}}
\newcommand{\sfG}{\mathsf{G}}
\newcommand{\sfH}{\mathsf{H}}
\newcommand{\sfI}{\mathsf{I}}
\newcommand{\sfJ}{\mathsf{J}}
\newcommand{\sfK}{\mathsf{K}}
\newcommand{\sfL}{\mathsf{L}}
\newcommand{\sfM}{\mathsf{M}}
\newcommand{\sfN}{\mathsf{N}}
\newcommand{\sfO}{\mathsf{O}}
\newcommand{\sfP}{\mathsf{P}}
\newcommand{\sfQ}{\mathsf{Q}}
\newcommand{\sfR}{\mathsf{R}}
\newcommand{\sfS}{\mathsf{S}}
\newcommand{\sfT}{\mathsf{T}}
\newcommand{\sfU}{\mathsf{U}}
\newcommand{\sfV}{\mathsf{V}}
\newcommand{\sfW}{\mathsf{W}}
\newcommand{\sfX}{\mathsf{X}}
\newcommand{\sfY}{\mathsf{Y}}
\newcommand{\sfZ}{\mathsf{Z}}
\newcommand{\bbA}{\mathbbm{A}}
\newcommand{\bbB}{\mathbbm{B}}
\newcommand{\bbC}{\mathbbm{C}}
\newcommand{\bbD}{\mathbbm{D}}
\newcommand{\bbE}{\mathbbm{E}}
\newcommand{\bbF}{\mathbbm{F}}
\newcommand{\bbG}{\mathbbm{G}}
\newcommand{\bbH}{\mathbbm{H}}
\newcommand{\bbI}{\mathbbm{I}}
\newcommand{\bbJ}{\mathbbm{J}}
\newcommand{\bbK}{\mathbbm{K}}
\newcommand{\bbL}{\mathbbm{L}}
\newcommand{\bbM}{\mathbbm{M}}
\newcommand{\bbN}{\mathbbm{N}}
\newcommand{\bbO}{\mathbbm{O}}
\newcommand{\bbP}{\mathbbm{P}}
\newcommand{\bbQ}{\mathbbm{Q}}
\newcommand{\bbR}{\mathbbm{R}}
\newcommand{\bbS}{\mathbbm{S}}
\newcommand{\bbT}{\mathbbm{T}}
\newcommand{\bbU}{\mathbbm{U}}
\newcommand{\bbV}{\mathbbm{V}}
\newcommand{\bbW}{\mathbbm{W}}
\newcommand{\bbX}{\mathbbm{X}}
\newcommand{\bbY}{\mathbbm{Y}}
\newcommand{\bbZ}{\mathbbm{Z}}
\newcommand{\bba}{\mathbbm{a}}
\newcommand{\bbb}{\mathbbm{b}}
\newcommand{\bbc}{\mathbbm{c}}
\newcommand{\bbd}{\mathbbm{d}}
\newcommand{\bbe}{\mathbbm{e}}
\newcommand{\bbf}{\mathbbm{f}}
\newcommand{\bbg}{\mathbbm{g}}
\newcommand{\bbh}{\mathbbm{h}}
\newcommand{\bbi}{\mathbbm{i}}
\newcommand{\bbj}{\mathbbm{j}}
\newcommand{\bbk}{\mathbbm{k}}
\newcommand{\bbl}{\mathbbm{l}}
\newcommand{\bbm}{\mathbbm{m}}
\newcommand{\bbn}{\mathbbm{n}}
\newcommand{\bbo}{\mathbbm{o}}
\newcommand{\bbp}{\mathbbm{p}}
\newcommand{\bbq}{\mathbbm{q}}
\newcommand{\bbr}{\mathbbm{r}}
\newcommand{\bbs}{\mathbbm{s}}
\newcommand{\bbt}{\mathbbm{t}}
\newcommand{\bbu}{\mathbbm{u}}
\newcommand{\bbv}{\mathbbm{v}}
\newcommand{\bbw}{\mathbbm{w}}
\newcommand{\bbx}{\mathbbm{x}}
\newcommand{\bby}{\mathbbm{y}}
\newcommand{\bbz}{\mathbbm{z}}
\newdir{ >}{{ }*!/-5pt/@{>}}
\begin{xy}
\xymatrix@=16pt {
(-)_+ \,:\, \mathbf{Set} \ar[r] & \mathbf{Set}_* \\
}
\end{xy}
\end{equation} を持つ.
関手 $(-)_+$ は各集合 $A$ に対して点付き集合
\begin{equation*}
A_+ = A \amalg \{ A \} = (A \amalg \{A\}, A)
\end{equation*} を対応させ, 関数 $f : A \rightarrow B$ に対して $f_+ : A_+ \rightarrow B_+$ を
\begin{equation*}
f_+(a) = \begin{cases}
f(a) & (a \in A) \\
B & (a = A)
\end{cases}
\end{equation*} として対応させる.
また, これに伴う単位 (unit) $\eta : \Un{\Set} \Rightarrow U(-)_+$ は, 各集合 $A$ に対して
\begin{equation*}
\begin{xy}
\xymatrix@=16pt@R=0pc {
\eta_A \,:\, A \ar[r] & A_+ \\
\hspace{2em}a \ar@{}[r]|(.6){\mapsto} & a
}
\end{xy}
\end{equation*} により, また余単位 (counit) $\epsilon : (-)_+ U \Rightarrow \Un{\Set_+}$ は, 各点付き集合 $(A,a_0)$ に対して
\begin{equation*}
\begin{xy}
\xymatrix@=16pt@R=0pc {
\epsilon_A \,:\, A_+ \ar[r] & (A,a_0) & \\
\hspace{1.6em}a \ar@{}[r]|(.6){\mapsto} & a & (a \in A) \\
\hspace{1.6em}A \ar@{}[r]|(.6){\mapsto} & a_0 & (a = A)
}
\end{xy}
\end{equation*} により与えられる.
この随伴
\begin{equation*}
\begin{xy}
\xymatrix@=32pt {
\Set_* \ar@<1ex>[r]^{(-)_+} \ar@{}[r]|{\bot} & \Set \ar@<1ex>[l]^{U}
}
\end{xy}
\end{equation*} から導かれるモナドを maybe モナドと呼ぶ.
maybe モナドを実際に構築してみる.
関手 $T : \Set \rightarrow \Set$ は $T=U(-)_+$ によって与えられる. 集合 $A$ に対して
\begin{equation*}
TA = A_+ = A \amalg \{A\}
\end{equation*} であり, 関数 $f : A \rightarrow B$ に対して
\begin{equation*}
Tf = f_+ : A_+ \rightarrow B_+
\end{equation*} である.
単位 (unit) は $\eta : \Un{\Set} \Rightarrow T$ で定まる.
積 (multiplication) は, 各集合 $A$ に対して
\begin{equation*}
(A_+)_+ = (A \amalg \{A\}) \amalg \{A \amalg \{A\}\} = (A \amalg \{A\}) \amalg \{A_+\}
\end{equation*} であるが
\begin{equation*} .
\begin{xy}
\xymatrix@=16pt@R=0pc {
\mu \,:\, (A_+)_+ \ar[r] & A_+ & \\
\hspace{2em}a \ar@{}[r]|(.6){\mapsto} & a & (a \in A) \\
\hspace{2em}A \ar@{}[r]|(.6){\mapsto} & A & (a = A) \\
\hspace{2em}A_+ \ar@{}[r]|(.6){\mapsto} & A & (a = A_+) \\
}
\end{xy}
\end{equation*} により定まる.

$(T,\eta,\mu)$ が実際にモナドになっていることを示す. 図式
\begin{equation*}
\begin{xy}
\xymatrix@=24pt {
T^3A \ar[r]^{T\mu_A} \ar[d]_{\mu_{TA}} & T^2A \ar[d]^{\mu} \\
T^2A \ar[r]_{\mu} & T
}
\qquad
\xymatrix {
TA \ar[r]^{\eta_{TA}} \ar[dr]_{\Un{TA}} & T^2A \ar[d]^{\mu} & TA \ar[l]_{T\eta_A} \ar[dl]^{\Un{TA}} \\
& TA &
}
\end{xy}
\end{equation*} を考える.
$a \in T^3A = ((A_+)_+)_+ = ((A \amalg \{A\}) \amalg \{A_+\}) \amalg \{(A_+)_+\}$ に対して
\begin{equation*}
T\mu_A(a) = \begin{cases}
a & (a \in (A_+)_+) \\
A_+ & (a = (A_+)_+),
\end{cases}
\end{equation*}
\begin{equation*}
\mu_{TA}(a) = \begin{cases}
a & (a \in A_+) \\
A_+ & (a = A_+, (A_+)_+),
\end{cases}
\end{equation*} だから
\begin{equation*}
\mu_A T\mu_A(a) = \begin{cases}
a & (a \in A) \\
A & (a=A, A_+, (A_+)_+)
\end{cases}
\end{equation*}
\begin{equation*}
\mu_A \mu_{TA}(a) = \begin{cases}
a & (a \in A) \\
A & (a=A, A_+, (A_+)_+)
\end{cases}
\end{equation*} となり, 左の図式は可換である.
また, $a \in TA$ に対して
\begin{equation*}
\eta_{TA}(a) = \begin{cases}
a & (a \in TA)
\end{cases}
\end{equation*}
\begin{equation*}
T\eta_A(a) = \begin{cases}
a & (a \in A) \\
A & (a = A)
\end{cases}
\end{equation*} だから
\begin{equation*}
\mu \eta_{TA}(a) = \begin{cases}
a & (a \in A) \\
A & (a = A)
\end{cases}
\end{equation*}
\begin{equation*}
\mu T\eta_A(a) = \begin{cases}
a & (a \in A) \\
A & (a = A)
\end{cases}
\end{equation*} となり, 右側の図式も可換である.
したがって maybe モナド $(T,\eta,\mu)$ は確かにモナドである.

プログラミングとの関係で言えば, 任意の関数 $f : A \rightarrow B$ を実装したプログラム $f_+ : A_+ \rightarrow B_+$ は, 入力 $a \in A$ に対しては出力として正常値 $f(a) \in B$ を返し, 予期せぬ入力 $a=A$ に対してはエラー値 $f_+(A) = B$ を返すということになる.

タグ：モナド maybe モナド

posted by 底彦 at 23:30 | Comment(0) | TrackBack(0) | 数学

2023年03月26日

数学: モナド ── 定義と随伴により引き起こされるモナド

モナドの概念をまとめておく.
定義等は Emily Riehl の教科書 "Category Theory in Context" に従う.

定義.圏 $\mathrm{C}$ における モナド (monad)は 3 つ組 $(T,\eta,\mu)$:
・関手 $T : \mathrm{C} \rightarrow \mathrm{C}$;
・ 単位 (unit)と呼ばれる自然変換 $\eta : 1_{\mathrm{C}} \Rightarrow T$;
・ 積 (multiplication)と呼ばれる自然変換 $\mu : T^2 \Rightarrow T$
で, 以下の図式を可換にするものである.
\begin{equation*}
\DeclareMathOperator{\Aff}{Aff}
\DeclareMathOperator{\Ar}{Ar}
\DeclareMathOperator{\Arccos}{Arccos}
\DeclareMathOperator{\Arcsin}{Arcsin}
\DeclareMathOperator{\Arr}{Arr}
\DeclareMathOperator{\arr}{arr}
\DeclareMathOperator{\Aut}{Aut}
\DeclareMathOperator{\Auto}{Auto}
\DeclareMathOperator{\Axiom}{Axiom}
\DeclareMathOperator{\Bilin}{Bilin}
\DeclareMathOperator{\card}{card}
\DeclareMathOperator{\Catelem}{\int}
\DeclareMathOperator{\Cocone}{Cocone}
\DeclareMathOperator{\Cod}{cod}
\DeclareMathOperator{\Codomain}{cod}
\DeclareMathOperator{\Coin}{coin}
\DeclareMathOperator{\coker}{coker}
\DeclareMathOperator{\Colim}{colim}
\DeclareMathOperator{\comp}{comp}
\DeclareMathOperator{\Conf}{Conf}
\DeclareMathOperator{\Conj}{Conj}
\DeclareMathOperator{\Dom}{dom}
\DeclareMathOperator{\Domain}{dom}
\DeclareMathOperator{\Edge}{Edge}
\DeclareMathOperator{\Ev}{ev}
\DeclareMathOperator{\GCD}{gcd}
\DeclareMathOperator{\Gr}{Gr}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Id}{id}
\DeclareMathOperator{\IM}{Im}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\Ind}{ind}
\DeclareMathOperator{\INIT}{init}
\DeclareMathOperator{\iso}{iso}
\DeclareMathOperator{\LCM}{lcm}
\DeclareMathOperator{\Map}{Map}
\DeclareMathOperator{\mor}{arr}
\DeclareMathOperator{\Nat}{Nat}
\DeclareMathOperator{\Ob}{Ob}
\DeclareMathOperator{\ob}{ob}
\DeclareMathOperator{\ord}{ord}
\DeclareMathOperator{\Path}{Path}
\DeclareMathOperator{\PConf}{PConf}
\DeclareMathOperator{\Point}{Point}
\DeclareMathOperator{\Prob}{Prob}
\DeclareMathOperator{\RE}{Re}
\DeclareMathOperator{\Res}{res}
\DeclareMathOperator{\Sect}{Sect}
\DeclareMathOperator{\SF}{SF}
\DeclareMathOperator{\SkelCat}{sk}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Sq}{Sq}
\DeclareMathOperator{\Struct}{Struct}
\DeclareMathOperator{\Sub}{Sub}
\DeclareMathOperator{\Sym}{Sym}
\DeclareMathOperator{\TERM}{term}
\DeclareMathOperator{\Vertex}{Vert}
\newcommand{\Abs}[1]{\lvert{#1}\rvert}
\newcommand{\Bs}{\backslash}
\newcommand{\Cdot}{\,\cdot^{\mathrm{op}}}
\newcommand{\Comma}[2]{{{#1}\!\downarrow\!{#2}}}
\newcommand{\CommaCat}[2]{(#1/#2)}
\newcommand{\Complement}[1]{{\smash[t]{\mathstrut #1}}^{\mathrm{c}}}
\newcommand{\Emph}[1]{\textit{#1}}
\newcommand{\Eqclass}[4]{{#1#2#3}_{#4}}
\newcommand{\EqCls}[2]{{\left[#1\right]}_{#2}}
\newcommand{\Eqcls}[1]{\left[#1\right]}
\newcommand{\Expt}[2]{{\smash[t]{\mathstrut #1}}^{\mathstrut #2}}
\newcommand{\FnRest}[2]{{#1}|{#2}}
\newcommand{\Func}[2]{\mathrm{Func}(#1,#2)}
\newcommand{\g}{\varg}
\newcommand{\Inc}[2]{\mathrm{incl}\left(#1,#2\right)}
\newcommand{\Incl}[2]{\mathrm{incl}_{#1}^{#2}}
\newcommand{\InclArrow}[2]{\morphism(0,0)/>->/<450,0>[\Incl{#1}{#2} : {#1}\,\,`{#2};]}
\newcommand{\Ip}{\amalg}
\newcommand{\Lb}[1]{\mathrm{lb}(#1)}
\newcommand{\LH}{\mathrm{LH}}
\newcommand{\Lowerset}[1]{\downarrow\!\!{#1}}
\newcommand{\Leadsto}{\quad\leadsto\quad}
\newcommand{\Lrsquigarrow}{\quad\leftrightsquigarrow\quad}
\newcommand{\Mb}[1]{\mathbf{#1}}
\newcommand{\Mbb}[1]{\mathbb{#1}}
\newcommand{\Mi}[1]{\mathit{#1}}
\newcommand{\Mlb}[1]{\mathrm{mlb}(#1)}
\newcommand{\Mr}[1]{\mathrm{#1}}
\newcommand{\Ms}[1]{\mathscr{#1}}
\newcommand{\Mt}[1]{\mathtt{#1}}
\newcommand{\Mub}[1]{\mathrm{mub}(#1)}
\newcommand{\newinf}{\mathop{\mathrm{inf}\vphantom{\mathrm{sup}}}}
\newcommand{\newsup}{\mathop{\smash{\mathrm{sup}}}}
\newcommand{\Opp}[1]{#1^{\mathrm{op}}}
\newcommand{\Prj}[2]{\mathrm{proj}\left(#1,#2\right)}
\newcommand{\Proj}[2]{\mathrm{proj}^{#1}_{#2}}
\newcommand{\Pw}{\mathbf{P}}
\newcommand{\Rn}[1]{{\bmdefine{R}}^{#1}}
\newcommand{\q}{\hspace{1em}}
\newcommand{\qq}{\hspace{0.5em}}
\newcommand{\Rel}[1]{\langle{#1}\rangle}
\newcommand{\Rest}[2]{{#1}|{#2}}
\newcommand{\Slash}[1]{{\ooalign{\hfil/\hfil\crcr$#1$}}}
\newcommand{\SliCat}[2]{{#1}\,\big/\,{#2}}
\newcommand{\Src}{d^{0,\mathrm{op}}}
\newcommand{\ssqrt}[1]{\sqrt{\smash[b]{\mathstrut #1}}}
\newcommand{\Tgt}{d^{1,\mathrm{op}}}
\newcommand{\TwArCat}[1]{\mathrm{Tw}(#1)}
\newcommand{\Ub}[1]{\mathrm{ub}(#1)}
\newcommand{\Un}[1]{{1}_{#1}}
\newcommand{\Upperset}[1]{\uparrow\!\!{#1}}
\newcommand{\VectCat}[1]{#1 \mathchar`- \mathbf{Vect}}
\newcommand{\VS}{\vspace*{-1ex}}
\newcommand{\Wbar}[1]{\widebar{#1}}
\newcommand{\Ab}{\mathbf{Ab}}
\newcommand{\Adj}{\mathbf{Adj}}
\newcommand{\Affine}{\mathbf{Affine}}
\newcommand{\Ban}{\mathbf{Ban}}
\newcommand{\bbDelta}{\Delta\mkern-12mu\Delta}
\newcommand{\Card}{\mathbf{Card}}
\newcommand{\CAT}{\mathbf{CAT}}
\newcommand{\Cat}{\mathbf{Cat}}
\newcommand{\cgHaus}{\mathbf{cgHaus}}
\newcommand{\Ch}{\mathbf{Ch}}
\newcommand{\cHaus}{\mathbf{cHaus}}
\newcommand{\Cluster}{\mathbf{Cluster}}
\newcommand{\CMonoid}{\mathbf{CMonoid}}
\newcommand{\CRing}{\mathbf{CRing}}
\newcommand{\DirGraph}{\mathbf{DirGraph}}
\newcommand{\End}{\mathbf{End}}
\newcommand{\Euclid}{\mathbf{Euclid}}
\newcommand{\Field}{\mathbf{Field}}
\newcommand{\Fin}{\mathbf{Fin}}
\newcommand{\FinMetric}{\mathbf{FinMetric}}
\newcommand{\Four}{\mathbbm{4}}
\newcommand{\Graph}{\mathbf{Graph}}
\newcommand{\GrMod}{\mathbf{GrMod}}
\newcommand{\Grp}{\mathbf{Grp}}
\newcommand{\Group}{\mathbf{Group}}
\newcommand{\Groupoid}{\mathbf{Groupoid}}
\newcommand{\Haus}{\mathbf{Haus}}
\newcommand{\Htpy}{\mathbf{Htpy}}
\newcommand{\Man}{\mathbf{Man}}
\newcommand{\Mapsdown}{\rotatebox{270}{$\mapsto$}}
\newcommand{\Mapsup}{\rotatebox{90}{$\mapsto$}}
\newcommand{\Mat}{\mathbf{Mat}}
\newcommand{\Meas}{\mathbf{Meas}}
\newcommand{\Measure}{\mathbf{Measure}}
\newcommand{\Mod}{\mathbf{Mod}}
\newcommand{\Model}{\mathbf{Model}}
\newcommand{\Mon}{\mathbf{Mon}}
\newcommand{\Monoid}{\mathbf{Monoid}}
\newcommand{\oMega}{\bbomega}
\newcommand{\One}{\mymathbb{1}}
\newcommand{\Ord}{\mathrm{Ord}}
\newcommand{\PCluster}{\mathbf{PCluster}}
\newcommand{\POs}{\mathbf{Poset}}
\newcommand{\Poset}{\mathbf{Poset}}
\newcommand{\PROJ}{\mathbf{Proj}}
\newcommand{\Psh}{\mathbf{Psh}}
\newcommand{\Ring}{\mathbf{Ring}}
\newcommand{\Rng}{\mathbf{Rng}}
\newcommand{\SET}{\mathbf{SET}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\setmid}{\mathrel{}\middle|\mathrel{}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Shv}{\mathbf{Shv}}
\newcommand{\Three}{\mymathbb{3}}
\renewcommand{\Top}{\mathbf{Top}}
\newcommand{\Two}{\mymathbb{2}}
\newcommand{\Vect}{\mathbf{Vect}}
\newcommand{\Zero}{\mymathbb{0}}
\newcommand{\sA}{\mathscr{A}}
\newcommand{\sB}{\mathscr{B}}
\newcommand{\sC}{\mathscr{C}}
\newcommand{\sD}{\mathscr{D}}
\newcommand{\sE}{\mathscr{E}}
\newcommand{\sF}{\mathscr{F}}
\newcommand{\sG}{\mathscr{G}}
\newcommand{\sH}{\mathscr{H}}
\newcommand{\sI}{\mathscr{I}}
\newcommand{\sJ}{\mathscr{J}}
\newcommand{\sK}{\mathscr{K}}
\newcommand{\sL}{\mathscr{L}}
\newcommand{\sM}{\mathscr{M}}
\newcommand{\sN}{\mathscr{N}}
\newcommand{\sO}{\mathscr{O}}
\newcommand{\sP}{\mathscr{P}}
\newcommand{\sQ}{\mathscr{Q}}
\newcommand{\sR}{\mathscr{R}}
\newcommand{\sS}{\mathscr{S}}
\newcommand{\sT}{\mathscr{T}}
\newcommand{\sU}{\mathscr{U}}
\newcommand{\sV}{\mathscr{V}}
\newcommand{\sW}{\mathscr{W}}
\newcommand{\sX}{\mathscr{X}}
\newcommand{\sY}{\mathscr{Y}}
\newcommand{\sZ}{\mathscr{Z}}
\newcommand{\bfA}{\mathbf{A}}
\newcommand{\bfB}{\mathbf{B}}
\newcommand{\bfC}{\mathbf{C}}
\newcommand{\bfD}{\mathbf{D}}
\newcommand{\bfE}{\mathbf{E}}
\newcommand{\bfF}{\mathbf{F}}
\newcommand{\bfG}{\mathbf{G}}
\newcommand{\bfH}{\mathbf{H}}
\newcommand{\bfI}{\mathbf{I}}
\newcommand{\bfJ}{\mathbf{J}}
\newcommand{\bfK}{\mathbf{K}}
\newcommand{\bfL}{\mathbf{L}}
\newcommand{\bfM}{\mathbf{M}}
\newcommand{\bfN}{\mathbf{N}}
\newcommand{\bfO}{\mathbf{O}}
\newcommand{\bfP}{\mathbf{P}}
\newcommand{\bfQ}{\mathbf{Q}}
\newcommand{\bfR}{\mathbf{R}}
\newcommand{\bfS}{\mathbf{S}}
\newcommand{\bfT}{\mathbf{T}}
\newcommand{\bfU}{\mathbf{U}}
\newcommand{\bfV}{\mathbf{V}}
\newcommand{\bfW}{\mathbf{W}}
\newcommand{\bfX}{\mathbf{X}}
\newcommand{\bfY}{\mathbf{Y}}
\newcommand{\bfZ}{\mathbf{Z}}
\newcommand{\bfa}{\mathbf{a}}
\newcommand{\bfb}{\mathbf{b}}
\newcommand{\bfc}{\mathbf{c}}
\newcommand{\bfd}{\mathbf{d}}
\newcommand{\bfe}{\mathbf{e}}
\newcommand{\bff}{\mathbf{f}}
\newcommand{\bfg}{\mathbf{g}}
\newcommand{\bfh}{\mathbf{h}}
\newcommand{\bfi}{\mathbf{i}}
\newcommand{\bfj}{\mathbf{j}}
\newcommand{\bfk}{\mathbf{k}}
\newcommand{\bfl}{\mathbf{l}}
\newcommand{\bfm}{\mathbf{m}}
\newcommand{\bfn}{\mathbf{n}}
\newcommand{\bfo}{\mathbf{o}}
\newcommand{\bfp}{\mathbf{p}}
\newcommand{\bfq}{\mathbf{q}}
\newcommand{\bfr}{\mathbf{r}}
\newcommand{\bfs}{\mathbf{s}}
\newcommand{\bft}{\mathbf{t}}
\newcommand{\bfu}{\mathbf{u}}
\newcommand{\bfv}{\mathbf{v}}
\newcommand{\bfw}{\mathbf{w}}
\newcommand{\bfx}{\mathbf{x}}
\newcommand{\bfy}{\mathbf{y}}
\newcommand{\bfz}{\mathbf{z}}
\newcommand{\frA}{\mathfrak{A}}
\newcommand{\frB}{\mathfrak{B}}
\newcommand{\frC}{\mathfrak{C}}
\newcommand{\frD}{\mathfrak{D}}
\newcommand{\frE}{\mathfrak{E}}
\newcommand{\frF}{\mathfrak{F}}
\newcommand{\frG}{\mathfrak{G}}
\newcommand{\frH}{\mathfrak{H}}
\newcommand{\frI}{\mathfrak{I}}
\newcommand{\frJ}{\mathfrak{J}}
\newcommand{\frK}{\mathfrak{K}}
\newcommand{\frL}{\mathfrak{L}}
\newcommand{\frM}{\mathfrak{M}}
\newcommand{\frN}{\mathfrak{N}}
\newcommand{\frO}{\mathfrak{O}}
\newcommand{\frP}{\mathfrak{P}}
\newcommand{\frQ}{\mathfrak{Q}}
\newcommand{\frR}{\mathfrak{R}}
\newcommand{\frS}{\mathfrak{S}}
\newcommand{\frT}{\mathfrak{T}}
\newcommand{\frU}{\mathfrak{U}}
\newcommand{\frV}{\mathfrak{V}}
\newcommand{\frW}{\mathfrak{W}}
\newcommand{\frX}{\mathfrak{X}}
\newcommand{\frY}{\mathfrak{Y}}
\newcommand{\frZ}{\mathfrak{Z}}
\newcommand{\Fra}{\mathfrak{a}}
\newcommand{\Frb}{\mathfrak{b}}
\newcommand{\Frc}{\mathfrak{c}}
\newcommand{\Frd}{\mathfrak{d}}
\newcommand{\Fre}{\mathfrak{e}}
\newcommand{\Frf}{\mathfrak{f}}
\newcommand{\Frg}{\mathfrak{g}}
\newcommand{\Frh}{\mathfrak{h}}
\newcommand{\Fri}{\mathfrak{i}}
\newcommand{\Frj}{\mathfrak{j}}
\newcommand{\Frk}{\mathfrak{k}}
\newcommand{\Frl}{\mathfrak{l}}
\newcommand{\Frm}{\mathfrak{m}}
\newcommand{\Frn}{\mathfrak{n}}
\newcommand{\Fro}{\mathfrak{o}}
\newcommand{\Frp}{\mathfrak{p}}
\newcommand{\Frq}{\mathfrak{q}}
\newcommand{\Frr}{\mathfrak{r}}
\newcommand{\Frs}{\mathfrak{s}}
\newcommand{\Frt}{\mathfrak{t}}
\newcommand{\Fru}{\mathfrak{u}}
\newcommand{\Frv}{\mathfrak{v}}
\newcommand{\Frw}{\mathfrak{w}}
\newcommand{\Frx}{\mathfrak{x}}
\newcommand{\Fry}{\mathfrak{y}}
\newcommand{\Frz}{\mathfrak{z}}
\newcommand{\rA}{\mathrm{A}}
\newcommand{\rB}{\mathrm{B}}
\newcommand{\rC}{\mathrm{C}}
\newcommand{\rD}{\mathrm{D}}
\newcommand{\rE}{\mathrm{E}}
\newcommand{\rF}{\mathrm{F}}
\newcommand{\rG}{\mathrm{G}}
\newcommand{\rH}{\mathrm{H}}
\newcommand{\rI}{\mathrm{I}}
\newcommand{\rJ}{\mathrm{J}}
\newcommand{\rK}{\mathrm{K}}
\newcommand{\rL}{\mathrm{L}}
\newcommand{\rM}{\mathrm{M}}
\newcommand{\rN}{\mathrm{N}}
\newcommand{\rO}{\mathrm{O}}
\newcommand{\rP}{\mathrm{P}}
\newcommand{\rQ}{\mathrm{Q}}
\newcommand{\rR}{\mathrm{R}}
\newcommand{\rS}{\mathrm{S}}
\newcommand{\rT}{\mathrm{T}}
\newcommand{\rU}{\mathrm{U}}
\newcommand{\rV}{\mathrm{V}}
\newcommand{\rW}{\mathrm{W}}
\newcommand{\rX}{\mathrm{X}}
\newcommand{\rY}{\mathrm{Y}}
\newcommand{\rZ}{\mathrm{Z}}
\newcommand{\sfA}{\mathsf{A}}
\newcommand{\sfB}{\mathsf{B}}
\newcommand{\sfC}{\mathsf{C}}
\newcommand{\sfD}{\mathsf{D}}
\newcommand{\sfE}{\mathsf{E}}
\newcommand{\sfF}{\mathsf{F}}
\newcommand{\sfG}{\mathsf{G}}
\newcommand{\sfH}{\mathsf{H}}
\newcommand{\sfI}{\mathsf{I}}
\newcommand{\sfJ}{\mathsf{J}}
\newcommand{\sfK}{\mathsf{K}}
\newcommand{\sfL}{\mathsf{L}}
\newcommand{\sfM}{\mathsf{M}}
\newcommand{\sfN}{\mathsf{N}}
\newcommand{\sfO}{\mathsf{O}}
\newcommand{\sfP}{\mathsf{P}}
\newcommand{\sfQ}{\mathsf{Q}}
\newcommand{\sfR}{\mathsf{R}}
\newcommand{\sfS}{\mathsf{S}}
\newcommand{\sfT}{\mathsf{T}}
\newcommand{\sfU}{\mathsf{U}}
\newcommand{\sfV}{\mathsf{V}}
\newcommand{\sfW}{\mathsf{W}}
\newcommand{\sfX}{\mathsf{X}}
\newcommand{\sfY}{\mathsf{Y}}
\newcommand{\sfZ}{\mathsf{Z}}
\newcommand{\bbA}{\mathbbm{A}}
\newcommand{\bbB}{\mathbbm{B}}
\newcommand{\bbC}{\mathbbm{C}}
\newcommand{\bbD}{\mathbbm{D}}
\newcommand{\bbE}{\mathbbm{E}}
\newcommand{\bbF}{\mathbbm{F}}
\newcommand{\bbG}{\mathbbm{G}}
\newcommand{\bbH}{\mathbbm{H}}
\newcommand{\bbI}{\mathbbm{I}}
\newcommand{\bbJ}{\mathbbm{J}}
\newcommand{\bbK}{\mathbbm{K}}
\newcommand{\bbL}{\mathbbm{L}}
\newcommand{\bbM}{\mathbbm{M}}
\newcommand{\bbN}{\mathbbm{N}}
\newcommand{\bbO}{\mathbbm{O}}
\newcommand{\bbP}{\mathbbm{P}}
\newcommand{\bbQ}{\mathbbm{Q}}
\newcommand{\bbR}{\mathbbm{R}}
\newcommand{\bbS}{\mathbbm{S}}
\newcommand{\bbT}{\mathbbm{T}}
\newcommand{\bbU}{\mathbbm{U}}
\newcommand{\bbV}{\mathbbm{V}}
\newcommand{\bbW}{\mathbbm{W}}
\newcommand{\bbX}{\mathbbm{X}}
\newcommand{\bbY}{\mathbbm{Y}}
\newcommand{\bbZ}{\mathbbm{Z}}
\newcommand{\bba}{\mathbbm{a}}
\newcommand{\bbb}{\mathbbm{b}}
\newcommand{\bbc}{\mathbbm{c}}
\newcommand{\bbd}{\mathbbm{d}}
\newcommand{\bbe}{\mathbbm{e}}
\newcommand{\bbf}{\mathbbm{f}}
\newcommand{\bbg}{\mathbbm{g}}
\newcommand{\bbh}{\mathbbm{h}}
\newcommand{\bbi}{\mathbbm{i}}
\newcommand{\bbj}{\mathbbm{j}}
\newcommand{\bbk}{\mathbbm{k}}
\newcommand{\bbl}{\mathbbm{l}}
\newcommand{\bbm}{\mathbbm{m}}
\newcommand{\bbn}{\mathbbm{n}}
\newcommand{\bbo}{\mathbbm{o}}
\newcommand{\bbp}{\mathbbm{p}}
\newcommand{\bbq}{\mathbbm{q}}
\newcommand{\bbr}{\mathbbm{r}}
\newcommand{\bbs}{\mathbbm{s}}
\newcommand{\bbt}{\mathbbm{t}}
\newcommand{\bbu}{\mathbbm{u}}
\newcommand{\bbv}{\mathbbm{v}}
\newcommand{\bbw}{\mathbbm{w}}
\newcommand{\bbx}{\mathbbm{x}}
\newcommand{\bby}{\mathbbm{y}}
\newcommand{\bbz}{\mathbbm{z}}
\begin{xy}
\xymatrix@=24pt {
T^3 \ar@{=>}[d]_{\mu T} \ar@{=>}[r]^{T \mu} & T^2 \ar@{=>}[d]^{\mu} \\
T^2 \ar@{=>}[r]_{\mu} & T
}
\qquad
\xymatrix@=24pt {
T \ar@{=>}[r]^{\eta T} \ar@{=>}[dr]_{\Un{T}}
& T^2 \ar@{=>}[d]^{\mu}
& T \ar@{=>}[l]_{T \eta} \ar@{=>}[dl]^{\Un{T}} \\
& T &
}
\end{xy}
\end{equation*}
補題.任意の随伴
\begin{equation*}
\begin{xy}
\xymatrix@=24pt {
\rC \ar@<1ex>[r]^F \ar@{}[r]|{\bot} & \rD \ar@<1ex>[l]^U
}
\end{xy}
\qquad
\eta : \Un{\rC} \Rightarrow UF,
\quad
\epsilon : FU \Rightarrow \Un{\rD}
\end{equation*} は以下の構成により左随伴の定義域の圏 $\rC$ 上のモナドを引き起こす:
・関手 $T : \rC \rightarrow \rC$ は $UF$ により与えられる.
・単位 $\eta : \Un{\rC} \Rightarrow UF$ がモナドの単位 $\eta : \Un{\rC} \Rightarrow T$ となる.
・ $U \epsilon F : UFUF \Rightarrow UF$ がモナドの積 $\mu : T^2 \Rightarrow T$ となる.

証明 (概略).
まず, 図式
\begin{equation}
\label{dgm:1}
\begin{xy}
\xymatrix@=24pt {
UF \ar@{=>}[r]^{\eta UF} \ar@{=>}[dr]_{\Un{UF}} & UFUF \ar@{=>}[d]^{U \epsilon F} & UF \ar@{=>}[l]_{UF\eta} \ar@{=>}[dl]^{\Un{UF}} \\
& UF &
}
\end{xy} \tag{1}
\end{equation}
を考える.
随伴の単位 (unit) $\eta : \Un{\rC} \Rightarrow UF$, 余単位 (counit) $\epsilon : FU \Rightarrow \Un{\rD}$ は三角恒等式 (triangle identities)
\begin{equation*}
\begin{xy}
\xymatrix@=24pt {
F \ar@{=>}[r]^{F\eta} \ar@{=>}[dr]_{\Un{F}} & FUF \ar@{=>}[d]^{\epsilon F} \\
& F
}
\end{xy}
\qquad
\begin{xy}
\xymatrix@=24pt {
U \ar@{=>}[r]^{\eta U} \ar@{=>}[dr]_{\Un{U}} & UFU \ar@{=>}[d]^{U\epsilon} \\
& U
}
\end{xy}
\end{equation*} を可換にする.
左の三角形に $U$ を適用すると (\ref{dgm:1}) の右側の三角形が得られる.
右の三角形を $F$ に適用すると (\ref{dgm:1}) の左側の三角形が得られる.
よって, 図式 (\ref{dgm:1}) は可換である.

次に図式
\begin{equation}
\label{dgm:2}
\begin{xy}
\xymatrix@=24pt {
UFUFUF \ar@{=>}[d]_{U \epsilon FUF} \ar@{=>}[rr]^{UFU \epsilon F} && UFUF \ar@{=>}[d]^{U \epsilon F} \\
UFUF \ar@{=>}[rr]_{U \epsilon F} && UF
}
\end{xy} \tag{2}
\end{equation} を考える.
任意の対象 $c\in\rC$ にこの図式を適用すると,
\begin{equation*}
\begin{xy}
\xymatrix@=24pt {
UFU(FUFc) \ar[d]_{U\epsilon_{FUFc}} \ar[rr]^{UFU(\epsilon_{Fc})} && UFU(Fc) \ar[d]^{U\epsilon_{Fc}} \\
U(FUFc) \ar[rr]_{U(\epsilon_{Fc})} && U(Fc)
}
\end{xy}
\end{equation*} となり, これは自然変換 $U\epsilon : UFU \Rightarrow U$ の $c$ における可換性を示す図式に他ならない.
よって, 図式 (\ref{dgm:2}) も可換となり, $(UF,\eta,U\epsilon F)$ はモナドとなる.

これにより, 関手の随伴が与えられれば, それに伴うモナドが構成されることになる.

タグ：随伴により引き起こされるモナドモナド圏論

posted by 底彦 at 09:24 | Comment(0) | TrackBack(0) | 数学

2022年12月11日

数学: 環の定義

環論の復習をしている.教科書は van der Waerden の "Algebra" で, そこにおける環の定義は次のようなものである.

定義.集合 $R$ において, 以下が成り立つとき, $R$ は環 (ring) であるという.
I. 加法律
和と呼ばれる演算 $+$ が定義されていて以下を満たす.
a) 加法の結合法則: 任意の $a,b,c \in R$ に対して
\begin{equation*}
(a+b)+c = a+(b+c)
\end{equation*}
が成り立つ.
b) 加法の可換性: 任意の $a,b \in R$ に対して
\begin{equation*}
a+b=b+a
\end{equation*}
が成り立つ.
c) 加法の左単位元の存在: $R$ のある元 $0$ で, 任意の $R$ の元 $a$ に対して
\begin{equation*}
0 + a = a
\end{equation*}
を満たすものが存在する. $0$ を加法に関する左単位元と呼ぶ.
d) 加法の左逆元の存在: 任意の $R$ の元 $a$ に対して, ある $R$ の元 $b$ が存在して
\begin{equation*}
b+a = 0
\end{equation*}
が成り立つ. $b$ を $-a$ と記す.
II. 乗法律.
積と呼ばれる演算 $\cdot$ が定義されていて以下を満たす. なお, 積 $a \cdot b$ を単に $ab$ とも記す.
a) 乗法の結合法則: 任意の $a,b,c \in R$ に対して
\begin{equation*}
a \cdot bc = ab \cdot c
\end{equation*}
が成り立つ.
III. 分配法則.
任意の $a,b,c \in R$ に対して
\begin{align*}
a \cdot (b+c) & = ab+ac, \\
(b+c) \cdot a & = ba+ca
\end{align*}
が成り立つ.

さらに, 条件
II. b) 乗法の可換性: 任意の $a,b \in R$ に対して
\begin{equation*}
ab = ba.
\end{equation*}
が成り立つとき, $R$ を可換環 (commutative ring) と呼ぶ.

なお, この定義では, 加法に関する右単位元や右逆元の存在などは仮定されていない.
これらの存在は加法の可換性 I. b) を使用すればすぐに導かれる.
以下ではあえて加法の可換性を使わずに存在および一意性を導いてみる.
なお, 以下において加法の結合法則は暗黙のうちに使用する.

$R$ を環とし, $a \in R$ とする.
I. d) によって $a$ の左逆元 $-a$ が存在して
\begin{equation*}
(-a)+a = 0
\end{equation*}
が成り立つ. 両辺に右側から $-a$ を加えると I. c) により,
\begin{equation*}
(-a)+a+(-a) = 0+(-a) = -a.
\end{equation*}
$-a$ の加法に関する左逆元 $-(-a)$ を両辺に左側から加えることにより,
\begin{align*}
-(-a)+(-a)+a+(-a) & = -(-a)+(-a) = 0, \\
0+a+(-a) & = 0, \\
a+(-a) & = 0.
\end{align*}
よって $a$ の左逆元 $-a$ は同時に $a$ の右逆元でもある.
$-a$ を単に $a$ の加法に関する逆元と呼ぶ.

次に $0$ を $R$ における任意の左単位元とする. 任意の $a \in R$ に対して
\begin{equation*}
(-a)+a=0
\end{equation*}
が成り立つが, この式の両辺に $0$ を右側から加えると, I. c) により
\begin{equation*}
(-a)+a+0 = 0+0 = 0
\end{equation*}
が成り立つ. この式の両辺に $-(-a)$ を左側から加えると,
\begin{align*}
-(-a)+(-a)+a+0 & = 0, \\
0+a+0 & = 0, \\
a+0 & = 0
\end{align*}
となる. よって $0$ は $R$ の加法に関する右単位元でもある.
$0$ を単に $R$ の加法に関する単位元と呼ぶ.

加法の逆元の一意性を示す.
$b \in R$ を $a$ の任意の加法に関する左逆元とすると,
\begin{equation*}
b+a = 0
\end{equation*}
となるが, $a$ の右逆元 $-a$ をこの式の右側から加えると, $0$ が $R$ の加法に関する右単位元でもあることから,
\begin{align*}
b+a+(-a) & = 0+(-a), \\
b+0 & = -a, \\
b & = -a.
\end{align*}
したがって, 各 $a$ に対して, その逆元 $-a$ は一意的に定まる.

加法の単位元 $0$ の一意性を示す.
$R$ の元 $b$ が, 任意の $a \in R$ に対して
\begin{equation*}
b+a = a
\end{equation*}
を満たすとする. この式の両辺に $a$ の逆元 $-a$ を右側から加えると, $0$ が $R$ の加法に関する右逆元でもあることから
\begin{align*}
b+a+(-a) & = a+(-a), \\
b+0 & = 0, \\
b & = 0
\end{align*}
が成り立つ. よって, $R$ の加法に関する逆元 $0$ は一意的に定まる.

したがって, 環 $R$ は加法に関して一意的な単位元と各元 $a \in R$ に対する一意的な逆元を持ち, 群をなす.

環論においては, 単位元 $e$ を持つ環を考えることが多い. これに関して次の公理が要求される.
II. b) 任意の $a \in R$ に対して, $R$ のある元 $e$ で
\begin{equation*}
ea=a
\end{equation*}
を満たすものが存在する. これを $R$ における乗法に関する左単位元と呼ぶ.
$ea=a$ であるが, $ae=a$ とは限らない. しかしもし $R$ において, 乗法に関する右単位元 $e'$ が存在すれば両者は一致する.
\begin{equation*}
e' = ee' = e.
\end{equation*}

タグ：環 van der Waerden, "Algebra"

posted by 底彦 at 18:25 | Comment(0) | TrackBack(0) | 数学

2021年01月25日

久し振りに数学をやる

3 時起床.

数学をやる. 鬱の波の中にあると数学のような深い集中が必要なことはほぼできない.

これまでのノートを読み返して, 新しい箇所に進む.
本の一つ一つの記述を解読するように読んでいくのが面白い.
昼過ぎまで続ける.

散歩を兼ねて買い物に行く. 晴れていて歩くのが気持ちいい.

夕方に食事. 鯖と玉葱のパスタ.

後片付けをして休む.

タグ：数学の勉強鯖と玉葱のパスタ

posted by 底彦 at 23:30 | Comment(0) | TrackBack(0) | 数学

2021年01月04日

数学の勉強～買い物

1 時半起床.

今日は体調が良い.
数学をやる. Emily Riehl の教科書 .
図式の極限について書かれた章. 数学をするのは久し振りなので最初はなかなか頭が働かない.

ノートをとりながら昼まで勉強する.

昼過ぎに買い物に出かける. 野菜や肉を買う.

午前中で疲れてしまい, 帰宅して横になって休む.

夕食はソーセージとトマトとキャベツ.

片付けをして休む.

タグ： Emily Riehl "Category Theory in Context" 数学の勉強ソーセージとトマトとキャベツ

posted by 底彦 at 23:30 | Comment(0) | TrackBack(0) | 数学

2020年05月13日

数学: 2 つの平面が交わる直線を求める

3 次元空間内の 2 平面
\begin{align*}
\DeclareMathOperator{\Ar}{Ar}
\DeclareMathOperator{\Arccos}{Arccos}
\DeclareMathOperator{\Arcsin}{Arcsin}
\DeclareMathOperator{\Arr}{Arr}
\DeclareMathOperator{\arr}{arr}
\DeclareMathOperator{\Aut}{Aut}
\DeclareMathOperator{\Auto}{Auto}
\DeclareMathOperator{\Card}{card}
\DeclareMathOperator{\card}{card}
\DeclareMathOperator{\Cocone}{Cocone}
\DeclareMathOperator{\Codomain}{cod}
\DeclareMathOperator{\Colim}{colim}
\DeclareMathOperator{\colim}{colim}
\DeclareMathOperator{\Cone}{Cone}
\DeclareMathOperator{\Conj}{Conj}
\DeclareMathOperator{\Domain}{dom}
\DeclareMathOperator{\Ev}{ev}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\IM}{Im}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\INIT}{init}
\DeclareMathOperator{\mor}{arr}
\DeclareMathOperator{\Nat}{Nat}
\DeclareMathOperator{\Ob}{Ob}
\DeclareMathOperator{\ob}{ob}
\DeclareMathOperator{\Path}{Path}
\DeclareMathOperator{\RE}{Re}
\DeclareMathOperator{\SF}{SF}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Sub}{Sub}
\DeclareMathOperator{\TERM}{term}
\newcommand{\Abs}[1]{\lvert{#1}\rvert}
\newcommand{\Bs}{\backslash}
\newcommand{\Cdot}{\,\cdot^{\mathrm{op}}}
\newcommand{\Comma}[2]{{{#1}\!\downarrow\!{#2}}}
\newcommand{\CommaCat}[2]{(#1/#2)}
\newcommand{\Complement}[1]{{\smash[t]{\mathstrut #1}}^{\mathrm{c}}}
\newcommand{\Emph}[1]{\textit{#1}}
\newcommand{\Eqclass}[4]{{#1#2#3}_{#4}}
\newcommand{\EqCls}[2]{{\left[#1\right]}_{#2}}
\newcommand{\Eqcls}[1]{\left[#1\right]}
\newcommand{\Expt}[2]{{\smash[t]{\mathstrut #1}}^{\mathstrut #2}}
\newcommand{\FnRest}[2]{{#1}|{#2}}
\newcommand{\Func}[2]{\mathrm{Func}(#1,#2)}
\newcommand{\g}{\varg}
\newcommand{\Id}[1]{\mathrm{id}_{#1}}
\newcommand{\Inc}[2]{\mathrm{incl}\left(#1,#2\right)}
\newcommand{\Incl}[2]{\mathrm{incl}_{#1}^{#2}}
\newcommand{\InclArrow}[2]{\morphism(0,0)/>->/<450,0>[\Incl{#1}{#2} : {#1}\,\,`{#2};]}
\newcommand{\Ip}{\rotatebox[origin=c]{180}{$\Pi$}}
\newcommand{\Lb}[1]{\mathrm{lb}(#1)}
\newcommand{\LH}{\mathrm{LH}}
\newcommand{\Lowerset}[1]{\downarrow\!\!{#1}}
\newcommand{\Leadsto}{\quad\leadsto\quad}
\newcommand{\Lrsquigarrow}{\quad\leftrightsquigarrow\quad}
\newcommand{\Mb}[1]{\mathbf{#1}}
\newcommand{\Mbb}[1]{\mathbb{#1}}
\newcommand{\Mi}[1]{\mathit{#1}}
\newcommand{\Mlb}[1]{\mathrm{mlb}(#1)}
\newcommand{\Mr}[1]{\mathrm{#1}}
\newcommand{\Ms}[1]{\mathscr{#1}}
\newcommand{\Mt}[1]{\mathtt{#1}}
\newcommand{\Mub}[1]{\mathrm{mub}(#1)}
\newcommand{\Opp}[1]{#1^{\mathrm{op}}}
\newcommand{\Prj}[2]{\mathrm{proj}\left(#1,#2\right)}
\newcommand{\Proj}[2]{\mathrm{proj}^{#1}_{#2}}
\newcommand{\Pw}{\mathbf{P}}
\newcommand{\Rn}[1]{{\bmdefine{R}}^{#1}}
\newcommand{\q}{\hspace{1em}}
\newcommand{\qq}{\hspace{0.5em}}
\newcommand{\Rel}[1]{\langle{#1}\rangle}
\newcommand{\Rest}[2]{{#1}|{#2}}
\newcommand{\SkelCat}[1]{\mathrm{sk}{#1}}
\newcommand{\Slash}[1]{{\ooalign{\hfil/\hfil\crcr$#1$}}}
\newcommand{\SliCat}[2]{{#1}\,\big/\,{#2}}
\newcommand{\Src}{d^{0,\mathrm{op}}}
\newcommand{\ssqrt}[1]{\sqrt{\smash[b]{\mathstrut #1}}}
\newcommand{\Tgt}{d^{1,\mathrm{op}}}
\newcommand{\TwArCat}[1]{\mathrm{Tw}(#1)}
\newcommand{\Ub}[1]{\mathrm{ub}(#1)}
\newcommand{\Un}[1]{{1}_{#1}}
\newcommand{\Upperset}[1]{\uparrow\!\!{#1}}
\newcommand{\VectCat}[1]{#1 \mathchar`- \mathbf{Vect}}
\newcommand{\VS}{\vspace*{-1ex}}
\newcommand{\Wbar}[1]{\widebar{#1}}
\newcommand{\Ab}{\mathbf{Ab}}
\newcommand{\Affine}{\mathbf{Affine}}
\newcommand{\Ban}{\mathbf{Ban}}
\newcommand{\CAT}{\mathbf{CAT}}
\newcommand{\Cat}{\mathbf{Cat}}
\newcommand{\Ch}{\mathbf{Ch}}
\newcommand{\cHaus}{\mathbf{cHaus}}
\newcommand{\Cluster}{\mathbf{Cluster}}
\newcommand{\CRing}{\mathbf{CRing}}
\newcommand{\DirGraph}{\mathbf{DirGraph}}
\newcommand{\Euclid}{\mathbf{Euclid}}
\newcommand{\Field}{\mathbf{Field}}
\newcommand{\Fin}{\mathbf{Fin}}
\newcommand{\FinMetric}{\mathbf{FinMetric}}
\newcommand{\Graph}{\mathbf{Graph}}
\newcommand{\GrMod}{\mathbf{GrMod}}
\newcommand{\Grp}{\mathbf{Grp}}
\newcommand{\Group}{\mathbf{Group}}
\newcommand{\Groupoid}{\mathbf{Groupoid}}
\newcommand{\Htpy}{\mathbf{Htpy}}
\newcommand{\Man}{\mathbf{Man}}
\newcommand{\Mat}{\mathbf{Mat}}
\newcommand{\Meas}{\mathbf{Meas}}
\newcommand{\Measure}{\mathbf{Measure}}
\newcommand{\Mod}{\mathbf{Mod}}
\newcommand{\Model}{\mathbf{Model}}
\newcommand{\Mon}{\mathbf{Mon}}
\newcommand{\Monoid}{\mathbf{Monoid}}
\newcommand{\oMega}{\bm{\omega}}
\newcommand{\One}{\mathbb{1}}
\newcommand{\PCluster}{\mathbf{PCluster}}
\newcommand{\POs}{\mathbf{Poset}}
\newcommand{\Poset}{\mathbf{Poset}}
\newcommand{\PROJ}{\mathbf{Proj}}
\newcommand{\Psh}{\mathbf{Psh}}
\newcommand{\Ring}{\mathbf{Ring}}
\newcommand{\Rng}{\mathbf{Rng}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Top}{\mathbf{Top}}
\newcommand{\Two}{\mathbb{2}}
\newcommand{\Vect}{\mathbf{Vect}}
\newcommand{\Zero}{\mathbb{0}}
\newcommand{\sA}{\mathscr{A}}
\newcommand{\sB}{\mathscr{B}}
\newcommand{\sC}{\mathscr{C}}
\newcommand{\sD}{\mathscr{D}}
\newcommand{\sE}{\mathscr{E}}
\newcommand{\sF}{\mathscr{F}}
\newcommand{\sG}{\mathscr{G}}
\newcommand{\sH}{\mathscr{H}}
\newcommand{\sI}{\mathscr{I}}
\newcommand{\sJ}{\mathscr{J}}
\newcommand{\sK}{\mathscr{K}}
\newcommand{\sL}{\mathscr{L}}
\newcommand{\sM}{\mathscr{M}}
\newcommand{\sN}{\mathscr{N}}
\newcommand{\sO}{\mathscr{O}}
\newcommand{\sP}{\mathscr{P}}
\newcommand{\sQ}{\mathscr{Q}}
\newcommand{\sR}{\mathscr{R}}
\newcommand{\sS}{\mathscr{S}}
\newcommand{\sT}{\mathscr{T}}
\newcommand{\sU}{\mathscr{U}}
\newcommand{\sV}{\mathscr{V}}
\newcommand{\sW}{\mathscr{W}}
\newcommand{\sX}{\mathscr{X}}
\newcommand{\sY}{\mathscr{Y}}
\newcommand{\sZ}{\mathscr{Z}}
\newcommand{\bfA}{\mathbf{A}}
\newcommand{\bfB}{\mathbf{B}}
\newcommand{\bfC}{\mathbf{C}}
\newcommand{\bfD}{\mathbf{D}}
\newcommand{\bfE}{\mathbf{E}}
\newcommand{\bfF}{\mathbf{F}}
\newcommand{\bfG}{\mathbf{G}}
\newcommand{\bfH}{\mathbf{H}}
\newcommand{\bfI}{\mathbf{I}}
\newcommand{\bfJ}{\mathbf{J}}
\newcommand{\bfK}{\mathbf{K}}
\newcommand{\bfL}{\mathbf{L}}
\newcommand{\bfM}{\mathbf{M}}
\newcommand{\bfN}{\mathbf{N}}
\newcommand{\bfO}{\mathbf{O}}
\newcommand{\bfP}{\mathbf{P}}
\newcommand{\bfQ}{\mathbf{Q}}
\newcommand{\bfR}{\mathbf{R}}
\newcommand{\bfS}{\mathbf{S}}
\newcommand{\bfT}{\mathbf{T}}
\newcommand{\bfU}{\mathbf{U}}
\newcommand{\bfV}{\mathbf{V}}
\newcommand{\bfW}{\mathbf{W}}
\newcommand{\bfX}{\mathbf{X}}
\newcommand{\bfY}{\mathbf{Y}}
\newcommand{\bfZ}{\mathbf{Z}}
\newcommand{\Bfa}{\mathbf{a}}
\newcommand{\Bfb}{\mathbf{b}}
\newcommand{\Bfc}{\mathbf{c}}
\newcommand{\Bfd}{\mathbf{d}}
\newcommand{\Bfe}{\mathbf{e}}
\newcommand{\Bff}{\mathbf{f}}
\newcommand{\Bfg}{\mathbf{g}}
\newcommand{\Bfh}{\mathbf{h}}
\newcommand{\Bfi}{\mathbf{i}}
\newcommand{\Bfj}{\mathbf{j}}
\newcommand{\Bfk}{\mathbf{k}}
\newcommand{\Bfl}{\mathbf{l}}
\newcommand{\Bfm}{\mathbf{m}}
\newcommand{\Bfn}{\mathbf{n}}
\newcommand{\Bfo}{\mathbf{o}}
\newcommand{\Bfp}{\mathbf{p}}
\newcommand{\Bfq}{\mathbf{q}}
\newcommand{\Bfr}{\mathbf{r}}
\newcommand{\Bfs}{\mathbf{s}}
\newcommand{\Bft}{\mathbf{t}}
\newcommand{\Bfu}{\mathbf{u}}
\newcommand{\Bfv}{\mathbf{v}}
\newcommand{\Bfw}{\mathbf{w}}
\newcommand{\Bfx}{\mathbf{x}}
\newcommand{\Bfy}{\mathbf{y}}
\newcommand{\Bfz}{\mathbf{z}}
\newcommand{\rA}{\mathrm{A}}
\newcommand{\rB}{\mathrm{B}}
\newcommand{\rC}{\mathrm{C}}
\newcommand{\rD}{\mathrm{D}}
\newcommand{\rE}{\mathrm{E}}
\newcommand{\rF}{\mathrm{F}}
\newcommand{\rG}{\mathrm{G}}
\newcommand{\rH}{\mathrm{H}}
\newcommand{\rI}{\mathrm{I}}
\newcommand{\rJ}{\mathrm{J}}
\newcommand{\rK}{\mathrm{K}}
\newcommand{\rL}{\mathrm{L}}
\newcommand{\rM}{\mathrm{M}}
\newcommand{\rN}{\mathrm{N}}
\newcommand{\rO}{\mathrm{O}}
\newcommand{\rP}{\mathrm{P}}
\newcommand{\rQ}{\mathrm{Q}}
\newcommand{\rR}{\mathrm{R}}
\newcommand{\rS}{\mathrm{S}}
\newcommand{\rT}{\mathrm{T}}
\newcommand{\rU}{\mathrm{U}}
\newcommand{\rV}{\mathrm{V}}
\newcommand{\rW}{\mathrm{W}}
\newcommand{\rX}{\mathrm{X}}
\newcommand{\rY}{\mathrm{Y}}
\newcommand{\rZ}{\mathrm{Z}}
\newcommand{\sfA}{\mathsf{A}}
\newcommand{\sfB}{\mathsf{B}}
\newcommand{\sfC}{\mathsf{C}}
\newcommand{\sfD}{\mathsf{D}}
\newcommand{\sfE}{\mathsf{E}}
\newcommand{\sfF}{\mathsf{F}}
\newcommand{\sfG}{\mathsf{G}}
\newcommand{\sfH}{\mathsf{H}}
\newcommand{\sfI}{\mathsf{I}}
\newcommand{\sfJ}{\mathsf{J}}
\newcommand{\sfK}{\mathsf{K}}
\newcommand{\sfL}{\mathsf{L}}
\newcommand{\sfM}{\mathsf{M}}
\newcommand{\sfN}{\mathsf{N}}
\newcommand{\sfO}{\mathsf{O}}
\newcommand{\sfP}{\mathsf{P}}
\newcommand{\sfQ}{\mathsf{Q}}
\newcommand{\sfR}{\mathsf{R}}
\newcommand{\sfS}{\mathsf{S}}
\newcommand{\sfT}{\mathsf{T}}
\newcommand{\sfU}{\mathsf{U}}
\newcommand{\sfV}{\mathsf{V}}
\newcommand{\sfW}{\mathsf{W}}
\newcommand{\sfX}{\mathsf{X}}
\newcommand{\sfY}{\mathsf{Y}}
\newcommand{\sfZ}{\mathsf{Z}}
\newcommand{\bbA}{\mathbb{A}}
\newcommand{\bbB}{\mathbb{B}}
\newcommand{\bbC}{\mathbb{C}}
\newcommand{\bbD}{\mathbb{D}}
\newcommand{\bbE}{\mathbb{E}}
\newcommand{\bbF}{\mathbb{F}}
\newcommand{\bbG}{\mathbb{G}}
\newcommand{\bbH}{\mathbb{H}}
\newcommand{\bbI}{\mathbb{I}}
\newcommand{\bbJ}{\mathbb{J}}
\newcommand{\bbK}{\mathbb{K}}
\newcommand{\bbL}{\mathbb{L}}
\newcommand{\bbM}{\mathbb{M}}
\newcommand{\bbN}{\mathbb{N}}
\newcommand{\bbO}{\mathbb{O}}
\newcommand{\bbP}{\mathbb{P}}
\newcommand{\bbQ}{\mathbb{Q}}
\newcommand{\bbR}{\mathbb{R}}
\newcommand{\bbS}{\mathbb{S}}
\newcommand{\bbT}{\mathbb{T}}
\newcommand{\bbU}{\mathbb{U}}
\newcommand{\bbV}{\mathbb{V}}
\newcommand{\bbW}{\mathbb{W}}
\newcommand{\bbX}{\mathbb{X}}
\newcommand{\bbY}{\mathbb{Y}}
\newcommand{\bbZ}{\mathbb{Z}}
\begin{cases}
a_1x+b_1y+c_1z = d_1 & ~ \\
a_2x+b_2y+c_2z = d_2 & ~
\end{cases}
\end{align*}
を考える.

2 平面が平行でなければ, これらは 1 つの直線で交わる. その直線の方程式を求める.

これは上記の 2 平面を連立方程式として解くことによって求められる.

計算の結果, 得られる直線の方程式は以下のようになる.
まず,
\begin{alignat*}{4}
D_1 & = \begin{vmatrix}
a_1 & b_1 \\
a_2 & b_2
\end{vmatrix},
& \quad &
D_2 & = \begin{vmatrix}
c_1 & a_1 \\
c_2 & a_2
\end{vmatrix},
& \quad &
D_3 & = \begin{vmatrix}
b_1 & c_1 \\
b_2 & c_2
\end{vmatrix}, \\
\\
D_4 & = \begin{vmatrix}
a_1 & d_1 \\
a_2 & d_2
\end{vmatrix},
& \quad &
D_5 & = \begin{vmatrix}
b_1 & d_1 \\
b_2 & d_2
\end{vmatrix},
& \quad &
D_6 & = \begin{vmatrix}
c_1 & d_1 \\
c_2 & d_2
\end{vmatrix}
\end{alignat*}
とおく.

(1) $D_1 \neq 0$ のとき, 求める直線の方程式はパラメンーターを $t$ として,
\begin{equation}
\label{eq1}
\left( D_3t-\frac{D_5}{D_1},\, D_2t+\frac{D_4}{D_1},\, D_1t \right) \tag{1}
\end{equation}
となる.

(2) $D_2 \neq 0$ のとき,
\begin{equation}
\label{eq2}
\left( D_3t+\frac{D_6}{D_2},\, D_2t,\, D_1t-\frac{D_4}{D_2} \right) \tag{2}
\end{equation}
となる.

(3) $D_3 \neq 0$ のとき,
\begin{equation}
\label{eq3}
\left( D_3t,\, D_2t-\frac{D_6}{D_3},\, D_1t+\frac{D_5}{D_3} \right) \tag{3}
\end{equation}

(4) $D_1=D_2=D_3=0$ のとき, 2 平面は平行であり交わらない.

特に,
\begin{equation*}
d_1=d_2=0
\end{equation*}
のとき, すなわち 2 平面が共に原点を通るとき求める直線の方程式は
\begin{equation*}
\left( D_3t,\, D_2t,\, D_1t \right)
\end{equation*}
となる.

計算してみるとわかるが, きれいな結果である.

具体例を計算してみる.
\begin{equation}
\label{eq4}
\begin{cases}
5x+6y+7z=8 & ~ \\
x+2y+3z=4 & ~
\end{cases} \tag{4}
\end{equation}
を解く.
\begin{equation*}
D_1=4,\, D_2=-8,\, D_3=4,\, D_4=12,\, D_5=8,\, D_6=4
\end{equation*}
である. $D_1 \neq 0, D_2 \neq 0, D_3 \neq 0$ だから, この方程式の解は (\ref{eq1}), (\ref{eq2}), (\ref{eq3}) により 3 通りの仕方で表わされる.
(\ref{eq1}) による解は
\begin{equation}
\label{eq5}
(4t-2,\, -8t+3,\, 4t) \tag{5}
\end{equation}
である. (\ref{eq2}) による解は
\begin{equation}
\label{eq6}
\left( 4t-\frac{1}{2},\, -8t,\, 4t+\frac{3}{2} \right) \tag{6}
\end{equation}
である. (\ref{eq3}) による解は
\begin{equation}
\label{eq7}
(4t,\, -8t-1,\, 4t+2) \tag{7}
\end{equation}
である.

表わし方は異っているるが, これらは全て同じ直線の異なる表現である. 実際に (\ref{eq5}) で $t=t'+\frac{3}{8}$ とおけば
\begin{equation*}
\left( 4t'-\frac{1}{2},\, -8t',\, 4t'+\frac{3}{2} \right)
\end{equation*}
となり (\ref{eq6}) が得られる. さらに (\ref{eq5}) で $t=t'+\frac{1}{2}$ とおけば
\begin{equation*}
(4t',\, -8t'-1,\, 4t'+2)
\end{equation*}
となり (\ref{eq7}) が得られる.

タグ：線形代数 2 平面の交わりの直線

posted by 底彦 at 23:30 | Comment(0) | TrackBack(0) | 数学

- 1 2 3 4 5 .. >>

<< 2024年12月 >>
日	月	火	水	木	金	土
1	2	3	4	5	6	7
8	9	10	11	12	13	14
15	16	17	18	19	20	21
22	23	24	25	26	27	28
29	30	31