Mercurial > hg > Members > kono > Proof > category
changeset 463:4c686e19db60
document clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 04 Mar 2017 11:05:40 +0900 |
| parents | e618db534987 |
| children | 037af9cf038c |
| files | category.ind doc/category.ind doc/fig/Kli-orig.svg doc/fig/Kli.graffle doc/fig/Kli.svg doc/fig/Monad.svg doc/test.tex doc/test2.tex |
| diffstat | 8 files changed, 3412 insertions(+), 1602 deletions(-) [+] |
line wrap: on
line diff
--- a/category.ind Sat Mar 04 10:54:26 2017 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1602 +0,0 @@ --title: Cateogry - ---author: Shinji KONO <kono@ie.u-ryukyu.ac.jp> - -\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: a -> T(a)$ in $A$. In $A_T$, $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) & = & μ(d)T(g)f(b) = μ(d)T(g)(m,f(b)) \\ & = & μ(m,(m',gf(b))) = (mm',gf(b)) \\ -(g * f) * h(a) & = & μ(d)T(μ(d)T(g)f)h(a) = μ(d)T(μ(d))(TT(g))T(f)(m,h(a)) \\ -\mbox{} & = & μ(d)T(μ(d))(TT(g))(m,(m',fh(a))) \\ & = & μ(d)T(μ(d)(m,(m',(m'',gfh(a)))) = (mm'm'',gfh(a)) \\ -g * (f * h)(a) & = & (μ(d)(T(g)))μ(c)T(f)h(a) = (μ(d)(T(g)))μ(c)T(f)(m,h(a)) \\ -\mbox{} & = & (μ(d)(T(g)))μ(c)(m,(m',fh(a))) \\ & = & μ(d)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} - - -$ μ(b)TT(f)TT(a) = T(f)μ(a)TT(a)$ - -$ μ(b)TT(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: - μ(TTT(a)) - TTTT(a) ----------> TTT(a) - | | - TT(μ(T(a))| |T(μ(T(a))) - | | - v μ(TT(a)) v - TTT(a) -----------> TT(a) -----end-comment: - -\begin{tikzcd} -TTTT(a) \arrow{r}{μ(TTT(a))} \arrow{d}[swap]{TT(μ)} & TTT(a) \arrow{d}{T(μ)} & \mbox{} \\ -TTT(a) \arrow{r}{μ(TT(a))} & TT(a) & \mbox{} \\ -\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} - - ---Vertcial 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/doc/category.ind Sat Mar 04 11:05:40 2017 +0900 @@ -0,0 +1,1602 @@ +-title: Cateogry + +--author: Shinji KONO <kono@ie.u-ryukyu.ac.jp> + +\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: a -> T(a)$ in $A$. In $A_T$, $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) & = & μ(d)T(g)f(b) = μ(d)T(g)(m,f(b)) \\ & = & μ(m,(m',gf(b))) = (mm',gf(b)) \\ +(g * f) * h(a) & = & μ(d)T(μ(d)T(g)f)h(a) = μ(d)T(μ(d))(TT(g))T(f)(m,h(a)) \\ +\mbox{} & = & μ(d)T(μ(d))(TT(g))(m,(m',fh(a))) \\ & = & μ(d)T(μ(d)(m,(m',(m'',gfh(a)))) = (mm'm'',gfh(a)) \\ +g * (f * h)(a) & = & (μ(d)(T(g)))μ(c)T(f)h(a) = (μ(d)(T(g)))μ(c)T(f)(m,h(a)) \\ +\mbox{} & = & (μ(d)(T(g)))μ(c)(m,(m',fh(a))) \\ & = & μ(d)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} + + +$ μ(b)TT(f)TT(a) = T(f)μ(a)TT(a)$ + +$ μ(b)TT(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: + μ(TTT(a)) + TTTT(a) ----------> TTT(a) + | | + TT(μ(T(a))| |T(μ(T(a))) + | | + v μ(TT(a)) v + TTT(a) -----------> TT(a) +----end-comment: + +\begin{tikzcd} +TTTT(a) \arrow{r}{μ(TTT(a))} \arrow{d}[swap]{TT(μ)} & TTT(a) \arrow{d}{T(μ)} & \mbox{} \\ +TTT(a) \arrow{r}{μ(TT(a))} & TT(a) & \mbox{} \\ +\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} + + +--Vertcial 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/doc/fig/Kli-orig.svg Sat Mar 04 11:05:40 2017 +0900 @@ -0,0 +1,79 @@ +<?xml version="1.0"?> + +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> + +<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="37 120 373 171" width="373pt" height="171pt"> +<metadata xmlns:dc="http://purl.org/dc/elements/1.1/"> +<dc:date> 2013-07-02 07:12Z</dc:date> +<!-- Produced by OmniGraffle Professional 5.4.3 --> +</metadata> +<defs> +<font-face font-family="Helvetica" font-size="12" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"> +<font-face-src> +<font-face-name name="Helvetica"/> +</font-face-src> +</font-face> +<marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"> +<g> +<path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> +</g> +</marker> +</defs> +<g stroke="none" stroke-opacity="1" stroke-dasharray="none" fill="none" fill-opacity="1"> +<title> Canvas 1</title> +<rect fill="white" width="559" height="783"/> +<g> +<title> Layer 1</title> +<text transform="translate(46 143)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" x="1.8496094" y="11" textLength="37.634766"> T^2(d) </tspan> +</text> +<text transform="translate(52 268)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" x="2.0019531" y="11" textLength="25.330078"> T(d) </tspan> +</text> +<text transform="translate(182.5 143)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" x="1.6904297" y="11" textLength="56.953125"> T^2(T((d)) </tspan> +</text> +<text transform="translate(192 268)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" x="1.8496094" y="11" textLength="37.634766"> T^2(d) </tspan> +</text> +<text transform="translate(338.5 143)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" x="1.6865234" y="11" textLength="36.960938"> T^2(c) </tspan> +</text> +<text transform="translate(344.5 268)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" x="1.8388672" y="11" textLength="24.65625"> T(c) </tspan> +</text> +<line x1="65.000006" y1="157" x2="65.000006" y2="258.1" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="182.5" y1="150.00001" x2="93.9" y2="150.00001" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="192" y1="275.00001" x2="87.9" y2="275.00001" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="211" y1="157" x2="211" y2="258.1" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="338.5" y1="150.00208" x2="249.4" y2="150.01209" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="357" y1="157" x2="357" y2="258.1" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="344.5" y1="275.00002" x2="239.9" y2="275.00002" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<text transform="translate(274.83959 134.10321)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x="0" y="11" textLength="34.300781"> T^2(g)</tspan> +</text> +<text transform="translate(276 256.30548)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".001953125" y="11" textLength="21.996094"> T(g)</tspan> +</text> +<text transform="translate(125 255.28434)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".001953125" y="11" textLength="21.996094"> μ(d)</tspan> +</text> +<text transform="translate(115 134.5493)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".33691406" y="11" textLength="29.326172"> Tμ(d)</tspan> +</text> +<rect x="71.064266" y="202" width="32" height="24" fill="white"/> +<text transform="translate(76.064266 207)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".001953125" y="11" textLength="21.996094"> μ(d)</tspan> +</text> +<rect x="213.00792" y="201" width="48" height="24" fill="white"/> +<text transform="translate(218.00792 206)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".34082031" y="11" textLength="37.31836"> μ(T(d))</tspan> +</text> +<rect x="368.93134" y="201.89765" width="32" height="24" fill="white"/> +<text transform="translate(373.93134 206.89765)" fill="black"> +<tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".33886719" y="11" textLength="21.322266"> μ(c)</tspan> +</text> +</g> +</g> +</svg> +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc/fig/Kli.graffle Sat Mar 04 11:05:40 2017 +0900 @@ -0,0 +1,1204 @@ +<?xml version="1.0" encoding="UTF-8"?> +<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd"> +<plist version="1.0"> +<dict> + <key>ActiveLayerIndex</key> + <integer>0</integer> + <key>ApplicationVersion</key> + <array> + <string>com.omnigroup.OmniGrafflePro</string> + <string>139.17.0.185490</string> + </array> + <key>AutoAdjust</key> + <true/> + <key>BackgroundGraphic</key> + <dict> + <key>Bounds</key> + <string>{{0, 0}, {559, 783}}</string> + <key>Class</key> + <string>SolidGraphic</string> + <key>ID</key> + <integer>2</integer> + <key>Style</key> + <dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + </dict> + <key>BaseZoom</key> + <integer>0</integer> + <key>CanvasOrigin</key> + <string>{0, 0}</string> + <key>ColumnAlign</key> + <integer>1</integer> + <key>ColumnSpacing</key> + <real>36</real> + <key>CreationDate</key> + <string>2013-07-02 07:00:53 +0000</string> + <key>Creator</key> + <string>Shinji KONO</string> + <key>DisplayScale</key> + <string>1.000 cm = 1.000 cm</string> + <key>GraphDocumentVersion</key> + <integer>8</integer> + <key>GraphicsList</key> + <array> + <dict> + <key>Bounds</key> + <string>{{368.93133932676363, 201.89764779806137}, {32, 24}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>FontInfo</key> + <dict> + <key>Color</key> + <dict> + <key>w</key> + <string>0</string> + </dict> + <key>Font</key> + <string>Helvetica</string> + <key>Size</key> + <real>12</real> + </dict> + <key>ID</key> + <integer>24</integer> + <key>Line</key> + <dict> + <key>ID</key> + <integer>15</integer> + <key>Offset</key> + <real>27.931337356567383</real> + <key>Position</key> + <real>0.51259142160415649</real> + <key>RotationType</key> + <integer>0</integer> + </dict> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 \uc0\u956 (c)}</string> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Bounds</key> + <string>{{213.0079244396849, 200.99999970197678}, {48, 24}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>FontInfo</key> + <dict> + <key>Color</key> + <dict> + <key>w</key> + <string>0</string> + </dict> + <key>Font</key> + <string>Helvetica</string> + <key>Size</key> + <real>12</real> + </dict> + <key>ID</key> + <integer>23</integer> + <key>Line</key> + <dict> + <key>ID</key> + <integer>13</integer> + <key>Offset</key> + <real>26.007923126220703</real> + <key>Position</key> + <real>0.5045045018196106</real> + <key>RotationType</key> + <integer>0</integer> + </dict> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 \uc0\u956 (T(d))}</string> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Bounds</key> + <string>{{71.064266359983762, 201.99999910593033}, {32, 24}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>FontInfo</key> + <dict> + <key>Color</key> + <dict> + <key>w</key> + <string>0</string> + </dict> + <key>Font</key> + <string>Helvetica</string> + <key>Size</key> + <real>12</real> + </dict> + <key>ID</key> + <integer>22</integer> + <key>Line</key> + <dict> + <key>ID</key> + <integer>10</integer> + <key>Offset</key> + <real>22.064260482788086</real> + <key>Position</key> + <real>0.51351350545883179</real> + <key>RotationType</key> + <integer>3</integer> + </dict> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 \uc0\u956 (d)}</string> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Bounds</key> + <string>{{109.99999979138374, 129.54930236107009}, {40, 24}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>FontInfo</key> + <dict> + <key>Color</key> + <dict> + <key>w</key> + <string>0</string> + </dict> + <key>Font</key> + <string>Helvetica</string> + <key>Size</key> + <real>12</real> + </dict> + <key>ID</key> + <integer>21</integer> + <key>Line</key> + <dict> + <key>ID</key> + <integer>11</integer> + <key>Offset</key> + <real>8.4507045745849609</real> + <key>Position</key> + <real>0.53299492597579956</real> + <key>RotationType</key> + <integer>0</integer> + </dict> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>fill</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 T\uc0\u956 (d)}</string> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Bounds</key> + <string>{{119.99999958276749, 250.28434070264922}, {32, 24}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>FontInfo</key> + <dict> + <key>Color</key> + <dict> + <key>w</key> + <string>0</string> + </dict> + <key>Font</key> + <string>Helvetica</string> + <key>Size</key> + <real>12</real> + </dict> + <key>ID</key> + <integer>20</integer> + <key>Line</key> + <dict> + <key>ID</key> + <integer>12</integer> + <key>Offset</key> + <real>12.715668678283691</real> + <key>Position</key> + <real>0.49122807383537292</real> + <key>RotationType</key> + <integer>0</integer> + </dict> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>fill</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 \uc0\u956 (d)}</string> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Bounds</key> + <string>{{271.00000324845314, 251.30547738246162}, {32, 24}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>FontInfo</key> + <dict> + <key>Color</key> + <dict> + <key>w</key> + <string>0</string> + </dict> + <key>Font</key> + <string>Helvetica</string> + <key>Size</key> + <real>12</real> + </dict> + <key>ID</key> + <integer>19</integer> + <key>Line</key> + <dict> + <key>ID</key> + <integer>17</integer> + <key>Offset</key> + <real>11.694541931152344</real> + <key>Position</key> + <real>0.50218337774276733</real> + <key>RotationType</key> + <integer>0</integer> + </dict> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>fill</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 T(g)}</string> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Bounds</key> + <string>{{269.83959170417245, 129.10321376221054}, {45, 24}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>FontInfo</key> + <dict> + <key>Color</key> + <dict> + <key>w</key> + <string>0</string> + </dict> + <key>Font</key> + <string>Helvetica</string> + <key>Size</key> + <real>12</real> + </dict> + <key>ID</key> + <integer>18</integer> + <key>Line</key> + <dict> + <key>ID</key> + <integer>14</integer> + <key>Offset</key> + <real>8.9040489196777344</real> + <key>Position</key> + <real>0.46625664830207825</real> + <key>RotationType</key> + <integer>0</integer> + </dict> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>fill</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Align</key> + <integer>3</integer> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qj + +\f0\fs24 \cf0 T^2(g)}</string> + </dict> + <key>TextPlacement</key> + <integer>0</integer> + <key>TextRelativeArea</key> + <string>{{0, 0}, {1, 1}}</string> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Class</key> + <string>LineGraphic</string> + <key>Head</key> + <dict> + <key>ID</key> + <integer>7</integer> + </dict> + <key>ID</key> + <integer>17</integer> + <key>Points</key> + <array> + <string>{344.5, 275.00001931361396}</string> + <string>{230, 275.00001931361396}</string> + </array> + <key>Style</key> + <dict> + <key>stroke</key> + <dict> + <key>HeadArrow</key> + <string>FilledArrow</string> + <key>Legacy</key> + <true/> + <key>TailArrow</key> + <string>0</string> + </dict> + </dict> + <key>Tail</key> + <dict> + <key>ID</key> + <integer>9</integer> + </dict> + </dict> + <dict> + <key>Class</key> + <string>LineGraphic</string> + <key>Head</key> + <dict> + <key>ID</key> + <integer>9</integer> + </dict> + <key>ID</key> + <integer>15</integer> + <key>Points</key> + <array> + <string>{357.00000197019625, 157}</string> + <string>{357.00000197019625, 268}</string> + </array> + <key>Style</key> + <dict> + <key>stroke</key> + <dict> + <key>HeadArrow</key> + <string>FilledArrow</string> + <key>Legacy</key> + <true/> + <key>TailArrow</key> + <string>0</string> + </dict> + </dict> + <key>Tail</key> + <dict> + <key>ID</key> + <integer>8</integer> + </dict> + </dict> + <dict> + <key>Class</key> + <string>LineGraphic</string> + <key>FontInfo</key> + <dict> + <key>Font</key> + <string>Helvetica</string> + <key>Size</key> + <real>12</real> + </dict> + <key>Head</key> + <dict> + <key>ID</key> + <integer>6</integer> + </dict> + <key>ID</key> + <integer>14</integer> + <key>Notes</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural + +\f0\fs24 \cf0 hoge\ +}</string> + <key>Points</key> + <array> + <string>{338.5, 150.00207794317365}</string> + <string>{239.5, 150.01319774718397}</string> + </array> + <key>Style</key> + <dict> + <key>stroke</key> + <dict> + <key>HeadArrow</key> + <string>FilledArrow</string> + <key>Legacy</key> + <true/> + <key>TailArrow</key> + <string>0</string> + </dict> + </dict> + <key>Tail</key> + <dict> + <key>ID</key> + <integer>8</integer> + </dict> + </dict> + <dict> + <key>Class</key> + <string>LineGraphic</string> + <key>Head</key> + <dict> + <key>ID</key> + <integer>7</integer> + </dict> + <key>ID</key> + <integer>13</integer> + <key>Points</key> + <array> + <string>{211.0000013134642, 157}</string> + <string>{211.0000013134642, 268}</string> + </array> + <key>Style</key> + <dict> + <key>stroke</key> + <dict> + <key>HeadArrow</key> + <string>FilledArrow</string> + <key>Legacy</key> + <true/> + <key>TailArrow</key> + <string>0</string> + </dict> + </dict> + <key>Tail</key> + <dict> + <key>ID</key> + <integer>6</integer> + </dict> + </dict> + <dict> + <key>Class</key> + <string>LineGraphic</string> + <key>Head</key> + <dict> + <key>ID</key> + <integer>5</integer> + </dict> + <key>ID</key> + <integer>12</integer> + <key>Points</key> + <array> + <string>{192, 275.00000938093291}</string> + <string>{78, 275.00000938093291}</string> + </array> + <key>Style</key> + <dict> + <key>stroke</key> + <dict> + <key>HeadArrow</key> + <string>FilledArrow</string> + <key>Legacy</key> + <true/> + <key>TailArrow</key> + <string>0</string> + </dict> + </dict> + <key>Tail</key> + <dict> + <key>ID</key> + <integer>7</integer> + </dict> + </dict> + <dict> + <key>Class</key> + <string>LineGraphic</string> + <key>Head</key> + <dict> + <key>ID</key> + <integer>3</integer> + </dict> + <key>ID</key> + <integer>11</integer> + <key>Points</key> + <array> + <string>{182.5, 150.00000693565505}</string> + <string>{84, 150.00000693565505}</string> + </array> + <key>Style</key> + <dict> + <key>stroke</key> + <dict> + <key>HeadArrow</key> + <string>FilledArrow</string> + <key>Legacy</key> + <true/> + <key>TailArrow</key> + <string>0</string> + </dict> + </dict> + <key>Tail</key> + <dict> + <key>ID</key> + <integer>6</integer> + </dict> + </dict> + <dict> + <key>Class</key> + <string>LineGraphic</string> + <key>Head</key> + <dict> + <key>ID</key> + <integer>5</integer> + </dict> + <key>ID</key> + <integer>10</integer> + <key>Points</key> + <array> + <string>{65.000005877195676, 157}</string> + <string>{65.000005877195676, 268}</string> + </array> + <key>Style</key> + <dict> + <key>stroke</key> + <dict> + <key>HeadArrow</key> + <string>FilledArrow</string> + <key>Legacy</key> + <true/> + <key>TailArrow</key> + <string>0</string> + </dict> + </dict> + <key>Tail</key> + <dict> + <key>ID</key> + <integer>3</integer> + </dict> + </dict> + <dict> + <key>Bounds</key> + <string>{{344.5, 268}, {25, 14}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>ID</key> + <integer>9</integer> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>fill</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Pad</key> + <integer>0</integer> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 T(c) }</string> + <key>VerticalPad</key> + <integer>0</integer> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Bounds</key> + <string>{{338.5, 143}, {37, 14}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>ID</key> + <integer>8</integer> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>fill</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Pad</key> + <integer>0</integer> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 T^2(c) }</string> + <key>VerticalPad</key> + <integer>0</integer> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Bounds</key> + <string>{{192, 268}, {38, 14}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>ID</key> + <integer>7</integer> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>fill</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Pad</key> + <integer>0</integer> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 T^2(d) }</string> + <key>VerticalPad</key> + <integer>0</integer> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Bounds</key> + <string>{{182.5, 143}, {57, 14}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>ID</key> + <integer>6</integer> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>fill</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Pad</key> + <integer>0</integer> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 T^2(T((d)) }</string> + <key>VerticalPad</key> + <integer>0</integer> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Bounds</key> + <string>{{52, 268}, {26, 14}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>ID</key> + <integer>5</integer> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>fill</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Pad</key> + <integer>0</integer> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 T(d) }</string> + <key>VerticalPad</key> + <integer>0</integer> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + <dict> + <key>Bounds</key> + <string>{{46, 143}, {38, 14}}</string> + <key>Class</key> + <string>ShapedGraphic</string> + <key>FitText</key> + <string>YES</string> + <key>Flow</key> + <string>Resize</string> + <key>ID</key> + <integer>3</integer> + <key>Shape</key> + <string>Rectangle</string> + <key>Style</key> + <dict> + <key>fill</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>shadow</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + <key>stroke</key> + <dict> + <key>Draws</key> + <string>NO</string> + </dict> + </dict> + <key>Text</key> + <dict> + <key>Pad</key> + <integer>0</integer> + <key>Text</key> + <string>{\rtf1\ansi\ansicpg1252\cocoartf1187\cocoasubrtf390 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs24 \cf0 T^2(d) }</string> + <key>VerticalPad</key> + <integer>0</integer> + </dict> + <key>Wrap</key> + <string>NO</string> + </dict> + </array> + <key>GridInfo</key> + <dict/> + <key>GuidesLocked</key> + <string>NO</string> + <key>GuidesVisible</key> + <string>YES</string> + <key>HPages</key> + <integer>1</integer> + <key>ImageCounter</key> + <integer>1</integer> + <key>KeepToScale</key> + <false/> + <key>Layers</key> + <array> + <dict> + <key>Lock</key> + <string>NO</string> + <key>Name</key> + <string>Layer 1</string> + <key>Print</key> + <string>YES</string> + <key>View</key> + <string>YES</string> + </dict> + </array> + <key>LayoutInfo</key> + <dict> + <key>Animate</key> + <string>NO</string> + <key>circoMinDist</key> + <real>18</real> + <key>circoSeparation</key> + <real>0.0</real> + <key>layoutEngine</key> + <string>dot</string> + <key>neatoSeparation</key> + <real>0.0</real> + <key>twopiSeparation</key> + <real>0.0</real> + </dict> + <key>LinksVisible</key> + <string>NO</string> + <key>MagnetsVisible</key> + <string>NO</string> + <key>MasterSheets</key> + <array/> + <key>ModificationDate</key> + <string>2013-07-02 07:12:11 +0000</string> + <key>Modifier</key> + <string>Shinji KONO</string> + <key>NotesVisible</key> + <string>NO</string> + <key>Orientation</key> + <integer>2</integer> + <key>OriginVisible</key> + <string>NO</string> + <key>PageBreaks</key> + <string>YES</string> + <key>PrintInfo</key> + <dict> + <key>NSBottomMargin</key> + <array> + <string>float</string> + <string>41</string> + </array> + <key>NSHorizonalPagination</key> + <array> + <string>coded</string> + <string>BAtzdHJlYW10eXBlZIHoA4QBQISEhAhOU051bWJlcgCEhAdOU1ZhbHVlAISECE5TT2JqZWN0AIWEASqEhAFxlwCG</string> + </array> + <key>NSLeftMargin</key> + <array> + <string>float</string> + <string>18</string> + </array> + <key>NSPaperSize</key> + <array> + <string>size</string> + <string>{595, 842}</string> + </array> + <key>NSPrintReverseOrientation</key> + <array> + <string>int</string> + <string>0</string> + </array> + <key>NSRightMargin</key> + <array> + <string>float</string> + <string>18</string> + </array> + <key>NSTopMargin</key> + <array> + <string>float</string> + <string>18</string> + </array> + </dict> + <key>PrintOnePage</key> + <false/> + <key>ReadOnly</key> + <string>NO</string> + <key>RowAlign</key> + <integer>1</integer> + <key>RowSpacing</key> + <real>36</real> + <key>SheetTitle</key> + <string>Canvas 1</string> + <key>SmartAlignmentGuidesActive</key> + <string>YES</string> + <key>SmartDistanceGuidesActive</key> + <string>YES</string> + <key>UniqueID</key> + <integer>1</integer> + <key>UseEntirePage</key> + <false/> + <key>VPages</key> + <integer>1</integer> + <key>WindowInfo</key> + <dict> + <key>CurrentSheet</key> + <integer>0</integer> + <key>ExpandedCanvases</key> + <array> + <dict> + <key>name</key> + <string>Canvas 1</string> + </dict> + </array> + <key>Frame</key> + <string>{{450, 180}, {693, 922}}</string> + <key>ListView</key> + <true/> + <key>OutlineWidth</key> + <integer>142</integer> + <key>RightSidebar</key> + <false/> + <key>ShowRuler</key> + <true/> + <key>Sidebar</key> + <true/> + <key>SidebarWidth</key> + <integer>120</integer> + <key>VisibleRegion</key> + <string>{{0, 0}, {558, 783}}</string> + <key>Zoom</key> + <real>1</real> + <key>ZoomValues</key> + <array> + <array> + <string>Canvas 1</string> + <real>1</real> + <real>1</real> + </array> + </array> + </dict> +</dict> +</plist>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc/fig/Kli.svg Sat Mar 04 11:05:40 2017 +0900 @@ -0,0 +1,64 @@ +<?xml version="1.0"?> + +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> + +<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="37 120 373 171" width="373pt" height="171pt"> +<defs> +<marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"> +<g> <path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> </g> +</marker> +</defs> +<g stroke="none" stroke-opacity="1" stroke-dasharray="none" fill="none" fill-opacity="1"> +<title> Canvas 1</title> +<g> +<title> Layer 1</title> +<text transform="translate(46 143)" fill="black"> +T^2(d) +</text> +<text transform="translate(52 268)" fill="black"> + T(d) +</text> +<text transform="translate(182.5 143)" fill="black"> + T^2(T((d)) +</text> +<text transform="translate(192 268)" fill="black"> + T^2(d) +</text> +<text transform="translate(338.5 143)" fill="black"> + T^2(c) +</text> +<text transform="translate(344.5 268)" fill="black"> + T(c) +</text> +<line x1="65.000006" y1="157" x2="65.000006" y2="258.1" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="182.5" y1="150.00001" x2="93.9" y2="150.00001" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="192" y1="275.00001" x2="87.9" y2="275.00001" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="211" y1="157" x2="211" y2="258.1" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="338.5" y1="150.00208" x2="249.4" y2="150.01209" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="357" y1="157" x2="357" y2="258.1" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<line x1="344.5" y1="275.00002" x2="239.9" y2="275.00002" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/> +<text transform="translate(274.83959 134.10321)" fill="black"> + T^2(g) +</text> +<text transform="translate(276 256.30548)" fill="black"> + T(g) +</text> +<text transform="translate(125 255.28434)" fill="black"> + μ(d) +</text> +<text transform="translate(115 134.5493)" fill="black"> + Tμ(d) +</text> +<text transform="translate(76.064266 207)" fill="black"> + μ(d) +</text> +<text transform="translate(218.00792 206)" fill="black"> + μ(T(d)) +</text> +<text transform="translate(373.93134 206.89765)" fill="black"> + μ(c) +</text> +</g> +</g> +</svg> +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc/fig/Monad.svg Sat Mar 04 11:05:40 2017 +0900 @@ -0,0 +1,3 @@ +<?xml version="1.0"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="57 45 358 146" width="358pt" height="146pt"><metadata xmlns:dc="http://purl.org/dc/elements/1.1/"><dc:date>2013-07-08 10:27Z</dc:date><!-- Produced by OmniGraffle Professional 5.4.3 --></metadata><defs><font-face font-family="Helvetica" font-size="12" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"><font-face-src><font-face-name name="Helvetica"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"><g><path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Hiragino Kaku Gothic ProN" font-size="12" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-60" underline-thickness="63.000004" slope="0" x-height="545" cap-height="766" ascent="880.00183" descent="-120.000244" font-weight="400"><font-face-src><font-face-name name="HiraKakuProN-W3"/></font-face-src></font-face></defs><g stroke="none" stroke-opacity="1" stroke-dasharray="none" fill="none" fill-opacity="1"><title>Canvas 1</title><rect fill="white" width="559" height="783"/><g><title>Layer 1</title><text transform="translate(94 73)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x=".33496094" y="11" textLength="7.330078">T</tspan></text><text transform="translate(172 73)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x=".16992188" y="11" textLength="14.660156">TT</tspan></text><text transform="translate(90.5 150)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x=".16992188" y="11" textLength="14.660156">TT</tspan></text><text transform="translate(172 150)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x="3.834961" y="11" textLength="7.330078">T</tspan></text><text transform="translate(279.5 73)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x=".0048828125" y="11" textLength="21.990234">TTT</tspan></text><text transform="translate(375.5 73)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x=".16992188" y="11" textLength="14.660156">TT</tspan></text><text transform="translate(283 150)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x=".16992188" y="11" textLength="14.660156">TT</tspan></text><text transform="translate(379 150)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" x=".33496094" y="11" textLength="7.330078">T</tspan></text><line x1="102" y1="80" x2="162.1" y2="80" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="98.00016" y1="87" x2="98.0014" y2="140.1" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="105.5" y1="157.00001" x2="162.1" y2="157.00001" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="179.50315" y1="87" x2="179.52704" y2="140.1" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="301.5" y1="80" x2="365.6" y2="80" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="290.49685" y1="87" x2="290.47295" y2="140.1" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="298" y1="157" x2="369.1" y2="157" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="383.00031" y1="87" x2="383.0027" y2="140.1" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><rect x="121.40783" y="56.49032" width="25" height="24" fill="white"/><text transform="translate(126.40783 61.49032)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".16992188" y="11" textLength="14.660156">Tη</tspan></text><rect x="66.92864" y="101.34047" width="26" height="28" fill="white"/><text transform="translate(71.92864 106.34047)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".44096094" y="11" textLength="7.330078">η</tspan><tspan font-family="Hiragino Kaku Gothic ProN" font-size="12" font-weight="400" fill="black" x="7.771039" y="11" textLength="7.788">T</tspan></text><rect x="120" y="157.54842" width="18" height="24" fill="white"/><text transform="translate(125 162.54842)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".33496094" y="11" textLength="7.330078">μ</tspan></text><rect x="185.9823" y="102.99371" width="18" height="24" fill="white"/><text transform="translate(190.9823 107.99371)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".33496094" y="11" textLength="7.330078">μ</tspan></text><rect x="322.5" y="54.685742" width="25" height="24" fill="white"/><text transform="translate(327.5 59.68574)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".16992188" y="11" textLength="14.660156">μT</tspan></text><rect x="260.88343" y="105.99342" width="25" height="24" fill="white"/><text transform="translate(265.88343 110.99342)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".16992188" y="11" textLength="14.660156">Tμ</tspan></text><rect x="321" y="157.95335" width="18" height="24" fill="white"/><text transform="translate(326 162.95335)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".33496094" y="11" textLength="7.330078">μ</tspan></text><rect x="387.04312" y="106.9183" width="18" height="24" fill="white"/><text transform="translate(392.04312 111.9183)" fill="black"><tspan font-family="Helvetica" font-size="12" font-weight="500" fill="black" x=".33496094" y="11" textLength="7.330078">μ</tspan></text></g></g></svg>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc/test.tex Sat Mar 04 11:05:40 2017 +0900 @@ -0,0 +1,189 @@ +\documentclass{jarticle} +\usepackage[dvipdfm]{graphicx} +\usepackage{tikz} +\usepackage{tikz-cd} +\usetikzlibrary{matrix,arrows,decorations.pathmorphing} +\usetikzlibrary{positioning} +\usepackage{amsmath} + +\begin{document} + +\date{} +\title{{\bf Commutative Diagram Exmamples}} +\author{} + +The tikz package +This is a general purpose graphics package. To load it for this document, I used: + + + +\begin{tikzcd} +A \arrow{r}{a} \arrow{d}{b} + &B \arrow{d}{c}\\ +C \arrow{r}{d} &D +\end{tikzcd} + + +\begin{tikzpicture}[scale=1.5] +\node (A) at (0,1) {$A$}; +\node (B) at (1,1) {$B$}; +\node (C) at (0,0) {$C$}; +\node (D) at (1,0) {$D$}; +\path[->,font=\scriptsize,>=angle 90] +(A) edge node[above]{$a$} (B) +(A) edge node[right]{$b$} (C) +(B) edge node[right]{$c$} (D) +(C) edge node[above]{$d$} (D); +\end{tikzpicture} + + +This is part of: Guide to Commutative Diagrams, www.jmilne.org/not/CDGuide.html Last revised October 30, 2012 + +\begin{tikzcd} +ABC A \arrow[hook]{r}\arrow[two heads]{rd} + &B \arrow[dotted]{d}\arrow[hookleftarrow]{r} +&C \arrow[two heads]{ld}\\ D &D +\end{tikzcd} + + +\begin{tikzcd} +A \arrow[hook]{r}{u}[swap]{b} +Aub Bub C \arrow[two heads]{rd}{u}[swap]{b} +&B \arrow[dotted]{d}{r}[swap]{l} + \arrow[hookleftarrow]{r}{u}[swap]{b} +D &C \arrow[two heads]{ld}{b}[swap]{u}\\ &D +\end{tikzcd} + +\begin{tikzcd} + A\arrow{r}\arrow{d} + &B\arrow{r}{\text{very long label}}\arrow{d} + &C\arrow{d}\\ +DEF D\arrow{r}&E\arrow{r}&F +\end{tikzcd} + +% \begin{tikzcd}[column sep=large] +% A\arrow{r}\arrow{d} + + +\begin{tikzcd} +A B A\arrow[bend left]{r}\arrow[bend right]{r}&B +\end{tikzcd} + + +\begin{tikzcd} +T\arrow[bend left]{drr}{x} +\arrow[bend right]{ddr}[swap]{y} +\arrow[dotted]{dr}[description]{(x,y)} & & \\ +& X \times_Z Y \arrow{r}{p} \arrow{d}{q} & X \arrow{d}{f} \\ +& Y \arrow{r}{g} & Z +\end{tikzcd} + + + + + + +\begin{tikzpicture} +\node (A) at (-1,0) {$A$}; +\node (B) at (1,0) {$B$}; +\node at (0,0) {\rotatebox{270}{$\Rightarrow$}}; +\path[->,font=\scriptsize,>=angle 90] + (A) edge [bend left] node[above] {$\alpha$} (B) + edge [bend right] node[below] {$\beta$} (B); +\end{tikzpicture} + +\begin{tikzpicture} +\node (P0) at (90:2.8cm) {$X\otimes (Y\otimes (Z\otimes T))$}; +\node (P1) at (90+72:2.5cm) {$X\otimes ((Y\otimes Z)\otimes T))$} ; +\node (P2) at (90+2*72:2.5cm) {${(X\otimes (Y\otimes Z))}\otimes T$}; +\node (P3) at (90+3*72:2.5cm) {$((X\otimes Y){\otimes Z)\otimes T}$}; +\node (P4) at (90+4*72:2.5cm) {$(X\otimes Y)\otimes (Z\otimes T)$}; +\draw +(P0) edge[->,>=angle 90] node[left] {$1\otimes\phi$} (P1) +(P1) edge[->,>=angle 90] node[left] {$\phi$} (P2) +(P2) edge[->,>=angle 90] node[above] {$\phi\otimes 1$} (P3) +(P4) edge[->,>=angle 90] node[right] {$\phi$} (P3) +(P0) edge[->,>=angle 90] node[right] {$\phi$} (P4); +\end{tikzpicture} + + +\begin{tikzpicture} +\node (a) at (0,0) {$Y\times_X Y$}; +\node (b) at (2,0) {$Y$}; +\node (c) at (3.5,0) {$X$}; +\path[->,font=\scriptsize,>=angle 90] +([yshift= 2pt]a.east) edge node[above] {$p_1$} ([yshift= 2pt]b.west) +([yshift= -2pt]a.east) edge node[below] {$p_2$} ([yshift= -2pt]b.west) +(b) edge (c); +\end{tikzpicture} + +\begin{tikzpicture}[descr/.style={fill=white},text height=1.5ex, text depth=0.25ex] +\node (a) at (0,0) {$\mathsf{S}(Z)$}; +\node (b) at (2.5,0) {$\mathsf{S}(X)$}; +\node (c) at (5,0) {$\mathsf{S}(U).$}; +\path[->,font=\scriptsize,>=angle 90] +([yshift= 9pt]b.west) edge node[above] {$i^{\ast}$} ([yshift= 9pt]a.east) +(a.east) edge node[descr] {$i_{\ast}$} (b.west) +([yshift= -9pt]b.west) edge node[below] {$i^!$} ([yshift= -9pt]a.east) +([yshift= 9pt]c.west) edge node[above] {$j_!$} ([yshift= 9pt]b.east) +(b.east) edge node[descr] {$j^{\ast}$} (c.west) +([yshift= -9pt]c.west) edge node[below] {$j_*$} ([yshift= -9pt]b.east); +\end{tikzpicture} + + +\begin{tikzpicture}[>=angle 90,scale=2.2,text height=1.5ex, text depth=0.25ex] +%%First place the nodes +\node (k-1) at (0,3) {$0$}; +\node (k0) [right=of k-1] {$Ker f$}; +\node (k1) [right=of k0] {$Ker a$}; +\node (k2) [right=of k1] {$Ker b$}; +\node (k3) [right=of k2] {$Ker c$}; +\node (a1) [below=of k1] {$A$}; +\node (a2) [below=of k2] {$B$}; +\node (a3) [below=of k3] {$C$}; +\node (a4) [right=of a3] {$0$}; +\node (b1) [below=of a1] {$A’$}; +\node (b0) [left=of b1] {$0$}; +\node (b2) [below=of a2] {$B’$}; +\node (b3) [below=of a3] {$C’$}; +\node (c1) [below=of b1] {$Coker a$}; +\node (c2) [below=of b2] {$Coker b$}; +\node (c3) [below=of b3] {$Coker c$}; +\node (c4) [right=of c3] {$Coker g’$}; +\node (c5) [right=of c4] {$0$}; +%%Draw the red arrows +\draw[->,red,font=\scriptsize] +(k-1) edge (k0) +(k0) edge (k1) +(k1) edge (k2) +(k2) edge (k3) +(c1) edge (c2) +(c2) edge (c3) +(c3) edge (c4) +(c4) edge (c5); +%%Draw the curvy red arrow +%\draw[->,red] +%(k3) edge[out=0,in=180,red] node[pos=0.55,yshift=5pt] {$d$} (c1); +%%Draw the black arrows +%\draw[->] +(k1) edge (a1) +(k2) edge (a2) +(k3) edge (a3) +(b1) edge (c1) +(b2) edge (c2) +(b3) edge (c3); +%%Draw the thick blue arrows +\draw[->,font=\scriptsize,blue,thick] +(a1) edge node[auto] {$f$} (a2) +(a2) edge node[auto] {$g$} (a3) +(a3) edge (a4) +(a1) edge node[auto] {$a$} (b1) +(a2) edge node[auto] {$b$} (b2) +(a3) edge node[auto] {$c$} (b3) +(b0) edge (b1) +(b1) edge node[below] {$f’$} (b2) +(b2) edge node[below] {$g’$} (b3); +\end{tikzpicture} + + +\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc/test2.tex Sat Mar 04 11:05:40 2017 +0900 @@ -0,0 +1,271 @@ +\documentclass{jarticle} +\usepackage[dvipdfm]{graphicx} +\usepackage{tikz} +\usepackage{tikz-cd} +\usetikzlibrary{matrix,arrows,decorations.pathmorphing} +\usetikzlibrary{positioning} +\usepackage{amsmath} + +\begin{document} + +\date{} +\title{{\bf Commutative Diagram Exmamples}} +\author{} + +The tikz package +This is a general purpose graphics package. To load it for this document, I used: + + +There are now three ways to enter commutative diagrams using tikz: with the package tikz-cd, with matrix, and directly with tikz (listed roughly in order of decreasing ease but increasing flexibility). + +\begin{tikzcd} +A \arrow{r}{a} \arrow{d}{b} + &B \arrow{d}{c}\\ +C \arrow{r}{d} &D +\end{tikzcd} + +\begin{tikzpicture} +\matrix(m)[matrix of math nodes, row sep=2.6em, column sep=2.8em, text height=1.5ex, text depth=0.25ex] +{A & B \\ + C & D \\ }; +\path[->,font=\scriptsize,>=angle 90] +(m-1-1) edge node[auto] {$a$} (m-1-2) + edge node[auto] {$b$} (m-2-1) +(m-1-2) edge node[auto] {$c$} (m-2-2) +(m-2-1) edge node[auto] {$d$} (m-2-2); +\end{tikzpicture} + +\begin{tikzpicture}[scale=1.5] +\node (A) at (0,1) {$A$}; +\node (B) at (1,1) {$B$}; +\node (C) at (0,0) {$C$}; +\node (D) at (1,0) {$D$}; +\path[->,font=\scriptsize,>=angle 90] +(A) edge node[above]{$a$} (B) +(A) edge node[right]{$b$} (C) +(B) edge node[right]{$c$} (D) +(C) edge node[above]{$d$} (D); +\end{tikzpicture} + + +This is part of: Guide to Commutative Diagrams, www.jmilne.org/not/CDGuide.html Last revised October 30, 2012 + +\begin{tikzcd} +ABC A \arrow[hook]{r}\arrow[two heads]{rd} + &B \arrow[dotted]{d}\arrow[hookleftarrow]{r} +&C \arrow[two heads]{ld}\\ D &D +\end{tikzcd} + + +\begin{tikzcd} +A \arrow[hook]{r}{u}[swap]{b} +Aub Bub C \arrow[two heads]{rd}{u}[swap]{b} +&B \arrow[dotted]{d}{r}[swap]{l} + \arrow[hookleftarrow]{r}{u}[swap]{b} +D &C \arrow[two heads]{ld}{b}[swap]{u}\\ &D +\end{tikzcd} + +\begin{tikzcd} + A\arrow{r}\arrow{d} + &B\arrow{r}{\text{very long label}}\arrow{d} + &C\arrow{d}\\ +DEF D\arrow{r}&E\arrow{r}&F +\end{tikzcd} + +% \begin{tikzcd}[column sep=large] +% A\arrow{r}\arrow{d} + + +\begin{tikzcd} +A B A\arrow[bend left]{r}\arrow[bend right]{r}&B +\end{tikzcd} + +\begin{tikzcd} +&A\arrow{ldd}[swap]{f}\arrow{rd}[description]{c} + \arrow{rrd}[description]{d} + \arrow{rrrd}[description]{e}\\ +&B\arrow{ld}\arrow{r}&C\arrow{r}&D\arrow{r}&E\\ +F +\end{tikzcd} + +\begin{tikzcd} +T\arrow[bend left]{drr}{x} +\arrow[bend right]{ddr}[swap]{y} +\arrow[dotted]{dr}[description]{(x,y)} & & \\ +& X \times_Z Y \arrow{r}{p} \arrow{d}{q} & X \arrow{d}{f} \\ +& Y \arrow{r}{g} & Z +\end{tikzcd} + +\begin{tikzpicture}[>=angle 90] +\matrix(a)[matrix of math nodes, +row sep=3em, column sep=2.5em, +text height=1.5ex, text depth=0.25ex] +{A&B&C\\ +&D\\}; +\path[right hook->](a-1-1) edge (a-1-2); +\path[->>](a-1-1) edge (a-2-2); +\path[dotted,->](a-1-2) edge (a-2-2); +\path[left hook->](a-1-3) edge (a-1-2); +\path[->>](a-1-3) edge (a-2-2); +\end{tikzpicture} + + + +\begin{tikzpicture} +\matrix(m)[matrix of math nodes, +row sep=3em, column sep=2.8em, +text height=1.5ex, text depth=0.25ex] +{A&B\\}; +\path[->] +(m-1-1) edge [bend left] (m-1-2) + edge [bend left=40] (m-1-2) + edge [bend left=60] (m-1-2) + edge [bend left=80] (m-1-2) + edge [bend right] (m-1-2); +\end{tikzpicture} + +\[ +\begin{tikzpicture}[descr/.style={fill=white}] +\matrix(m)[matrix of math nodes, row sep=3em, column sep=2.8em, text height=1.5ex, text depth=0.25ex] +{&A\\&B&C&D&E\\F\\}; +\path[->,font=\scriptsize] +(m-1-2) edge node[above left] {$f$} (m-3-1) + edge node[descr] {$c$} (m-2-3) + edge node[descr] {$d$} (m-2-4) + edge node[descr] {$e$} (m-2-5); +\path[->] +(m-2-2) edge (m-3-1) + edge (m-2-3); +\path[->] +(m-2-3) edge (m-2-4); +\path[->] +(m-2-4) edge (m-2-5); +\end{tikzpicture} +\] + +\[ +\begin{tikzpicture}[descr/.style={fill=white}] +\matrix(m)[matrix of math nodes, row sep=3em, column sep=2.8em, +text height=1.5ex, text depth=0.25ex] +{T\\&X\times_Z Y&X\\&Y&Z\\}; +7 + +\path[->,font=\scriptsize] +(m-1-1) edge [bend left=10] node[above] {$x$} (m-2-3) +(m-1-1) edge [bend right=10] node[below] {$y$} (m-3-2); +\path[->,dotted,font=\scriptsize] +(m-1-1) edge node[descr] {$(x,y)$} (m-2-2); +\path[->,font=\scriptsize] +(m-2-2) edge node[below] {$p$} (m-2-3) +(m-2-2) edge node[right] {$q$} (m-3-2); +\path[->,font=\scriptsize] +(m-2-3) edge node[right] {$f$} (m-3-3); +\path[->,font=\scriptsize] +(m-3-2) edge node[above] {$g$} (m-3-3); +\end{tikzpicture} +\] + +\begin{tikzpicture} +\node (A) at (-1,0) {$A$}; +\node (B) at (1,0) {$B$}; +\node at (0,0) {\rotatebox{270}{$\Rightarrow$}}; +\path[->,font=\scriptsize,>=angle 90] + (A) edge [bend left] node[above] {$\alpha$} (B) + edge [bend right] node[below] {$\beta$} (B); +\end{tikzpicture} + +\begin{tikzpicture} +\node (P0) at (90:2.8cm) {$X\otimes (Y\otimes (Z\otimes T))$}; +\node (P1) at (90+72:2.5cm) {$X\otimes ((Y\otimes Z)\otimes T))$} ; +\node (P2) at (90+2*72:2.5cm) {${(X\otimes (Y\otimes Z))}\otimes T$}; +\node (P3) at (90+3*72:2.5cm) {$((X\otimes Y){\otimes Z)\otimes T}$}; +\node (P4) at (90+4*72:2.5cm) {$(X\otimes Y)\otimes (Z\otimes T)$}; +\draw +(P0) edge[->,>=angle 90] node[left] {$1\otimes\phi$} (P1) +(P1) edge[->,>=angle 90] node[left] {$\phi$} (P2) +(P2) edge[->,>=angle 90] node[above] {$\phi\otimes 1$} (P3) +(P4) edge[->,>=angle 90] node[right] {$\phi$} (P3) +(P0) edge[->,>=angle 90] node[right] {$\phi$} (P4); +\end{tikzpicture} + + +\begin{tikzpicture} +\node (a) at (0,0) {$Y\times_X Y$}; +\node (b) at (2,0) {$Y$}; +\node (c) at (3.5,0) {$X$}; +\path[->,font=\scriptsize,>=angle 90] +([yshift= 2pt]a.east) edge node[above] {$p_1$} ([yshift= 2pt]b.west) +([yshift= -2pt]a.east) edge node[below] {$p_2$} ([yshift= -2pt]b.west) +(b) edge (c); +\end{tikzpicture} + +\begin{tikzpicture}[descr/.style={fill=white},text height=1.5ex, text depth=0.25ex] +\node (a) at (0,0) {$\mathsf{S}(Z)$}; +\node (b) at (2.5,0) {$\mathsf{S}(X)$}; +\node (c) at (5,0) {$\mathsf{S}(U).$}; +\path[->,font=\scriptsize,>=angle 90] +([yshift= 9pt]b.west) edge node[above] {$i^{\ast}$} ([yshift= 9pt]a.east) +(a.east) edge node[descr] {$i_{\ast}$} (b.west) +([yshift= -9pt]b.west) edge node[below] {$i^!$} ([yshift= -9pt]a.east) +([yshift= 9pt]c.west) edge node[above] {$j_!$} ([yshift= 9pt]b.east) +(b.east) edge node[descr] {$j^{\ast}$} (c.west) +([yshift= -9pt]c.west) edge node[below] {$j_*$} ([yshift= -9pt]b.east); +\end{tikzpicture} + + +\begin{tikzpicture}[>=angle 90,scale=2.2,text height=1.5ex, text depth=0.25ex] +%%First place the nodes +\node (k-1) at (0,3) {$0$}; +\node (k0) [right=of k-1] {$Ker f$}; +\node (k1) [right=of k0] {$Ker a$}; +\node (k2) [right=of k1] {$Ker b$}; +\node (k3) [right=of k2] {$Ker c$}; +\node (a1) [below=of k1] {$A$}; +\node (a2) [below=of k2] {$B$}; +\node (a3) [below=of k3] {$C$}; +\node (a4) [right=of a3] {$0$}; +\node (b1) [below=of a1] {$A’$}; +\node (b0) [left=of b1] {$0$}; +\node (b2) [below=of a2] {$B’$}; +\node (b3) [below=of a3] {$C’$}; +\node (c1) [below=of b1] {$Coker a$}; +\node (c2) [below=of b2] {$Coker b$}; +\node (c3) [below=of b3] {$Coker c$}; +\node (c4) [right=of c3] {$Coker g’$}; +\node (c5) [right=of c4] {$0$}; +%%Draw the red arrows +\draw[->,red,font=\scriptsize] +(k-1) edge (k0) +(k0) edge (k1) +(k1) edge (k2) +(k2) edge (k3) +(c1) edge (c2) +(c2) edge (c3) +(c3) edge (c4) +(c4) edge (c5); +%%Draw the curvy red arrow +\draw[->,red] +(k3) edge[out=0,in=180,red] node[pos=0.55,yshift=5pt] {$d$} (c1); +%%Draw the black arrows +\draw[->] +(k1) edge (a1) +(k2) edge (a2) +(k3) edge (a3) +(b1) edge (c1) +(b2) edge (c2) +(b3) edge (c3); +%%Draw the thick blue arrows +\draw[->,font=\scriptsize,blue,thick] +(a1) edge node[auto] {$f$} (a2) +(a2) edge node[auto] {$g$} (a3) +(a3) edge (a4) +(a1) edge node[auto] {$a$} (b1) +(a2) edge node[auto] {$b$} (b2) +(a3) edge node[auto] {$c$} (b3) +(b0) edge (b1) +(b1) edge node[below] {$f’$} (b2) +(b2) edge node[below] {$g’$} (b3); +\end{tikzpicture} + + +\end{document}