-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)  $