-title: Cateogry --author: Shinji KONO \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) $