Mercurial > hg > Members > kono > Proof > category
changeset 0:302941542c0f
category agda
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 06 Jul 2013 00:34:08 +0900 |
| parents | |
| children | 73b780d13f60 |
| files | category.ind list.agda nat.agda |
| diffstat | 3 files changed, 1708 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/category.ind Sat Jul 06 00:34:08 2013 +0900 @@ -0,0 +1,1601 @@ +-title: Cateogry + +\usepackage{tikz} +\usepackage{tikz-cd} + +--Adjunction + +\begin{eqnarray*} +Uε○ηU & = & 1_U \\ +εF○Fη & = & 1_F +\end{eqnarray*} + +$f: a -> Ub $ + +--begin-comment: + FU(b) + ・ | + ・ | + F(f) ・ | + ・ ε(b) + ・ | + ・ f* v + F(a) -----------------> b + + U(f*) + UF(a) -----------------> Ub + ^ ・ + | ・ + | ・ + η(a) ・ f + | ・ + | ・ f = U(f*)η + |・ + a + +--end-comment: + +\begin{tikzcd} +\mbox{} & FU(b) \arrow{d}{ε(b)} \\ +F(a) \arrow{ru}{F(f)} \arrow{r}{f*} & b \\ +UF(a) \arrow{r}{U(f*)} & Ub \\ +a \arrow{u}{η(a)} \arrow{ru}{f} & \\ +\end{tikzcd} + +Universal mapping problem is +for each $f:->Ub$, there exists $f*$ such that $f = U(f*)η$. + +--Adjunction to Universal mapping + +In adjunction $(F,U,ε,η)$, put $f* = ε(b)F(f)$, +we are going to prove $f*$ is a solution of Universal mmapping problem. That is $U(f*)η = f$. + +\begin{tikzcd} +UF(a) \arrow{r}[swap]{UF(f)} \arrow[bend left]{rr}{U(ε(b)F(f))=U(f*)} +& UFUb \arrow{r}[swap]{U(ε(b))} & \mbox{?} \\ +a \arrow{u}{η(a)} \arrow{r}[swap]{f} & Ub \arrow{u}{η(Ub)} \\ +\end{tikzcd} + +\begin{tikzcd} +UF(a) \arrow{rd}[swap]{U(f*)} \arrow{r}{UF(f)} & UFUb \arrow[bend left]{d}{U(ε(b))} \\ +a \arrow{u}{η(a)} \arrow{r}[swap]{f} & Ub \arrow{u}{η(Ub)} \\ +F(a) \arrow{r}{F(f)} \arrow{rd}[swap]{f*} & FU(b) \arrow{d}{ε(b)} \\ +\mbox{} & b \\ +\end{tikzcd} +∵$ Uε○ηU = 1_U $ + +\[ U(ε(b))η(U(b)) = 1_{U(b)} \] + +means that + +$ε(b) : FU(b)->b $ is solution of $1_{U(b)}$. + +naturality $ fη(U(b)) = U(F(f))η(a) $ + +gives solution $ U(ε(b))UF(f) = U(F(f)ε(b)) $ for $f$. + + + +\[ U(f*)η(a)(a) = f(a) \] + +then + +$U(ε(b)F(f))η(a)(a) = U(ε(b))UF(f)η(a)(a) $ + +since $F$ is a functor. And we have + +$U(ε(b))UF(f)η(a)(a) = U(ε(b))η(b)f(a)$ + +because of naturality of $η$ + +--begin-comment: + η(a) + UF(a) <------- a UF(f)η(a) = η(b)f + | | + |UF(f) f| + v v + UF(b) <------- b + η(b) + +--end-comment: + +\begin{tikzcd} +UF(a) \arrow[leftarrow]{r}{η(a)} \arrow{d}{UF(f)} & a \arrow{d}{f} & UF(f)η(a) = η(b)f \\ +UF(b) \arrow[leftarrow]{r}{η(b)} & b & +\end{tikzcd} + +too bad.... we need some thing more. + + +---Adjoint of η + +$ Uε○ηU = 1_U $ + +--begin-comment: + F(f) ε(b) + F(a) ---------> FU(b) --------> b + + UF(f) U(ε(b)) + UF(a) --------> UFU(b) --------> U(b) + + η(a) UF(f) U(ε(b)) + a ---------> UF(a) --------> UFU(b) --------> U(b) + + f η(Ub) U(ε(b)) + a ---------> Ub --------> UFU(b) --------> U(b) + + η(Ub) U(ε(b)) = 1 + ∵ Uε○ηU = 1_U + +--end-comment: + +\begin{tikzcd} +F(a) \arrow{r}{F(f)} & FU(b) \arrow{r}{ε(b)} & b & \\ +UF(a) \arrow{r}{UF(f)} & UFU(b) \arrow{r}{U(ε(b))} & U(b) & \\ +a \arrow{r}{η(a)} & UF(a) \arrow{r}{UF(f)} & UFU(b) \arrow{r}{U(ε(b))} & U(b) \\ +a \arrow{r}{f} & Ub \arrow{r}{η(Ub)}[swap]{η(Ub)} & UFU(b) \arrow{r}{U(ε(b))}[swap]{U(ε(b))=1} & U(b) \\ +\end{tikzcd} + + +∵ $Uε○ηU = 1_U$ + +naturality of $f:a->Ub$ + +--begin-comment: + + η(Ub) + Ub ---------> UF(Ub) + ^ ^ + | | + f| |UF(f) + | η(a) | + a ---------> UF(a) + +--end-comment: + +\begin{tikzcd} +Ub \arrow{r}{η(Ub)} & UF(Ub) \\ +a \arrow{u}{f} \arrow{r}{η(a)} & UF(a) \arrow{u}[swap]{UF(f)} +\end{tikzcd} + +--begin-comment: + + UF(f) + UF(a) ------------->UF(U(b)) UF(U(b)) + ^ ^ | + | | | +η(a)| η(U(b))| |U(ε(U(b))) + | f | v + a --------------->U(b) U(b) + +--end-comment: + +\begin{tikzcd} +UF(a) \arrow{r}{UF(f)} & UF(U(b)) & UF(U(b)) \arrow{d}{U(ε(U(b)))} & \mbox{} \\ +a \arrow{r}{f} \arrow{u}[swap]{η(a)} & U(b) \arrow{u}[swap]{η(U(b))} & U(b) & \mbox{} \\ +\end{tikzcd} + +Solution of universal mapping yields naturality of $Uε○ηU = 1_U$. + +--begin-comment: + + F(η(a)) + UF(a) F(a) ----------> FUF(a) + ^ | + | | +η(a)| |ε(F(a)) + | η(a) v + a --------------->UF(a) F(a) + +--end-comment: + +$εF○Fη = 1_F$. + +\begin{tikzcd} +UF(a) \arrow{rd}[swap]{1_{UF(a)}} & F(a) \arrow{r}{F(η(a))} \arrow{rd}{1_{F(a)}}[swap]{(1_{UF(a)})*} & FUF(a) \arrow{d}{ε(F(a))} & \mbox{} \\ +a \arrow{r}[swap]{η(a)} \arrow{u}{η(a)} & UF(a) & F(a) & \mbox{} \\ +\end{tikzcd} + +--Universal mapping to adjunction + +Functor $U$, mapping $F(a)$ and $(f)*, U(f*)η(a) = f $ are given. + +object $F(a):A -> B$ + +$ η(a): a->UF(a)$ + +put +\[ F(f) = (η(b)f)* \] +\[ ε : FU -> 1_B \] +\[ ε(b) = (1_{U(b)})* \] + +--begin-comment: + f* + F(a) -----------------> b + + U(f*) + UF(a) -----------------> Ub + ^ ・ + | ・ + | ・ + η(a) ・ f + | ・ + | ・ f = U(f*)η + |・ + a +--end-comment: + +\begin{tikzcd} +F(a) \arrow{r}{f*} & b \\ +UF(a) \arrow{r}{U(f*)} & Ub \\ +a \arrow{u}{η(a)} \arrow{ur}{f} +\end{tikzcd} + +$f = U(f*)η$ + +Show F is a Functor, that is $F(fg) = F(f)F(g)$. + +Show naturality of $η(a)$. + +\[ f:a->b, F(f) = (η(b)f)*\] + +Show naturality of $ε(b) = (1_U)*$. + +---Definitions + +f's destination +\[ f: a -> U(b) \] +universal mapping +\[ U(f*)η(a) = f \] +defnition of F(f) +\[ F(f) = (η(U(b))f)* \] +definition of $ε$ +\[ ε(b) = (1_{U(b)})* \] + +--begin-comment: + + FU(f*) + FUF(a)------------->FU(b) + ^| | + ||ε(F(a)) | + F(η(a))|| |ε(b)=(1_U(b))* + || (η(Ub)f)*=F(f) | + |v v + F(a) --------------->b + f* + UF(f) + UF(a)------------->UFU(b) + ^ ^| + | U(f*) || + η(a)| η(U(b))||U(ε(b)) + | || + | |v + a --------------->U(b) + f + +--end-comment: + +\begin{tikzcd} +FUF(a) \arrow{r}{FU(f*)} \arrow{d}{ε(F(a))} & FU(b) \arrow{d}{ε(b)=(1_U(b))*} & \mbox{} \\ +F(a) \arrow{r}[swap]{f*} \arrow[bend left]{u}{F(η(a))} \arrow{ru}[swap]{F(f)} & b & \mbox{} \\ +UF(a) \arrow{r}{UF(f)} \arrow{rd}[swap]{U(f*)} & UFU(b) \arrow[bend left]{d}{U(ε(b))} & \mbox{} \\ +a \arrow{r}[swap]{f} \arrow{u}{η(a)} & U(b) \arrow{u}{η(U(b))} & \mbox{} \\ +\end{tikzcd} + +$εF○Fη = 1_F$, +$ ε(b) = (1_{U(b)})* $, + +$ ε(F(a)) = (1_{UF(a)})* $ + + +--begin-comment: + + F(η(a)) + UF(a) F(a) --------------> FUF(a) + ^ |^ + | || + η(a)| U(1_{F(a)}) 1_{F(a)} ε(F(a))||F(η(a)) + | || + | v| + a ---------------> U(F(a)) F(a) + η(a) + +--end-comment: + +\begin{tikzcd} +UF(a) \arrow{rd}{U(1_{F(a)}) } & F(a) \arrow{r}{F(η(a))} \arrow{rd}[swap]{1_{F(a)}} & FUF(a) \arrow{d}[swap]{ε(F(a))} & \mbox{} \\ +a \arrow{r}[swap]{η(a)} \arrow{u}{η(a)} & U(F(a)) & F(a) \arrow[bend right]{u}[swap]{F(η(a))} & \mbox{} \\ +\end{tikzcd} + + + + + +--- Functor F + +\[ F(f) = (η(b)f)* \] + +\[ U(F(f))η(a) = η(b)f \] + + +show $F(fg) = F(f)F(g)$ + + +--begin-comment: + g f + a -----> Ub ----> UUc +--end-comment: + +\begin{tikzcd} +a \arrow{r}{g} & Ub \arrow{r}{f} & UUc +\end{tikzcd} + +\begin{eqnarray*} +U(F(g))η(a) & = & η(Ub)g \\ +U(F(f))η(Ub) & = & η(UUc)f +\end{eqnarray*} + +show +\[ +U(F(f)F(g))η(a) = η(UUc)fg +\] + +then $F(f)F(g) = F(fg)$ + +\begin{eqnarray*} +U(F(f)F(g))η(a) & = & UF(f)UF(g)η(a) \\ +& = & UF(f)η(Ub)g \\ +& = & η(UUc)fg +\end{eqnarray*} +\mbox{Q.E.D.} + +--begin-comment: + FU(f) + FU(b) -------------> FUU(c) + ・ | | + ・ | | + F(g) ・ | | + ・ ε(b) ε(Uc) | + ・ | | + ・ g* v f* v + F(a) -----------------> b ---------------> c + + U(F(f)) + UF(a) UFUb + ^ ・ ^ ・ + | ・ | ・ + | ・ | ・ + η(a) ・ UFg | ・ UFf + | ・ η(Ub) ・ + | ・ | ・ + | g ・ | f ・ + a -----------------> Ub ---------------> UU(c) +--end-comment: + + +\begin{tikzcd} +F(a) \arrow{r}{F(g)} \arrow{rd}{g*}& FU(b) \arrow{r}{FU(f)} \arrow{d}{ε(b)} \arrow{rd}{f*} & FUU(c) \arrow{d}{ε(Uc)} \\ +\mbox{} & b & U(c) \\ +\\ +UF(a) \arrow{rd}{U(g*)} \arrow{r}{UFg} & UFUb \arrow{rd}{Uf*} \arrow{r}{UFf} & UFUUc \\ +a \arrow{r}{g}\arrow{u}{η(a)} & Ub \arrow{r}{f} \arrow{u}[swap]{η(Ub)} & UU(c) \arrow{u}[swap]{η(UUc)} +\end{tikzcd} + +--- naturality of η + +$ η: 1->UB $ + +--begin-comment: + + UF(a)-----------------> UFb + ^ UF(f) ^ + | | + | | + η(a) η(b) + | | + | f | + a -----------------> b +--end-comment: + +\begin{tikzcd} +UF(a) \arrow{r}[swap]{UF(f)} & UFb \\ +a \arrow{r}{f} \arrow{u}{η(a)} & b \arrow{u}{η(b)} +\end{tikzcd} + +prove $η(b)f = UF(f)η(a) $ +\begin{eqnarray*} +& η(b)f: & a-> UFb \\ +F(f) & = & (η(b)f)* \mbox{\hspace{1cm}(definition)} \\ +η(b)f & = & U(F(f))η(a) +\end{eqnarray*} +\mbox{Q.E.D.} + +--- naturality of ε + +\[ +ε : FU -> 1_B +\] +\[ +U: B->A +\] + +$ ε(b) = (1_{U(b)})*$ + +$ U(ε(b))η(U(b)) = 1_{U(b)}$ + +$ U(ε(b))η(U(b))U(b) = U(b)$ + + +--begin-comment: + FU(f) + FU(b) -------------> FU(c) + | | + | | + ε(b) | ε(c) + | | + v f v + b ---------------> c +--end-comment: + +\begin{tikzcd} +FU(b) \arrow{r}{FU(f)} \arrow{d}{ε(b)} & FU(c) \arrow{d}{ε(c)}\\ +b \arrow{r}{f} & c +\end{tikzcd} + +prove $fε(b) = ε(c)FU(f)$ + + +\[ f = Ub -> Uc \] + +--begin-comment: + + FU(f) (1_U(c))* + F(Ub) --------------> FU(c) ---------------> c + + (1_U(b))* f + F(Ub) ----------------> b -----------------> c + + U(1_U(b)*) U(f) + UF(Ub) ----------------> Ub -----------------> U(c) + || ・ || + || ・ || + || UFU(f) ・ U(1_U(c)*) || + UF(Ub) ----- ・ ------> UFUc ---------------> U(c) + ^ ・ ^ || + | ・ | || + η(Ub) ・ 1_Ub η(Uc) | || + |・ | 1_Uc || + Ub ------------------> Uc -----------------> U(c) + U(f) + +--end-comment: + +\begin{tikzcd} +F(Ub) \arrow{r}{(1_{U(b)})*} & b \arrow{r}{f} & c \\ +UF(Ub) \arrow{r}{U(1_{U(b)})*} \arrow{rd}[swap]{UFU(f)} & Ub \arrow{r}{U(f)} & U(c) \\ +\mbox{} & UFUc \arrow{ru}{U(1_U(c)*)} & \\ +Ub \arrow{r}{U(f)} \arrow{ruu}[swap]{1_{Ub}} \arrow{uu}{η(Ub)} & Uc \arrow{ruu}[swap]{1_{Uc}} \arrow{u}{η(Uc)} \\ +F(Ub) \arrow{r}{FU(f)} & FU(c) \arrow{r}{(1_{U(c)})*} & c \\ +\end{tikzcd} + +--begin-comment: + +\begin{tikzcd} +\mbox{} & Ub \arrow{r}{U(f)} & U(c) \\ +UF(Ub) \arrow{ru}{U(1_U(b)*)} \arrow{r}[swap]{UFU(f)} & UFUc \arrow{ru}{U(1_U(c)*)} & \\ +Ub \arrow{r}{U(f)} \arrow{ruu}{1_Ub} \arrow{u}{η(Ub)} & Uc \arrow{ruu}[swap]{1_Uc} \arrow{u}{η(Uc)} & \mbox{} +\end{tikzcd} + + +\begin{tikzcd} +UF(Ub) \arrow{d}{U(1_U(b)*)} \arrow{r}{UFU(f)} & UFUc \arrow{d}{U(1_U(c)*)} \\ +Ub \arrow{r}{U(f)} & U(c) \\ +Ub \arrow{r}{U(f)} \arrow{u}{1_Ub} \arrow[bend left]{uu}{η(Ub)} & Uc \arrow{u}[swap]{1_Uc} \arrow[bend right]{uu}[swap]{η(Uc)} +\end{tikzcd} + +--end-comment: + + +show $ε(c)FU(f)$ and $fε(b)$ are both solution of $(1_{Uc})U(f) ( = U(f)(1_{Ub}))$ + +\[ +(fε(b)))η(Ub)Ub = U(f))U(ε(b))η(Ub)Ub +\] +\[ += U(f)1_{U(b)}Ub = U(f)Ub = Ufb = U(f)(1_{Ub})Ub +\] +\[ +\mbox{∴}fε(b) = (U(f)(1_{Ub}))* +\] + +$ UFU(f)η(Ub) = η(Uc)U(f)$ naturality of η + +\[ +U(ε(c)FU(f))η(Ub)Ub = U(ε(c))UFU(f)η(Ub)Ub +\] +\[ += U(ε(c))η(Uc)U(f)Ub = 1_{U(c)}U(f)Ub = U(f)Ub = U(f)(1_{Ub})Ub +\] +\[ +\mbox{∵} U(ε(c))η(Uc) = 1_U(c) +\] + +end of proof. + +--begin-comment: + U(f*) + c U(c) <- ----------- U(b) b + ^ ^| |^ ^ + | U(ε(c))||η(U(c)) η(U(b))||U(ε(b)) | + |ε(c) || || ε(b)| + | |v UFU(f) v| | + FU(c) UFU(c) <----------- UFU(b) FU(b) +--end-comment: + +\begin{tikzcd} +c \arrow[bend left,leftarrow]{rrr}{f} +& U(c) \arrow[leftarrow]{r}{U(f)} \arrow{d}{η(U(c))} & U(b) \arrow{d}[swap]{η(U(b))} & b \\ +FU(c) \arrow{u}{(1_{Uc})* = ε(c)} \arrow[bend right,leftarrow]{rrr}{FU(f)} & +UFU(c) \arrow[leftarrow]{r}{UFU(f)} \arrow[bend left]{u}{U(ε(c))} & UFU(b) \arrow[bend right]{u}[swap]{U(ε(b))} +& FU(b) \arrow{u}[swap]{ε(b) = (1_{Ub})*} +\end{tikzcd} + +It also prove + +\[ Uε○ηU = 1_U\] + +---$Uε○ηU = 1_U$ + +$ ε(b) = (1_U(b))* $ + +that is + +$ U((1_U(b)*)η(U(b)) = 1_U(b) $ +$ U(ε(b))η(U(b)) = 1_U(b) $ + +$ \mbox{∴} Uε○ηU = 1_U $ + +--- $εF○Fη = 1_F$ + +$ η(a) = U(1_F(a))η(a) $ + +$=> (η(a))* = 1_F(a)$ ... (1) + +$ ε(F(a)) = (1_UF(a))*$ + +$=> 1_UF(a) = U(ε(F(a)))η(UF(a)) $ + +times $η(a)$ from left + +$ η(a) = U(ε(F(a)))η(UF(a))η(a)$ + +$η(UF(a)) = UFη(a)$ naturality of $η$ + +$ η(a) = U(ε(F(a)))(UFη(a))η(a) $ \\ +$ = U(ε(F(a)Fη(a)))η(a) $ \\ +$ => (η(a))* = ε(F(a))Fη(a) .... (2) $ \\ + +from (1),(2), since $(η(a))*$ is unique + +\[ ε(F(a))Fη(a) = 1_F(a) \] + +--begin-comment: + + F U + UF(a) --------> FUF(a) ----------> UFUF(a) FUF(a) + ^ ^| |^ ^| + | || || || + |η(a) F(η(a))||ε(F(a)) U(εF(a))||η(UF(a)) ||ε(F(a)) + | || || || + | F |v U v| |v + a ------------> F(a) ------------> UF(a) F(a) +--end-comment: + + +\begin{tikzcd} +UF(a) \arrow{r}{F}& FUF(a) \arrow{rr}{U} \arrow[bend left]{d}{ε(F(a))} & \mbox{} & UFUF(a) \arrow[bend left]{d}{U(εF(a))} \\ +a \arrow{r}{F} \arrow{u}{η(a)} & F(a) \arrow{rr}{U} \arrow[bend left]{u}{F(η(a))} & \mbox{} & UF(a) \arrow[bend left]{u}{η(UF(a))} \\ +\mbox{} & F(a) \arrow{u}{(η(a))* = 1_{Fa}} \arrow{rr}{U} & & UF(a) \arrow{u}[swap]{η(a) = U(εF(a))η(UF(a))} +\end{tikzcd} + +\begin{tikzcd} +UF(a) \arrow{r}{F} & FUF(a) \arrow{r}{U} \arrow[bend left]{d}{ε(F(a))} & UFUF(a) \arrow[bend right]{d}[swap]{U(εF(a))} & FUF(a) \arrow[bend left]{d}{ε(F(a))} & \mbox{} \\ +a \arrow{r}{F} \arrow{u}[swap]{η(a)} & F(a) \arrow{r}{U} \arrow[bend left]{u}{F(η(a))} & UF(a) \arrow[bend right]{u}[swap]{η(UF(a))} & F(a) \arrow{u}{} & \mbox{} \\ +\end{tikzcd} + +--begin-comment: + + UUF(a) + ^ | + | | + η(UF(a))| |U(ε(Fa)) U(ε(F(a))η(UF(a)) = 1_UF(a) + | v ε(F(a) = (1_UF(a))* + UF(a) +--end-comment: + +\begin{tikzcd} +UUF(a) \arrow[bend left]{d}{U(ε(Fa))} \\ +UF(a) \arrow[bend left]{u}{η(UF(a))} +\end{tikzcd} +$U(ε(F(a)))η(UF(a)) = 1_UF(a) $ \\ +$ ε(F(a)) = (1_UF(a))* $ + + +--begin-comment: + FA -------->UFA + | | + | Fη(A) | UFηA + v v + FUFA ------>UFUFA +--end-comment: + +\begin{tikzcd} +FA \arrow{r} \arrow{d}{Fη(A)} & UFA \arrow{d}{UFηA} \\ +FUFA \arrow{r} & UFUFA +\end{tikzcd} + +$ε(FA)$の定義から $U(ε(FA)): UFUFA→UFA$ + +唯一性から $ε(F(A)):FUFA→FA$ 従って + +\[ ε(F(A))Fη(A)=1 \] + +ってなのを考えました。 + + +$ Uη(A') = U(1(FA'))η(A')$より \\ +$ η(A')*=1(FA')$、 \\ +$ Uη(A') = U(ε(FA')Fη(A'))η(A')$より \\ +$ η(A')*=ε(FA')Fη(A')$から \\ +$ 1_F=εF.Fη$は言えました。 \\ + +後者で$η$の自然性と$ε$の定義を使いました。 + + +--おまけ + +$ εF○Fη=1_F, Uε○ηU = 1_U $ +--begin-comment: + + U + UFU(a) <--------------- FU(a) + ^| | + η(U(a))||U(ε(a)) |ε(a) + |v v + U(a) <---------------- (a) + U + + F + FUF(a) <--------------- UF(a) + ^| ^ + Fη(a)||εF(a) |η(a) + |v | + F(a) <---------------- (a) + F + +--end-comment: + +\begin{tikzcd} +UFU(a) \arrow[leftarrow]{r}{U} \arrow[bend left]{d}{U(ε(a))} & FU(a) \arrow{d}{ε(a)} & \mbox{} \\ +U(a) \arrow[leftarrow]{r}[swap]{U} \arrow[bend left]{u}{η(U(a))} & (a) & \mbox{} \\ +FUF(a) \arrow[leftarrow]{r}{F} \arrow[bend left]{d}{εF(a)} & UF(a) & \mbox{} \\ +F(a) \arrow[leftarrow]{r}[swap]{F} \arrow[bend left]{u}{Fη(a)} & (a) \arrow{u}[swap]{η(a)} & \mbox{} \\ +\end{tikzcd} + + + +なら、 $ FU(ε(F(a))) = εF(a) $ ? + +--begin-comment: + U + UFU(F(a)) <--------------- FU(F(a)) + ^| | + η(U(a))||U(ε(F(a))) |ε(F(a)) + |v v + U(F(a)) <---------------- F(a) + U + + FU + FUFU(F(a)) <--------------- FU(F(a)) + ^| | + Fη(U(a))||FU(ε(F(a))) |ε(F(a)) + |v v + FU(F(a)) <---------------- F(a) + FU + + F + FUF(a) <--------------- UF(a) + ^| ^ + Fη(a)||εF(a) |η(a) + |v | + F(a) <---------------- (a) + F +--end-comment: + +\begin{tikzcd} +UFU(F(a)) \arrow[leftarrow]{r}{U} \arrow[bend left]{d}{U(ε(F(a)))} & FU(F(a)) \arrow{d}{ε(F(a))} & \mbox{} \\ +U(F(a)) \arrow[leftarrow]{r}[swap]{U} \arrow[bend left]{u}{η(U(a))} & F(a) & \mbox{} \\ +FUFU(F(a)) \arrow[leftarrow]{r}{FU} \arrow[bend left]{d}{FU(ε(F(a)))} & FU(F(a)) \arrow{d}{ε(F(a))} & \mbox{} \\ +FU(F(a)) \arrow[leftarrow]{r}[swap]{FU} \arrow[bend left]{u}{Fη(U(a))} & F(a) & \mbox{} \\ +FUF(a) \arrow[leftarrow]{r}{F} \arrow[bend left]{d}{εF(a)} & UF(a) & \mbox{} \\ +F(a) \arrow[leftarrow]{r}[swap]{F} \arrow[bend left]{u}{Fη(a)} & (a) \arrow{u}[swap]{η(a)} & \mbox{} \\ +\end{tikzcd} + +--Monad + +$(T,η,μ)$ + +$ T: A -> A $ + +$ η: 1_A -> T $ + +$ μ: T^2 -> T $ + +$ μ○Tη = 1_T = μ○ηT $ Unity law + +$ μ○μT = μ○Tμ $ association law + +--begin-comment: + Tη μT + T ---------> T^2 T^3---------> T^2 + |・ | | | + | ・1_T | | | + ηT| ・ |μ Tμ| |μ + | ・ | | | + v ・ v v v + T^2 -------> T T^2 --------> T + μ μ +--end-comment: + +\begin{tikzcd} +T \arrow{r}{Tη} \arrow{d}[swap]{ηT} \arrow{rd}{1_T} & T^2 \arrow{d}{μ} & T^3 \arrow{r}{μT} \arrow{d}[swap]{Tμ}& T^2 \arrow{d}{μ} & \mbox{} \\ +T^2 \arrow{r}[swap]{μ} & T & T^2 \arrow{r}[swap]{μ} & T & \mbox{} \\ +\end{tikzcd} + + +--Adjoint to Monad + +Monad (UF, η, UεF) on adjoint (U,F, η, ε) + +\begin{eqnarray*} +εF○Fμ & = & 1_F \\ +Uε○μU & = & 1_U \\ +\end{eqnarray*} + +\begin{eqnarray*} +μ○Tη & = & (UεF)○(UFη) = U (εF○Fη) = U 1_F = 1_{UF} \\ +μ○ηT & = & (UεF)○(ηUF) = (Uε○ηU) F = 1_U F = 1_{UF} \\ +\end{eqnarray*} + +\begin{eqnarray*} +(UεF)○(ηUF) & = & (U(ε(F(b))))(UF(η(b))) \\ +& = & U(ε(F(b))F(η(b))) = U(1_F) \\ +\end{eqnarray*} + +--begin-comment: + + UεFUF εFUF ε(a) + UFUFUF-------> UFUF FUFUF-------> FUF FU(a)---------->a + | | | | | | + | | | | | | + UFUεF| |UεF FUεF| |εF FU(f)| |f + | | | | | | + v v v v v v + UFUF --------> UF FUF --------> F FU(b)---------> b + UεF εF ε(b) + +--end-comment: + +\begin{tikzcd} +UFUFUF \arrow{r}{UεFUF} \arrow{d}[swap]{UFUεF} & UFUF \arrow{d}{UεF} & FUFUF \arrow{r}{εFUF} \arrow{d}[swap]{FUεF} & FUF \arrow{d}{εF} & FU(a) \arrow{r}{ε(a)} \arrow{d}[swap]{FU(f)} & a \arrow{d}[swap]{f} & \mbox{} \\ +UFUF \arrow{r}{UεF} & UF & FUF \arrow{r}[swap]{εF} & F & FU(b) \arrow{r}[swap]{ε(b)} & b & \mbox{} \\ +\end{tikzcd} + +association law + +\begin{eqnarray*} +μ ○ μ T & = & μ ○ T μ \\ +Uε(a)F ○ Uε(a)F FU & = & Uε(a)F ○ FU Uε(a)F \\ +\end{eqnarray*} + +$UεF○UεFFU=UεF○FUUεF$ + +naturality of $ε$ + +$ ε(b)FU(f)(a) = fε(a) $ + +$ a = FUF(a), b = F(a), f = εF $ + +\begin{eqnarray*} +ε(F(a))(FU(εF))(a) & = & (εF)(εFUF(a)) \\ +U(ε(F(a))(FU(εF))(a)) & = & U((εF)(εFUF(a))) \\ +U(ε(F(a))(FU(εF))(a)) & = & U((εF)(εFUF(a))) \\ +UεF○FUUεF & = UεF○UεFFU \\ +\end{eqnarray*} + +--begin-comment: + + FU(ε(F(a))) + FUF(a) <-------------FUFUF(a) + | | + |ε(F(a)) |ε(FUF(a)) + | | + v v + F(a) <------------- FUF(a) + ε(F(a)) + +--end-comment: + +\begin{tikzcd} +FUF(a) \arrow[leftarrow]{r}{FU(ε(F(a)))} \arrow{d}{ε(F(a))} & FUFUF(a) \arrow{d}{ε(FUF(a))} & \mbox{} \\ +F(a) \arrow[leftarrow]{r}[swap]{ε(F(a))} & FUF(a) & \mbox{} \\ +\end{tikzcd} + +--Eilenberg-Moore category + +$(T,η,μ)$ + +$A^T$ object $(A,φ)$ + +$ φη(A) = 1_A, φμ(A) = φT(φ) $ + +arrow $f$. + +$ φT(f) = fφ $ + + +--begin-comment: + + η(a) μ(a) T(f) + a-----------> T(a) T^2(a)--------> T(a) T(a)---------->T(b) + | | | | | + | | | | | + |φ T(φ)| |φ φ| |φ' + | | | | | + v v v v v + _ a T(a)-------->T(a) a------------> b + φ f + +--end-comment: + +\begin{tikzcd} +a \arrow{r}{η(a)} \arrow{rd}{1_a} & T(a) \arrow{d}{φ} & T^2(a) \arrow{r}{μ(a)} \arrow{d}[swap]{T(φ)} & T(a) \arrow{d}{φ} & T(a) \arrow{r}{T(f)} \arrow{d}[swap]{φ} & T(b) \arrow{d}{φ'} & \mbox{} \\ +\mbox{} & a & T(a) \arrow{r}[swap]{φ} & T(a) & a \arrow{r}[swap]{f} & b & \mbox{} \\ +\end{tikzcd} + +--EM on monoid + +$f: a-> b$ + +$T: a -> (m,a) $ + +$η: a -> (1,a) $ + +$μ: (m,(m',a)) -> (mm',a) $ + +$φ: (m,a) -> φ(m,a) = ma $ + +--begin-comment: + + η(a) μ(a) T(f) + a----------->(1,a) (m,(m',a))-----> (mm',a) (m,a)----------->(m,f(a)) + | | | | | + | | | | | + |φ T(φ)| |φ φ| |φ' + | | | | | + v v v v v + _ 1a (m,m'a)-------->mm'a ma------------> mf(a)=f(ma) + φ f +--end-comment: + +\begin{tikzcd} +a \arrow{r}{η(a)} \arrow{rd}{1_a} & (1,a) \arrow{d}{φ} & (m,(m',a)) \arrow{r}{μ(a)} \arrow{d}[swap]{T(φ)} & (mm',a) \arrow{d}{φ} & (m,a) \arrow{r}{T(f)} \arrow{d}[swap]{φ} & (m,f(a)) \arrow{d}{φ'} & \mbox{} \\ +\mbox{} & 1a & (m,m'a) \arrow{r}[swap]{φ} & mm'a & ma \arrow{r}[swap]{f} & mf(a)=f(ma) & \mbox{} \\ +\end{tikzcd} + +object $(a,φ)$. arrow $f$. + +$ φT(f)(m,a) = fφ(m,a) $ + +$ φ(m,f(a)) = f(a) $ + +$ U^T : A^T->A $ + +$ U^T(a,φ) = a, U^T(f) = f $ + +$ F^T : A->A^T$ + +$ F^T(a) = (T(a),μ(a)), F^T(f) = T(F) $ + +--Comparison Functor $K^T$ + +$ K^T(B) = (U(B),Uε(B))a, K^T(f) = U(g) $ + +$ U^T K^T (b) = U(b) $ + +$ U^TK^T(f) = U^TU(f) = U(f) $ + +$ K^TF(a) = (UF(a),Uε(F(a))) = (T(a), μ(a)) = F^T(a) $ + +$ K^TF(f) = UF(f) = T(f) = F^T(f) $ + +$ ηU(a,φ) = η(a), Uε(a,φ) = ε^TK^T(b) = Uε(b) $ + +--begin-comment: + + + _ Ba _ + |^ + || + || + K_T F||U K^T + || + || + || + U_T v| F^T + A_T---------> A ---------> A^T + <--------- <-------- + F_T U^T + +--end-comment: + + +\begin{tikzcd} +\mbox{} & B \arrow{r}{K^T} \arrow{rd}{F} \arrow[leftarrow]{rd}[swap]{U} & A^T \arrow{d}{U^T} & \mbox{} \\ +\mbox{} & A_T \arrow{r}[swap]{U_T} \arrow[leftarrow]{r}{F_T} \arrow{u}[swap]{K_T} & A \arrow{u}{F^T} & \mbox{} \\ +\\ +\mbox{} & B \arrow{d}{F} \arrow{rd}{K^T} & \mbox{} \\ +A_T \arrow{r}{U_T} \arrow{ru}[leftarrow]{K_T} & A \arrow{r}{F^T} \arrow{u}{U} & A^T & \mbox{} \\ +\end{tikzcd} + +--Kleisli Category + +Object of $A$. + +Arrow $f: T -> T(A)$. In $f: b -> c, g: c -> d$, + +$ g * f = μ(d)T(g)f $ + +$η(b):b->T(b)$ is an identity. + +$ f * η(b) = μ(c)T(f)η(b) = μ(c)η(T(c))f = 1_T(c) f = f $ + +and + +$ η(c) * f = μ(c)Tη(c)f = 1_T(c) f = f $ + +association law $ g * (f * h) = (g * f) * h $, + +$h: a -> T(b), f: b -> T(c), g: c -> T(d) $, + +naturality of $μ$ + +--begin-comment: + + μ(c) T(f) h +f*h _ _ T(c) <---------------- T^2(c) <------- T(b) <----------- a + + + μ(d) T(g) μ(c) T(f) h +g*(f*h) T(d)<--------T^2(d) <-------------- T(c) <---------------- T^2(c) <------- T(b) <----------- a + + + μ(d) μ(d)T T^2(g) T(f) h +(g*f)*h T(d)<--------T^2(d) <---------------T^3(d) <-------------- T^2(c) <------- T(b) <----------- a + + + μ(d) Tμ(d) T^2(g) T(f) h +(g*f)*h T(d)<--------T^2(d) <---------------T^3(d) <-------------- T^2(c) <------- T(b) <----------- a + + + μ(d) T(g) f +(g*f) _ T(d) <---------------T^2(d) <-------------- T(c) <----------- b _ + + + + + Tμ(d) T^2(g) + T^2(d)<-----------T^2(T(d))<-------- T^2(c) + | | | + | | | + μ(d)| |μ(T(d)) |μ(c) + | | | + v μ(d) v T(g) v + T(d) <----------- T(T(d)) <---------- T(c) + + + +--end-comment: + +\begin{tikzcd} +f*h & \mbox{} & \mbox{} & T(c) \arrow[leftarrow]{r}{μ(c)} & T^2(c) \arrow[leftarrow]{r}{T(f)} & T(b) \arrow[leftarrow]{r}{h} & a & \mbox{} \\ +g*(f*h) & T(d) \arrow[leftarrow]{r}{μ(d)} & T^2(d) \arrow[leftarrow]{r}{T(g)} & T(c) \arrow[leftarrow]{r}{μ(c)} & T^2(c) \arrow[leftarrow]{r}{T(f)} & T(b) \arrow[leftarrow]{r}{h} & a & \mbox{} \\ +(g*f)*h & T(d) \arrow[leftarrow]{r}{μ(d)} & T^2(d) \arrow[leftarrow]{r}{μ(d)T} & T^3(d) \arrow[leftarrow]{r}{T^2(g)} & T^2(c) \arrow[leftarrow]{r}{T(f)} & T(b) \arrow[leftarrow]{r}{h} & a & \mbox{} \\ +(g*f)*h & T(d) \arrow[leftarrow]{r}{μ(d)} & T^2(d) \arrow[leftarrow]{r}{Tμ(d)} & T^3(d) \arrow[leftarrow]{r}{T^2(g)} & T^2(c) \arrow[leftarrow]{r}{T(f)} & T(b) \arrow[leftarrow]{r}{h} & a & \mbox{} \\ +g*f & T(d) \arrow[leftarrow]{r}{μ(d)} & T^2(d) \arrow[leftarrow]{r}{T(g)} & T(c) \arrow[leftarrow]{r}{f} & b & \mbox{} \\ +\mbox{} & T^2(d) \arrow[leftarrow]{r}{Tμ(d)} \arrow{d}[swap]{μ(d)} & T^2(T(d)) \arrow[leftarrow]{r}{T^2(g)} \arrow{d}{μ(T(d))} & T^2(c) \arrow{d}{μ(c)}& \mbox{} \\ +\mbox{} & T(d) \arrow[leftarrow]{r}{μ(d)} & T(T(d)) \arrow[leftarrow]{r}{T(g)} & T(c) & \mbox{} \\ +\end{tikzcd} + + +\begin{eqnarray*} +g * (f * h) & = & g * (μ(c)T(f)h) \\ +\mbox{} & = & μ(d)(T(g))(μ(c)T(f)h) \\ +\mbox{} & = & μ(d) T(g)μ(c) T(f)h \\ +\\ +(g * f) * h & = & (μ(d)T(g)f) * h \\ +\mbox{} & = & μ(d)T(μ(d)T(g)f)h \\ +\mbox{} & = & μ(d) T(μ(d))T^2(g) T(f)h \\ +\end{eqnarray*} + +$ μ(d)μ(d)T = μ(d)Tμ(d) $ + +$ μ(T(d))T^2(g) = T(g)μ(c) $ naturality of $μ$. + +$ μ(d)Tμ(d)T^2(g) = μ(d)μ(T(d))T^2(g) = μ(d)T(g)μ(c) $ + +--begin-comment: + + T^2(g) + T^3(d) <----------- T^2(c) + | | + |μ(T(d)) |μ(c) + | | + v v + T^2(d)<------------ T(c) + T(g) + +--end-comment: + +\begin{tikzcd} +T^3(d) \arrow[leftarrow]{r}{T^2(g)} \arrow{d}{μ(T(d))} & T^2(c) & \mbox{} \\ +T^2(d) \arrow[leftarrow]{r}[swap]{T(g)} & T(c) \arrow{u}{μ(c)} & \mbox{} \\ +\end{tikzcd} + +$ μ(T(d)) = Tμ(d) ? $ + +$ (m,(m'm'',a)) = (mm',(m'',a))$ No, but + +$ μμ(T(d)) = μTμ(d) $. + + +--Ok + +$ T(g)μ(c) = T(μ(d))T^2(g) $ であれば良いが。 + +$ μ(d)T^2(g) = T(g)μ(c) $ + +ちょっと違う。 $ μ(d) T(μ(d))T^2(g) $ が、 + +$ μ(d) μ(d)T^2(g) $ + +となると良いが。 + +$ μ(d)T(μ(d)) = μ(d)μ(T(d)) $ + + +--monoid in Kleisli category + +$ T : a -> (m,a) $ + +$ T : f -> ((m,a)->(m,f(a))) $ + +$ μ(a) : (m,(m',a)) -> (mm',a) $ + +$ f: a -> (m,f(a)) $ + +\begin{eqnarray*} +g * f (b) & = & μ(T(g))f(b) = μ(T(g))(m,f(b)) \\ & = & μ(m,(m',gf(b))) = (mm',gf(b)) \\ +(g * f) * h(a) & = & μT(μ(T(g)f))h(a) = μT(μ)(TT(g))T(f)(m,h(a)) \\ +\mbox{} & = & μT(μ)(TT(g))(m,(m',fh(a))) \\ & = & μT(μ)(m,(m',(m'',gfh(a)))) = (mm'm'',gfh(a)) \\ +g * (f * h)(a) & = & (μ(T(g)))μT(f)h(a) = (μ(T(g)))μT(f)(m,h(a)) \\ +\mbox{} & = & (μ(T(g)))μ(m,(m',fh(a)) \\ & = & μ(T(g))(mm',fh(a)) = (mm'm'',gfh(a)) \\ +\end{eqnarray*} + + +--Resolution of Kleiseli category + +$f : a-> b, g: b->c $ + +$ U_T : A_T -> A $ + +$ U_T(a) = T(a) $ + +$ U_T(f) = μ(b)T(f) $ + +$ g * f = μ(d)T(g)f $ + +\begin{eqnarray*} +U_T(g*f) & = & U_T(μ(c)T(g)f) \\ & = & μ(c) T(μ(c)T(g)f) \\ & = & μ(c) μ(c)T(T(g)f)) = μ(c)μ(c) TT(g) T(f) \mbox{ association law} \\ +U_T(g)U_T(f) & = & μ(c)T(g)μ(b)T(f) = μ(c) μ(c) TT(g) T(f) \\ +T(g)μ(b) & = & μ(c)TT(g) \\ +\end{eqnarray*} + + + +--begin-comment: + + TT(g) + TT <--------------TT + | | + |μ(c) |μ(b) + | | + v T(g) v + T<---------------T + +--end-comment: + +\begin{tikzcd} +TT \arrow[leftarrow]{r}{TT(g)} \arrow{d}{μ(c)} & TT \arrow{d}{μ(b)} & \mbox{} \\ +T \arrow[leftarrow]{r}{T(g)} & T & \mbox{} \\ +\end{tikzcd} + + +$ F_T : A -> A_T $ + +$ F_T(a) = a $ + +$ F_T(f) = η(b) f $ + +$ F_T(1_a) = η(a) = 1_{F_T(a)} $ + +\begin{eqnarray*} +F_T(g)*F_T(f) & = & μ(c)T(F_T(g))F_T(f) \\& = & μ(c)T(η(c)g)η(b)f \\ & = & μ(c)T(η(c))T(g)η(b)f \\& = & T(g)η(b) f \mbox{ unity law} \\ +\mbox{} & = & η(c)gf = F_T(gf) +\end{eqnarray*} + +$ η(c)g = T(g)η(b) $ + +--begin-comment: + + g + c<---------------b + | | + |η(c) |η(b) + | | + v T(g) v + T(b)<-------------T(b) + +--end-comment: + +\begin{tikzcd} +c \arrow[leftarrow]{r}{g} \arrow{d}{η(c)} & b \arrow{d}{η(b)} & \mbox{} \\ +T \arrow[leftarrow]{r}{T(g)} & T & \mbox{} \\ +\end{tikzcd} + + +$ μ○Tη = 1_T = μ○ηT $ Unity law + +\begin{eqnarray*} +\mbox{} ε_T(a) & = & 1_{T(a)} \\ +\mbox{}\\ +\mbox{}\\ +\mbox{} U_T ε_T F_T & = & μ \\ +\mbox{}\\ +\mbox{} U_T ε_T F_Ta(a) & = & U_T ε_T (a) = U_T(1_{T(a)} = μ(a) \\ +\mbox{}\\ +\mbox{} ε_T(F_T(a))*F_T(η(a)) & = & ε_T(a) * F_T(η(a)) \\ & = & 1_{T(a)} * (F_T(η(a))) \\ & = & 1_{T(a)} * (η(T(a))η(a))) \\ +\mbox{} & = & μ(T(a)) T (1_{T(a)} ) (η(T(a))η(a))) \\ & = & μ(T(a))η(T(a))η(a) \\ +\mbox{} & = & η(a) = 1_{F_T} \\ +\end{eqnarray*} + + + +\begin{eqnarray*} +U_T(ε_T(a))η(U_T(a)) & = & U_T(1_{T(a)} η( T(a)) ) \\ & = & μ(T(a))T(1_{T(a)}) η(T(a)) \\ & = & μ(T(a)) η(T(a)) 1_{T(a)} \\ +& = & 1_{T(a)} = T(1_a) = 1_{U_T} \\ +\end{eqnarray*} + + + +---Comparison functor $K_T$ + +Adjoint $(B,U,F,ε)$, $K_T : A_T -> B $, + +$ g : b -> c$. + + +\begin{eqnarray*} +K_T(a) & = & F(a) \\ +K_T(g) & = & ε(F(c)) F(g) \\ +K_T F_T(a) & = & K_T(a) = F(a) \\ +K_T F_T(f) & = & K_T(η(b) f) \\& = & ε(F(b))F(μ(b)f) \\ & = & ε(F(b))F(μ(b))F(f) = F(f) \\ +\end{eqnarray*} + + +\begin{eqnarray*} +K_T (η(b)) & = & ε(F(b))F(η(b)) = 1_{F(b)} \\ +K_T (η(T(c))g) & = & ε(F(T(c)))F(η(T(c))g) = F(g) \\ +K_T (g) K_T(f) & = & ε(F(c))F(g) ε(F(b))F(f) = ε(F(c)) ε(F(c)) FUF(g) F(f) \\ +K_T (g*f) & = & ε(F(c)) F(μ(c)UF(g)f) = ε(F(c)) F(μ(c)) FUF(g) F(f) \\ +ε(F(c))FUF(g) & = & F(g) ε(F(b)) \\ +\end{eqnarray*} + +--begin-comment: + + FU(F(g)) + FU(F(c))<-------------FU(F(b)) + | | + |ε(F(c)) |ε(F(b)) + | | + v F(g) v + F(c)<----------------F(b) + +--end-comment: + +\begin{tikzcd} +FU(F(c)) \arrow[leftarrow]{r}{FU(F(g))} \arrow{d}{ε(F(c))} & FU(F(b)) \arrow{d}{ε(F(b))} & \mbox{} \\ +F(c) \arrow[leftarrow]{r}{F(g)} & F(b) & \mbox{} \\ +\end{tikzcd} + +$ ε(F(c)) F(μ(c)) = ε(F(c)) ε(F(c)) $ ? + +$ ε(F(c)) F(μ(c)) = ε(F(c)) FUε(F(c)) $ + +--begin-comment: + + FUε(F(c)) + FUFU(c)<---------------FUFU(F(c)) + | | + |εF(c)) |ε(F(c)) + | | + v ε(F(c)) v + FU(c)<----------------FU(F(c)) + + +--end-comment: + +\begin{tikzcd} +FUFU(c) \arrow[leftarrow]{r}{FUε(F(c))} \arrow{d}{εF(c))} & FUFU(F(c)) \arrow{d}{ε(F(c))} & \mbox{} \\ +FU(c) \arrow[leftarrow]{r}{ε(F(c))} & FU(F(c)) & \mbox{} \\ +\end{tikzcd} + + + +$ UK_T(a) = UF(a) = T(a) = U_T(a) $ + +$ UK_T(g) = U(ε((F(c))F(g))) = U(ε(F(c)))UF(g) = μ(c)T(g) = U_T(g) $ + + + + + + +--Monoid + + +$T : A -> M x A$ + +$T(a) = (m,a)$ + +$T(f) : T(A) -> T(f(A))$ + +$T(f)(m,a) = (m,f(a))$ + +$T(fg)(m,a) = (m,fg(a)) $ + +-- association of Functor + +$T(f)T(g)(m,a) = T(f)(m,g(a)) = (m,fg(a)) = T(fg)(m,a)$ + + +$μ : T x T -> T$ + +$μ_a(T(T(a)) = μ_A((m,(m',a))) = (m*m',a) $ + +-- $TT$ + +$TT(a) = (m,(m',a))$ + +$TT(f)(m,(m',a)) = (m,(m',f(a))$ + + + +-- naturality of $μ$ + +--begin-comment: + μ_a + TT(a) ---------> T(a) + | | + TT(f)| |T(f) + | | + v μ_b v + TT(b) ---------> T(b) +--end-comment: + +\begin{tikzcd} +TT(a) \arrow{r}{μ_a} \arrow{d}{TT(f)} & T(a) \arrow{d}{T(f)} \\ +TT(b) \arrow{r}{μ_b} & T(b) +\end{tikzcd} + + +$ μ_bTT(f)TT(a) = T(f)μ_aTT(a)$ + +$ μ_bTT(f)TT(a) = μ_b((m,(m',f(a))) = (m*m',f(a))$ + +$ T(f)μ_a(TT(a)) = T(f)(m*m',a) = (m*m',f(a))$ + +--μ○μ + +Horizontal composition of $μ$ + +$f -> μ_TT(a)$ + +$a -> TT(a)$ + +$μ_T(a) TTT(a) = μ_T(a) (m,(m',(m'',a))) = (m*m',(m'',a)) $ + +--begin-comment: + μ_a + TTTT(a) ---------> TTT(a) + | | + TT(μ)| |T(μ) + | | + v μ_b v + TTT(a) ---------> TT(a) +--end-comment: + + +\begin{tikzcd} +TTTT(a) \arrow{r}{μ_a} \arrow{d}{TT(μ)} & TTT(a) \arrow{d}{T(μ)} \\ +TTT(a) \arrow{r}{μ_b} & TT(a) +\end{tikzcd} + + +\begin{eqnarray*} +T(μ_a)μ_aTTTT(a) & = & T(μ_a)μ_a(m_0,(m_1,(m_2,(m_3,a))))) \\& = & T(μ_a)(m_0*m_1,(m_2,(m_3,a))) = (m_0*m_1,(m_2*m_3,a)) \\ +μ_bTT(μ_a)TTTT(a) & = & μ_bTT(μ_a)(m_0,(m_1,(m_2,(m_3,a))))) \\& = & μ_b (m_0,(m_1,(m_2*m_3,a))) = (m_0*m_1,(m_2*m_3,a)) \\ +\end{eqnarray*} + +-Horizontal composition of natural transformation + + +--Natural transformation $ε$ and Functor $F: A->B, U:B->A$ + + +$ ε: FUFU->FU$ + +$ ε: FU->1_B$ + +Naturality of $ε$ + +--begin-comment: + ε(a) + FU(a) ------> a + FU(f)| |f + v ε(b) v + FU(b) ------> b ε(b)FU(f)a = fε(a)a + + ε(FU(a)) + FUFU(a) -----------> FU(a) + FUFU(f)| |FU(f) + v ε(FU(b)) v + FUFU(b) -----------> FU(b) + + ε((FU(b))FUFU(f)FU(a) = FU(f)ε(FU(a))FU(a) +--end-comment: + +\begin{tikzcd} +FU(a) \arrow{r}{ε(a)} \arrow{d}{FU(f)} & a \arrow{d}{f} \\ +FU(b) \arrow{r}{ε(b)} & b & ε(b)FU(f)a = fε(a)a \\ +FUFU(a) \arrow{r}{ε(FU(a))} \arrow{d}{FUFU(f)}& FU(a) \arrow{d}{FU(f)} \\ +FUFU(b) \arrow{r}{ε(FU(b))} & FU(b) \\ +& & ε((FU(b))FUFU(f)FU(a) = FU(f)ε(FU(a))FU(a) \\ +\end{tikzcd} + + +--Vertial Compositon $ε・ε$ + +$ ε・ε : FUFU -> 1B$ + +--begin-comment: + ε(FU(a)) ε(a) + FUFU(a) ---------> FU(a) ------> a + FUFU(f)| |FU(f) |f + v ε(FU(b)) v ε(b) v + FUFU(b) ---------> FU(b) ------> b +--end-comment: + +\begin{tikzcd} +FUFU(a) \arrow{r}{ε(FU(a))} \arrow{d}{FUFU(f)} & FU(a) \arrow{r}{ε(a)}\arrow{d}{FU(f)} & a\arrow{d}{f} \\ +FUFU(b) \arrow{r}{ε(FU(b))} & FU(b) \arrow{r}{ε(b)} & b +\end{tikzcd} + + +--Horizontal Composition $ε○ε$ + +--begin-comment: + FUFU <----- FU <------ B + FU FU + | | + |ε |ε + v v + 1_B 1_B + B <----- B <------ B +--end-comment: + +\begin{tikzcd} +FUFU \arrow[leftarrow]{rr} & & FU \arrow[leftarrow]{rr} & & B \\ +& FU \arrow{d}{ε} & & FU \arrow{d}{ε}& & \\ +& 1_B & & 1_B & & \\ +B \arrow[leftarrow]{rr} & & B \arrow[leftarrow]{rr} & & B \\ +\end{tikzcd} + +cf. $FUFU, FU$ has objects of $B$. + +$ ε○ε : FUFU -> 1_B 1_B$ + +--begin-comment: + εFU(b) + FUFU(b) ------------> 1_AFU(b) + | | + |FUε(b) |1_aε(b) + | | + v ε(b) v + FU1_B(b) ------------> 1_B1_B(b) + +--end-comment: + +\begin{tikzcd} +FUFU(b) \arrow{r}{εFU(b)} \arrow{d}{FUε(b)} & 1_A \arrow{d}{1_aε(b)} & \mbox{} \\ +FU1_B(b) \arrow{r}{ε(b)} & 1_B & \mbox{} \\ +\end{tikzcd} + +that is + +--begin-comment: + εFU(b) + FUFU(b) ------------> FU(b) + | | + |FUε(b) |ε(b) + | | + v ε(b) v + FU(b) ------------> b +--end-comment: + +\begin{tikzcd} +FUFU(b) \arrow{r}{εFU(b)} \arrow{d}{FUε(b)} & FU(b) \arrow{d}{ε(b)} & \mbox{} \\ +FU(b) \arrow{r}{ε(b)} & b & \mbox{} \\ +\end{tikzcd} + + +$ε(b) : b -> ε(b)$ arrow of $B$ + +$ ε: FU -> 1_B$ + +$ ε(b) : FU(b) -> b$ + +--begin-comment: + U F ε(b) + b ----> U(b) ----> FU(b) -------> b +--end-comment: + +\begin{tikzcd} +b \arrow{r}{U} & U(b) \arrow{r}{F} & FU(b) \arrow{r}{ε(b)} & b & \mbox{} \\ +\end{tikzcd} + +replace $f$ by $ε(b)$, $a$ by $FU(b)$ in naturality $ε(b)FU(f)a = fε(a)a$ + +$ ε(b)FU(ε(b))FU(b) = εε(FU(b))FU(b)$ + +remove $FU(b)$ on right, + +$ ε(b)FU(ε(b)) = ε(b)ε(FU(b))$ + +this shows commutativity of previous diagram + +$ ε(b)ε(FU(b)) = ε(b)FU(ε(b))$ + +that is + +$ εεFU = εFUε$ + + + +--Yoneda Functor + + +$ Y: A -> Sets^{A^{op}} $ + +$ Hom_A : A^{op} \times A -> Sets $ + +$ g:a'->a, h:b->b' $ + +$ Hom_A((g,h)) : Home_A(a,b) -> \{hfg | f \in Home_A(a,b) \} $ + +$ Hom_A((g,h)○(g',h') : Home_A(a,b) -> \{hh'fgg' | f \in Home_A(a,b) \} $ + +$ Hom_A((g,h)) Hom_A((g',h')) : Home_A(a,b) -> \{h'fg' | f \in Home_A(a,b) \} -> \{hh'fgg' | f \in Home_A(a,b) \} $ + +--begin-comment: + + g' g + a -----> a' -----> a'' + | | + | |f + h' v h v + b<-------b' <----- b'' + +--end-comment: + +\begin{tikzcd} +a \arrow{r}{g'} & a' \arrow{r}{g} \arrow{d}{} & a'' \arrow{d}{f} & \mbox{} \\ +b \arrow[leftarrow]{r}{h'} & b' \arrow[leftarrow]{r}{h} & b'' & \mbox{} \\ +\end{tikzcd} + +$ Hom^*_A : A^{op} -> Sets^{A} $ + +$ f^{op}: a->c ( f : c->a ) $ + +$ g^{op}: c->d ( g : d->c ) $ + +$ Home^*_A(a) : a -> λ b . Hom_A(a,b) $ + +$ Home^*_A(f^{op}) : (a -> λ b . Hom_A(a,b)) -> (c -> λ b . Hom_A(f(c),b)) $ + +$ Home^*_A(g^{op}f^{op}) : (a -> λ b . Hom_A(a,b)) -> (d -> λ b . Hom_A(fg(d),b)) $ + +$ Home^*_A(g^{op}) Home^*_A(f^{op}) : (a -> λ b . Hom_A(a,b)) -> (c -> λ b . Hom_A(f(c),b)) -> (d -> λ b . Hom_A(fg(d),b)) $ + + +$ Hom^*_{A^{op}} : A -> Sets^{A^{op}} $ + +$ f : c->b $ +$ g : d->c $ + +$ Home^*_{A^{op}}(b) : b -> λ a . Hom_{A^{op}}(a,b) $ + +$ Home^*_{A^{op}}(f) : (b -> λ a . Hom_{A^{op}}(a,b)) -> (c -> λ a . Hom_{A^{op}}(a,f(c))) $ + +$ Home^*_{A^{op}}(gf) : (b -> λ a . Hom_{A^{op}}(a,b)) -> (d -> λ a . Hom_{A^{op}}(a,gf(d))) $ + +$ Home^*_{A^{op}}(g) Home^*_{A^{op}}(f) : (b -> λ a . Hom_{A^{op}}(a,b)) -> (c -> λ a . Hom_{A^{op}}(a,f(c))) -> (d -> λ a . Hom_{A^{op}}(a,gf(d))) $ + + +Arrows in $ Set^{A^{op}} $? + +$ f: b->c = (b -> λ a . Hom_{A^{op}}(a,b)) -> (c -> λ a . Hom_{A^{op}}(a,f(c))) $ + +$ Set^{A^{op}} : A^{op} -> Set $ + +an object $ b = λ a . Hom_{A^{op}}(a,b) $ is a functor from $A^{op}$ to $ Set $. + +$ t: (λ a . Hom_{A^{op}}(a,b)) -> (λ a . Hom_{A^{op}}(a,t(c))) $ should be a natural transformatin. + +$ f^{op}: (b : A^{op}) -> (c : A^{op} ) = f : c->b $ + + +--begin-comment: + + t(c) +Hom_{A^{op}}(a,c) ------------------------->Hom_{A^{op}}(a,t(c)) + | ^ + | | + |Home^*{A^{op}}(a,f) |Home^*{A^{op}}(a,f) + | | + v t(b) | +Hom_{A^{op}}(a,b) ------------------------->Hom_{A^{op}}(a,t(b)) + + + +--end-comment: + +\begin{tikzcd} +Hom_{A^{op}}(a,c) \arrow{r}{t(c)} \arrow{d}{Home^*{A^{op}}(a,f)} & Hom_{A^{op}}(a,t(c)) & \mbox{} \\ +Hom_{A^{op}}(a,b) \arrow{r}{t(b)} & Hom_{A^{op}}(a,t(b)) \arrow{u}[swap]{Home^*{A^{op}}(a,f)} & \mbox{} \\ +\end{tikzcd} + + +---Contravariant functor + +$ h_a = Hom_A(-,a) $ + +$ f:b->c, Hom_A(f,1_a): Hom_A(c,a) -> Hom_A(b,a) $ + + + + + + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/list.agda Sat Jul 06 00:34:08 2013 +0900 @@ -0,0 +1,13 @@ +module list where + +open import Data.List + + +postulate a : Set +postulate b : Set +postulate c : Set + +l1 = [ a ] + +l2 = ( a :: [] ) +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/nat.agda Sat Jul 06 00:34:08 2013 +0900 @@ -0,0 +1,94 @@ + + +module nat where + + +-- Monad +-- Category A + +-- A = Category + +-- Functor T : A -> A + + + +--T(a) = t(a) +--T(f) = tf(f) + +--T(g f) = T(g) T(f) + +open import Category +open import Level +open Functor + +Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) -> {a b c : Obj A} {g : Hom A b c} { f : Hom A a b } + -> A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] +Lemma1 = \t -> IsFunctor.distr ( isFunctor t ) + + + + +-- F(f) +-- F(a) ----> F(b) +-- | | +-- |t(a) |t(b) G(f)t(a) = t(b)F(f) +-- | | +-- v v +-- G(a) ----> G(b) +-- G(f) + +record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) + ( F G : Functor D C ) + (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A)) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + field + naturality : {a b : Obj D} {f : Hom D a b} + → C [ C [ ( FMap G f ) o ( Trans a ) ] ≈ C [ (Trans b ) o (FMap F f) ] ] +-- how to write uniquness? +-- uniqness : {d : Obj D} +-- → ∃{e : Trans d} -> ∀{a : Trans d} → C [ e ≈ a ] + + +record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + field + Trans : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) + isNTrans : IsNTrans domain codomain F G Trans + +open NTrans +Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} -> (μ : NTrans A A F G) -> {a b : Obj A} { f : Hom A a b } + -> A [ A [ FMap G f o Trans μ a ] ≈ A [ Trans μ b o FMap F f ] ] +Lemma2 = \n -> IsNTrans.naturality ( isNTrans n ) + +open import Category.Cat + +record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + ( T : Functor A A ) + ( η : NTrans A A (identityFunctor) T ) + ( μ : NTrans A A T (T ○ T)) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + unity1 : {a b : Obj A} + → A [ A [ ( Trans μ a ) o ( Trans η a) ] ≈ Id A a ] + +-- η : 1_A -> T +-- μ : TT -> T +-- μ(a)η(T(a)) = a +-- μ(a)T(η(a)) = a +-- μ(a)(μ(T(a))) = μ(a)T(μ(a)) + + + + + +-- nat of η + + +-- g ○ f = μ(c) T(g) f + +-- h ○ (g ○ f) = (h ○ g) ○ f + +-- η(b) ○ f = f +-- f ○ η(a) = f + +