|
0
|
1 -title: Cateogry
|
|
|
2
|
|
|
3 \usepackage{tikz}
|
|
|
4 \usepackage{tikz-cd}
|
|
|
5
|
|
|
6 --Adjunction
|
|
|
7
|
|
|
8 \begin{eqnarray*}
|
|
|
9 Uε○ηU & = & 1_U \\
|
|
|
10 εF○Fη & = & 1_F
|
|
|
11 \end{eqnarray*}
|
|
|
12
|
|
|
13 $f: a -> Ub $
|
|
|
14
|
|
31
|
15 ----begin-comment:
|
|
|
16 FU(b)
|
|
|
17 ・ |
|
|
|
18 ・ |
|
|
|
19 F(f) ・ |
|
|
|
20 ・ ε(b)
|
|
|
21 ・ |
|
|
|
22 ・ f* v
|
|
|
23 F(a) -----------------> b
|
|
0
|
24
|
|
31
|
25 U(f*)
|
|
|
26 UF(a) -----------------> Ub
|
|
|
27 ^ ・
|
|
|
28 | ・
|
|
|
29 | ・
|
|
|
30 η(a) ・ f
|
|
|
31 | ・
|
|
|
32 | ・ f = U(f*)η
|
|
|
33 |・
|
|
|
34 a
|
|
0
|
35
|
|
31
|
36 ----end-comment:
|
|
0
|
37
|
|
|
38 \begin{tikzcd}
|
|
|
39 \mbox{} & FU(b) \arrow{d}{ε(b)} \\
|
|
|
40 F(a) \arrow{ru}{F(f)} \arrow{r}{f*} & b \\
|
|
|
41 UF(a) \arrow{r}{U(f*)} & Ub \\
|
|
|
42 a \arrow{u}{η(a)} \arrow{ru}{f} & \\
|
|
|
43 \end{tikzcd}
|
|
|
44
|
|
|
45 Universal mapping problem is
|
|
|
46 for each $f:->Ub$, there exists $f*$ such that $f = U(f*)η$.
|
|
|
47
|
|
|
48 --Adjunction to Universal mapping
|
|
|
49
|
|
|
50 In adjunction $(F,U,ε,η)$, put $f* = ε(b)F(f)$,
|
|
|
51 we are going to prove $f*$ is a solution of Universal mmapping problem. That is $U(f*)η = f$.
|
|
|
52
|
|
|
53 \begin{tikzcd}
|
|
|
54 UF(a) \arrow{r}[swap]{UF(f)} \arrow[bend left]{rr}{U(ε(b)F(f))=U(f*)}
|
|
|
55 & UFUb \arrow{r}[swap]{U(ε(b))} & \mbox{?} \\
|
|
|
56 a \arrow{u}{η(a)} \arrow{r}[swap]{f} & Ub \arrow{u}{η(Ub)} \\
|
|
|
57 \end{tikzcd}
|
|
|
58
|
|
|
59 \begin{tikzcd}
|
|
|
60 UF(a) \arrow{rd}[swap]{U(f*)} \arrow{r}{UF(f)} & UFUb \arrow[bend left]{d}{U(ε(b))} \\
|
|
|
61 a \arrow{u}{η(a)} \arrow{r}[swap]{f} & Ub \arrow{u}{η(Ub)} \\
|
|
|
62 F(a) \arrow{r}{F(f)} \arrow{rd}[swap]{f*} & FU(b) \arrow{d}{ε(b)} \\
|
|
|
63 \mbox{} & b \\
|
|
|
64 \end{tikzcd}
|
|
|
65 ∵$ Uε○ηU = 1_U $
|
|
|
66
|
|
|
67 \[ U(ε(b))η(U(b)) = 1_{U(b)} \]
|
|
|
68
|
|
|
69 means that
|
|
|
70
|
|
|
71 $ε(b) : FU(b)->b $ is solution of $1_{U(b)}$.
|
|
|
72
|
|
|
73 naturality $ fη(U(b)) = U(F(f))η(a) $
|
|
|
74
|
|
|
75 gives solution $ U(ε(b))UF(f) = U(F(f)ε(b)) $ for $f$.
|
|
|
76
|
|
|
77
|
|
|
78
|
|
|
79 \[ U(f*)η(a)(a) = f(a) \]
|
|
|
80
|
|
|
81 then
|
|
|
82
|
|
|
83 $U(ε(b)F(f))η(a)(a) = U(ε(b))UF(f)η(a)(a) $
|
|
|
84
|
|
|
85 since $F$ is a functor. And we have
|
|
|
86
|
|
|
87 $U(ε(b))UF(f)η(a)(a) = U(ε(b))η(b)f(a)$
|
|
|
88
|
|
|
89 because of naturality of $η$
|
|
|
90
|
|
31
|
91 ----begin-comment:
|
|
|
92 η(a)
|
|
|
93 UF(a) <------- a UF(f)η(a) = η(b)f
|
|
|
94 | |
|
|
|
95 |UF(f) f|
|
|
|
96 v v
|
|
|
97 UF(b) <------- b
|
|
|
98 η(b)
|
|
0
|
99
|
|
31
|
100 ----end-comment:
|
|
0
|
101
|
|
|
102 \begin{tikzcd}
|
|
|
103 UF(a) \arrow[leftarrow]{r}{η(a)} \arrow{d}{UF(f)} & a \arrow{d}{f} & UF(f)η(a) = η(b)f \\
|
|
|
104 UF(b) \arrow[leftarrow]{r}{η(b)} & b &
|
|
|
105 \end{tikzcd}
|
|
|
106
|
|
|
107 too bad.... we need some thing more.
|
|
|
108
|
|
|
109
|
|
|
110 ---Adjoint of η
|
|
|
111
|
|
|
112 $ Uε○ηU = 1_U $
|
|
|
113
|
|
31
|
114 ----begin-comment:
|
|
|
115 F(f) ε(b)
|
|
|
116 F(a) ---------> FU(b) --------> b
|
|
0
|
117
|
|
31
|
118 UF(f) U(ε(b))
|
|
|
119 UF(a) --------> UFU(b) --------> U(b)
|
|
0
|
120
|
|
31
|
121 η(a) UF(f) U(ε(b))
|
|
|
122 a ---------> UF(a) --------> UFU(b) --------> U(b)
|
|
0
|
123
|
|
31
|
124 f η(Ub) U(ε(b))
|
|
|
125 a ---------> Ub --------> UFU(b) --------> U(b)
|
|
0
|
126
|
|
31
|
127 η(Ub) U(ε(b)) = 1
|
|
|
128 ∵ Uε○ηU = 1_U
|
|
0
|
129
|
|
31
|
130 ----end-comment:
|
|
0
|
131
|
|
|
132 \begin{tikzcd}
|
|
|
133 F(a) \arrow{r}{F(f)} & FU(b) \arrow{r}{ε(b)} & b & \\
|
|
|
134 UF(a) \arrow{r}{UF(f)} & UFU(b) \arrow{r}{U(ε(b))} & U(b) & \\
|
|
|
135 a \arrow{r}{η(a)} & UF(a) \arrow{r}{UF(f)} & UFU(b) \arrow{r}{U(ε(b))} & U(b) \\
|
|
|
136 a \arrow{r}{f} & Ub \arrow{r}{η(Ub)}[swap]{η(Ub)} & UFU(b) \arrow{r}{U(ε(b))}[swap]{U(ε(b))=1} & U(b) \\
|
|
|
137 \end{tikzcd}
|
|
|
138
|
|
|
139
|
|
|
140 ∵ $Uε○ηU = 1_U$
|
|
|
141
|
|
|
142 naturality of $f:a->Ub$
|
|
|
143
|
|
31
|
144 ----begin-comment:
|
|
0
|
145
|
|
31
|
146 η(Ub)
|
|
|
147 Ub ---------> UF(Ub)
|
|
|
148 ^ ^
|
|
|
149 | |
|
|
|
150 f| |UF(f)
|
|
|
151 | η(a) |
|
|
|
152 a ---------> UF(a)
|
|
0
|
153
|
|
31
|
154 ----end-comment:
|
|
0
|
155
|
|
|
156 \begin{tikzcd}
|
|
|
157 Ub \arrow{r}{η(Ub)} & UF(Ub) \\
|
|
|
158 a \arrow{u}{f} \arrow{r}{η(a)} & UF(a) \arrow{u}[swap]{UF(f)}
|
|
|
159 \end{tikzcd}
|
|
|
160
|
|
31
|
161 ----begin-comment:
|
|
0
|
162
|
|
31
|
163 UF(f)
|
|
|
164 UF(a) ------------->UF(U(b)) UF(U(b))
|
|
|
165 ^ ^ |
|
|
|
166 | | |
|
|
0
|
167 η(a)| η(U(b))| |U(ε(U(b)))
|
|
31
|
168 | f | v
|
|
|
169 a --------------->U(b) U(b)
|
|
0
|
170
|
|
31
|
171 ----end-comment:
|
|
0
|
172
|
|
|
173 \begin{tikzcd}
|
|
|
174 UF(a) \arrow{r}{UF(f)} & UF(U(b)) & UF(U(b)) \arrow{d}{U(ε(U(b)))} & \mbox{} \\
|
|
|
175 a \arrow{r}{f} \arrow{u}[swap]{η(a)} & U(b) \arrow{u}[swap]{η(U(b))} & U(b) & \mbox{} \\
|
|
|
176 \end{tikzcd}
|
|
|
177
|
|
|
178 Solution of universal mapping yields naturality of $Uε○ηU = 1_U$.
|
|
|
179
|
|
31
|
180 ----begin-comment:
|
|
0
|
181
|
|
31
|
182 F(η(a))
|
|
|
183 UF(a) F(a) ----------> FUF(a)
|
|
|
184 ^ |
|
|
|
185 | |
|
|
0
|
186 η(a)| |ε(F(a))
|
|
31
|
187 | η(a) v
|
|
|
188 a --------------->UF(a) F(a)
|
|
0
|
189
|
|
31
|
190 ----end-comment:
|
|
0
|
191
|
|
|
192 $εF○Fη = 1_F$.
|
|
|
193
|
|
|
194 \begin{tikzcd}
|
|
|
195 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{} \\
|
|
|
196 a \arrow{r}[swap]{η(a)} \arrow{u}{η(a)} & UF(a) & F(a) & \mbox{} \\
|
|
|
197 \end{tikzcd}
|
|
|
198
|
|
|
199 --Universal mapping to adjunction
|
|
|
200
|
|
|
201 Functor $U$, mapping $F(a)$ and $(f)*, U(f*)η(a) = f $ are given.
|
|
|
202
|
|
|
203 object $F(a):A -> B$
|
|
|
204
|
|
|
205 $ η(a): a->UF(a)$
|
|
|
206
|
|
|
207 put
|
|
41
|
208 \[ F(f) = (η(U(b))f)* \]
|
|
0
|
209 \[ ε : FU -> 1_B \]
|
|
|
210 \[ ε(b) = (1_{U(b)})* \]
|
|
|
211
|
|
31
|
212 ----begin-comment:
|
|
|
213 f*
|
|
|
214 F(a) -----------------> b
|
|
0
|
215
|
|
31
|
216 U(f*)
|
|
|
217 UF(a) -----------------> Ub
|
|
|
218 ^ ・
|
|
|
219 | ・
|
|
|
220 | ・
|
|
|
221 η(a) ・ f
|
|
|
222 | ・
|
|
|
223 | ・ f = U(f*)η
|
|
|
224 |・
|
|
|
225 a
|
|
|
226 ----end-comment:
|
|
0
|
227
|
|
|
228 \begin{tikzcd}
|
|
|
229 F(a) \arrow{r}{f*} & b \\
|
|
|
230 UF(a) \arrow{r}{U(f*)} & Ub \\
|
|
|
231 a \arrow{u}{η(a)} \arrow{ur}{f}
|
|
|
232 \end{tikzcd}
|
|
|
233
|
|
|
234 $f = U(f*)η$
|
|
|
235
|
|
|
236 Show F is a Functor, that is $F(fg) = F(f)F(g)$.
|
|
|
237
|
|
|
238 Show naturality of $η(a)$.
|
|
|
239
|
|
|
240 \[ f:a->b, F(f) = (η(b)f)*\]
|
|
|
241
|
|
|
242 Show naturality of $ε(b) = (1_U)*$.
|
|
|
243
|
|
|
244 ---Definitions
|
|
|
245
|
|
|
246 f's destination
|
|
|
247 \[ f: a -> U(b) \]
|
|
|
248 universal mapping
|
|
|
249 \[ U(f*)η(a) = f \]
|
|
|
250 defnition of F(f)
|
|
|
251 \[ F(f) = (η(U(b))f)* \]
|
|
|
252 definition of $ε$
|
|
|
253 \[ ε(b) = (1_{U(b)})* \]
|
|
|
254
|
|
31
|
255 ----begin-comment:
|
|
0
|
256
|
|
31
|
257 FU(f*)
|
|
|
258 FUF(a)------------->FU(b)
|
|
|
259 ^| |
|
|
|
260 ||ε(F(a)) |
|
|
|
261 F(η(a))|| |ε(b)=(1_U(b))*
|
|
|
262 || (η(Ub)f)*=F(f) |
|
|
|
263 |v v
|
|
|
264 F(a) --------------->b
|
|
|
265 f*
|
|
|
266 UF(f)
|
|
|
267 UF(a)------------->UFU(b)
|
|
|
268 ^ ^|
|
|
|
269 | U(f*) ||
|
|
|
270 η(a)| η(U(b))||U(ε(b))
|
|
|
271 | ||
|
|
|
272 | |v
|
|
|
273 a --------------->U(b)
|
|
|
274 f
|
|
0
|
275
|
|
31
|
276 ----end-comment:
|
|
0
|
277
|
|
|
278 \begin{tikzcd}
|
|
|
279 FUF(a) \arrow{r}{FU(f*)} \arrow{d}{ε(F(a))} & FU(b) \arrow{d}{ε(b)=(1_U(b))*} & \mbox{} \\
|
|
|
280 F(a) \arrow{r}[swap]{f*} \arrow[bend left]{u}{F(η(a))} \arrow{ru}[swap]{F(f)} & b & \mbox{} \\
|
|
|
281 UF(a) \arrow{r}{UF(f)} \arrow{rd}[swap]{U(f*)} & UFU(b) \arrow[bend left]{d}{U(ε(b))} & \mbox{} \\
|
|
|
282 a \arrow{r}[swap]{f} \arrow{u}{η(a)} & U(b) \arrow{u}{η(U(b))} & \mbox{} \\
|
|
|
283 \end{tikzcd}
|
|
|
284
|
|
|
285 $εF○Fη = 1_F$,
|
|
|
286 $ ε(b) = (1_{U(b)})* $,
|
|
|
287
|
|
|
288 $ ε(F(a)) = (1_{UF(a)})* $
|
|
|
289
|
|
|
290
|
|
31
|
291 ----begin-comment:
|
|
0
|
292
|
|
31
|
293 F(η(a))
|
|
|
294 UF(a) F(a) --------------> FUF(a)
|
|
|
295 ^ |^
|
|
|
296 | ||
|
|
|
297 η(a)| U(1_{F(a)}) 1_{F(a)} ε(F(a))||F(η(a))
|
|
|
298 | ||
|
|
|
299 | v|
|
|
|
300 a ---------------> U(F(a)) F(a)
|
|
|
301 η(a)
|
|
0
|
302
|
|
31
|
303 ----end-comment:
|
|
0
|
304
|
|
|
305 \begin{tikzcd}
|
|
|
306 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{} \\
|
|
|
307 a \arrow{r}[swap]{η(a)} \arrow{u}{η(a)} & U(F(a)) & F(a) \arrow[bend right]{u}[swap]{F(η(a))} & \mbox{} \\
|
|
|
308 \end{tikzcd}
|
|
|
309
|
|
|
310
|
|
|
311
|
|
|
312
|
|
|
313
|
|
|
314 --- Functor F
|
|
|
315
|
|
|
316 \[ F(f) = (η(b)f)* \]
|
|
|
317
|
|
|
318 \[ U(F(f))η(a) = η(b)f \]
|
|
|
319
|
|
|
320
|
|
|
321 show $F(fg) = F(f)F(g)$
|
|
|
322
|
|
|
323
|
|
31
|
324 ----begin-comment:
|
|
|
325 g f
|
|
|
326 a -----> Ub ----> UUc
|
|
|
327 ----end-comment:
|
|
0
|
328
|
|
|
329 \begin{tikzcd}
|
|
|
330 a \arrow{r}{g} & Ub \arrow{r}{f} & UUc
|
|
|
331 \end{tikzcd}
|
|
|
332
|
|
|
333 \begin{eqnarray*}
|
|
|
334 U(F(g))η(a) & = & η(Ub)g \\
|
|
|
335 U(F(f))η(Ub) & = & η(UUc)f
|
|
|
336 \end{eqnarray*}
|
|
|
337
|
|
|
338 show
|
|
|
339 \[
|
|
|
340 U(F(f)F(g))η(a) = η(UUc)fg
|
|
|
341 \]
|
|
|
342
|
|
|
343 then $F(f)F(g) = F(fg)$
|
|
|
344
|
|
|
345 \begin{eqnarray*}
|
|
|
346 U(F(f)F(g))η(a) & = & UF(f)UF(g)η(a) \\
|
|
|
347 & = & UF(f)η(Ub)g \\
|
|
|
348 & = & η(UUc)fg
|
|
|
349 \end{eqnarray*}
|
|
|
350 \mbox{Q.E.D.}
|
|
|
351
|
|
31
|
352 ----begin-comment:
|
|
|
353 FU(f)
|
|
|
354 FU(b) -------------> FUU(c)
|
|
|
355 ・ | |
|
|
|
356 ・ | |
|
|
|
357 F(g) ・ | |
|
|
|
358 ・ ε(b) ε(Uc) |
|
|
|
359 ・ | |
|
|
|
360 ・ g* v f* v
|
|
|
361 F(a) -----------------> b ---------------> c
|
|
0
|
362
|
|
31
|
363 U(F(f))
|
|
|
364 UF(a) UFUb
|
|
|
365 ^ ・ ^ ・
|
|
|
366 | ・ | ・
|
|
|
367 | ・ | ・
|
|
|
368 η(a) ・ UFg | ・ UFf
|
|
|
369 | ・ η(Ub) ・
|
|
|
370 | ・ | ・
|
|
|
371 | g ・ | f ・
|
|
|
372 a -----------------> Ub ---------------> UU(c)
|
|
|
373 ----end-comment:
|
|
0
|
374
|
|
|
375
|
|
|
376 \begin{tikzcd}
|
|
|
377 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)} \\
|
|
|
378 \mbox{} & b & U(c) \\
|
|
|
379 \\
|
|
|
380 UF(a) \arrow{rd}{U(g*)} \arrow{r}{UFg} & UFUb \arrow{rd}{Uf*} \arrow{r}{UFf} & UFUUc \\
|
|
|
381 a \arrow{r}{g}\arrow{u}{η(a)} & Ub \arrow{r}{f} \arrow{u}[swap]{η(Ub)} & UU(c) \arrow{u}[swap]{η(UUc)}
|
|
|
382 \end{tikzcd}
|
|
|
383
|
|
|
384 --- naturality of η
|
|
|
385
|
|
|
386 $ η: 1->UB $
|
|
|
387
|
|
31
|
388 ----begin-comment:
|
|
0
|
389
|
|
31
|
390 UF(a)-----------------> UFb
|
|
|
391 ^ UF(f) ^
|
|
|
392 | |
|
|
|
393 | |
|
|
|
394 η(a) η(b)
|
|
|
395 | |
|
|
|
396 | f |
|
|
|
397 a -----------------> b
|
|
|
398 ----end-comment:
|
|
0
|
399
|
|
|
400 \begin{tikzcd}
|
|
|
401 UF(a) \arrow{r}[swap]{UF(f)} & UFb \\
|
|
|
402 a \arrow{r}{f} \arrow{u}{η(a)} & b \arrow{u}{η(b)}
|
|
|
403 \end{tikzcd}
|
|
|
404
|
|
|
405 prove $η(b)f = UF(f)η(a) $
|
|
|
406 \begin{eqnarray*}
|
|
|
407 & η(b)f: & a-> UFb \\
|
|
|
408 F(f) & = & (η(b)f)* \mbox{\hspace{1cm}(definition)} \\
|
|
|
409 η(b)f & = & U(F(f))η(a)
|
|
|
410 \end{eqnarray*}
|
|
|
411 \mbox{Q.E.D.}
|
|
|
412
|
|
|
413 --- naturality of ε
|
|
|
414
|
|
|
415 \[
|
|
|
416 ε : FU -> 1_B
|
|
|
417 \]
|
|
|
418 \[
|
|
|
419 U: B->A
|
|
|
420 \]
|
|
|
421
|
|
|
422 $ ε(b) = (1_{U(b)})*$
|
|
|
423
|
|
|
424 $ U(ε(b))η(U(b)) = 1_{U(b)}$
|
|
|
425
|
|
|
426 $ U(ε(b))η(U(b))U(b) = U(b)$
|
|
|
427
|
|
|
428
|
|
31
|
429 ----begin-comment:
|
|
|
430 FU(f)
|
|
|
431 FU(b) -------------> FU(c)
|
|
|
432 | |
|
|
|
433 | |
|
|
|
434 ε(b) | ε(c)
|
|
|
435 | |
|
|
|
436 v f v
|
|
|
437 b ---------------> c
|
|
|
438 ----end-comment:
|
|
0
|
439
|
|
|
440 \begin{tikzcd}
|
|
|
441 FU(b) \arrow{r}{FU(f)} \arrow{d}{ε(b)} & FU(c) \arrow{d}{ε(c)}\\
|
|
|
442 b \arrow{r}{f} & c
|
|
|
443 \end{tikzcd}
|
|
|
444
|
|
|
445 prove $fε(b) = ε(c)FU(f)$
|
|
|
446
|
|
|
447
|
|
|
448 \[ f = Ub -> Uc \]
|
|
|
449
|
|
31
|
450 ----begin-comment:
|
|
0
|
451
|
|
31
|
452 FU(f) (1_U(c))*
|
|
|
453 F(Ub) --------------> FU(c) ---------------> c
|
|
0
|
454
|
|
31
|
455 (1_U(b))* f
|
|
|
456 F(Ub) ----------------> b -----------------> c
|
|
0
|
457
|
|
31
|
458 U(1_U(b)*) U(f)
|
|
|
459 UF(Ub) ----------------> Ub -----------------> U(c)
|
|
|
460 || ・ ||
|
|
|
461 || ・ ||
|
|
|
462 || UFU(f) ・ U(1_U(c)*) ||
|
|
|
463 UF(Ub) ----- ・ ------> UFUc ---------------> U(c)
|
|
|
464 ^ ・ ^ ||
|
|
|
465 | ・ | ||
|
|
|
466 η(Ub) ・ 1_Ub η(Uc) | ||
|
|
|
467 |・ | 1_Uc ||
|
|
|
468 Ub ------------------> Uc -----------------> U(c)
|
|
|
469 U(f)
|
|
0
|
470
|
|
31
|
471 ----end-comment:
|
|
0
|
472
|
|
|
473 \begin{tikzcd}
|
|
|
474 F(Ub) \arrow{r}{(1_{U(b)})*} & b \arrow{r}{f} & c \\
|
|
|
475 UF(Ub) \arrow{r}{U(1_{U(b)})*} \arrow{rd}[swap]{UFU(f)} & Ub \arrow{r}{U(f)} & U(c) \\
|
|
|
476 \mbox{} & UFUc \arrow{ru}{U(1_U(c)*)} & \\
|
|
|
477 Ub \arrow{r}{U(f)} \arrow{ruu}[swap]{1_{Ub}} \arrow{uu}{η(Ub)} & Uc \arrow{ruu}[swap]{1_{Uc}} \arrow{u}{η(Uc)} \\
|
|
|
478 F(Ub) \arrow{r}{FU(f)} & FU(c) \arrow{r}{(1_{U(c)})*} & c \\
|
|
|
479 \end{tikzcd}
|
|
|
480
|
|
31
|
481 ----begin-comment:
|
|
0
|
482
|
|
|
483 \begin{tikzcd}
|
|
|
484 \mbox{} & Ub \arrow{r}{U(f)} & U(c) \\
|
|
|
485 UF(Ub) \arrow{ru}{U(1_U(b)*)} \arrow{r}[swap]{UFU(f)} & UFUc \arrow{ru}{U(1_U(c)*)} & \\
|
|
|
486 Ub \arrow{r}{U(f)} \arrow{ruu}{1_Ub} \arrow{u}{η(Ub)} & Uc \arrow{ruu}[swap]{1_Uc} \arrow{u}{η(Uc)} & \mbox{}
|
|
|
487 \end{tikzcd}
|
|
|
488
|
|
|
489
|
|
|
490 \begin{tikzcd}
|
|
|
491 UF(Ub) \arrow{d}{U(1_U(b)*)} \arrow{r}{UFU(f)} & UFUc \arrow{d}{U(1_U(c)*)} \\
|
|
|
492 Ub \arrow{r}{U(f)} & U(c) \\
|
|
|
493 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)}
|
|
|
494 \end{tikzcd}
|
|
|
495
|
|
31
|
496 ----end-comment:
|
|
0
|
497
|
|
|
498
|
|
|
499 show $ε(c)FU(f)$ and $fε(b)$ are both solution of $(1_{Uc})U(f) ( = U(f)(1_{Ub}))$
|
|
|
500
|
|
|
501 \[
|
|
|
502 (fε(b)))η(Ub)Ub = U(f))U(ε(b))η(Ub)Ub
|
|
|
503 \]
|
|
|
504 \[
|
|
|
505 = U(f)1_{U(b)}Ub = U(f)Ub = Ufb = U(f)(1_{Ub})Ub
|
|
|
506 \]
|
|
|
507 \[
|
|
|
508 \mbox{∴}fε(b) = (U(f)(1_{Ub}))*
|
|
|
509 \]
|
|
|
510
|
|
|
511 $ UFU(f)η(Ub) = η(Uc)U(f)$ naturality of η
|
|
|
512
|
|
|
513 \[
|
|
|
514 U(ε(c)FU(f))η(Ub)Ub = U(ε(c))UFU(f)η(Ub)Ub
|
|
|
515 \]
|
|
|
516 \[
|
|
|
517 = U(ε(c))η(Uc)U(f)Ub = 1_{U(c)}U(f)Ub = U(f)Ub = U(f)(1_{Ub})Ub
|
|
|
518 \]
|
|
|
519 \[
|
|
|
520 \mbox{∵} U(ε(c))η(Uc) = 1_U(c)
|
|
|
521 \]
|
|
|
522
|
|
|
523 end of proof.
|
|
|
524
|
|
31
|
525 ----begin-comment:
|
|
|
526 U(f*)
|
|
|
527 c U(c) <- ----------- U(b) b
|
|
|
528 ^ ^| |^ ^
|
|
|
529 | U(ε(c))||η(U(c)) η(U(b))||U(ε(b)) |
|
|
|
530 |ε(c) || || ε(b)|
|
|
|
531 | |v UFU(f) v| |
|
|
|
532 FU(c) UFU(c) <----------- UFU(b) FU(b)
|
|
|
533 ----end-comment:
|
|
0
|
534
|
|
|
535 \begin{tikzcd}
|
|
|
536 c \arrow[bend left,leftarrow]{rrr}{f}
|
|
|
537 & U(c) \arrow[leftarrow]{r}{U(f)} \arrow{d}{η(U(c))} & U(b) \arrow{d}[swap]{η(U(b))} & b \\
|
|
|
538 FU(c) \arrow{u}{(1_{Uc})* = ε(c)} \arrow[bend right,leftarrow]{rrr}{FU(f)} &
|
|
|
539 UFU(c) \arrow[leftarrow]{r}{UFU(f)} \arrow[bend left]{u}{U(ε(c))} & UFU(b) \arrow[bend right]{u}[swap]{U(ε(b))}
|
|
|
540 & FU(b) \arrow{u}[swap]{ε(b) = (1_{Ub})*}
|
|
|
541 \end{tikzcd}
|
|
|
542
|
|
|
543 It also prove
|
|
|
544
|
|
|
545 \[ Uε○ηU = 1_U\]
|
|
|
546
|
|
|
547 ---$Uε○ηU = 1_U$
|
|
|
548
|
|
|
549 $ ε(b) = (1_U(b))* $
|
|
|
550
|
|
|
551 that is
|
|
|
552
|
|
|
553 $ U((1_U(b)*)η(U(b)) = 1_U(b) $
|
|
|
554 $ U(ε(b))η(U(b)) = 1_U(b) $
|
|
|
555
|
|
|
556 $ \mbox{∴} Uε○ηU = 1_U $
|
|
|
557
|
|
|
558 --- $εF○Fη = 1_F$
|
|
|
559
|
|
|
560 $ η(a) = U(1_F(a))η(a) $
|
|
|
561
|
|
|
562 $=> (η(a))* = 1_F(a)$ ... (1)
|
|
|
563
|
|
|
564 $ ε(F(a)) = (1_UF(a))*$
|
|
|
565
|
|
|
566 $=> 1_UF(a) = U(ε(F(a)))η(UF(a)) $
|
|
|
567
|
|
|
568 times $η(a)$ from left
|
|
|
569
|
|
|
570 $ η(a) = U(ε(F(a)))η(UF(a))η(a)$
|
|
|
571
|
|
|
572 $η(UF(a)) = UFη(a)$ naturality of $η$
|
|
|
573
|
|
|
574 $ η(a) = U(ε(F(a)))(UFη(a))η(a) $ \\
|
|
|
575 $ = U(ε(F(a)Fη(a)))η(a) $ \\
|
|
|
576 $ => (η(a))* = ε(F(a))Fη(a) .... (2) $ \\
|
|
|
577
|
|
|
578 from (1),(2), since $(η(a))*$ is unique
|
|
|
579
|
|
|
580 \[ ε(F(a))Fη(a) = 1_F(a) \]
|
|
|
581
|
|
31
|
582 ----begin-comment:
|
|
0
|
583
|
|
31
|
584 F U
|
|
|
585 UF(a) --------> FUF(a) ----------> UFUF(a) FUF(a)
|
|
|
586 ^ ^| |^ ^|
|
|
|
587 | || || ||
|
|
|
588 |η(a) F(η(a))||ε(F(a)) U(εF(a))||η(UF(a)) ||ε(F(a))
|
|
|
589 | || || ||
|
|
|
590 | F |v U v| |v
|
|
|
591 a ------------> F(a) ------------> UF(a) F(a)
|
|
|
592 ----end-comment:
|
|
0
|
593
|
|
|
594
|
|
|
595 \begin{tikzcd}
|
|
|
596 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))} \\
|
|
|
597 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))} \\
|
|
|
598 \mbox{} & F(a) \arrow{u}{(η(a))* = 1_{Fa}} \arrow{rr}{U} & & UF(a) \arrow{u}[swap]{η(a) = U(εF(a))η(UF(a))}
|
|
|
599 \end{tikzcd}
|
|
|
600
|
|
|
601 \begin{tikzcd}
|
|
|
602 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{} \\
|
|
|
603 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{} \\
|
|
|
604 \end{tikzcd}
|
|
|
605
|
|
31
|
606 ----begin-comment:
|
|
0
|
607
|
|
|
608 UUF(a)
|
|
|
609 ^ |
|
|
|
610 | |
|
|
|
611 η(UF(a))| |U(ε(Fa)) U(ε(F(a))η(UF(a)) = 1_UF(a)
|
|
|
612 | v ε(F(a) = (1_UF(a))*
|
|
|
613 UF(a)
|
|
31
|
614 ----end-comment:
|
|
0
|
615
|
|
|
616 \begin{tikzcd}
|
|
|
617 UUF(a) \arrow[bend left]{d}{U(ε(Fa))} \\
|
|
|
618 UF(a) \arrow[bend left]{u}{η(UF(a))}
|
|
|
619 \end{tikzcd}
|
|
|
620 $U(ε(F(a)))η(UF(a)) = 1_UF(a) $ \\
|
|
|
621 $ ε(F(a)) = (1_UF(a))* $
|
|
|
622
|
|
|
623
|
|
31
|
624 ----begin-comment:
|
|
0
|
625 FA -------->UFA
|
|
|
626 | |
|
|
|
627 | Fη(A) | UFηA
|
|
|
628 v v
|
|
|
629 FUFA ------>UFUFA
|
|
31
|
630 ----end-comment:
|
|
0
|
631
|
|
|
632 \begin{tikzcd}
|
|
|
633 FA \arrow{r} \arrow{d}{Fη(A)} & UFA \arrow{d}{UFηA} \\
|
|
|
634 FUFA \arrow{r} & UFUFA
|
|
|
635 \end{tikzcd}
|
|
|
636
|
|
|
637 $ε(FA)$の定義から $U(ε(FA)): UFUFA→UFA$
|
|
|
638
|
|
|
639 唯一性から $ε(F(A)):FUFA→FA$ 従って
|
|
|
640
|
|
|
641 \[ ε(F(A))Fη(A)=1 \]
|
|
|
642
|
|
|
643 ってなのを考えました。
|
|
|
644
|
|
|
645
|
|
|
646 $ Uη(A') = U(1(FA'))η(A')$より \\
|
|
|
647 $ η(A')*=1(FA')$、 \\
|
|
|
648 $ Uη(A') = U(ε(FA')Fη(A'))η(A')$より \\
|
|
|
649 $ η(A')*=ε(FA')Fη(A')$から \\
|
|
|
650 $ 1_F=εF.Fη$は言えました。 \\
|
|
|
651
|
|
|
652 後者で$η$の自然性と$ε$の定義を使いました。
|
|
|
653
|
|
|
654
|
|
|
655 --おまけ
|
|
|
656
|
|
|
657 $ εF○Fη=1_F, Uε○ηU = 1_U $
|
|
31
|
658 ----begin-comment:
|
|
0
|
659
|
|
|
660 U
|
|
|
661 UFU(a) <--------------- FU(a)
|
|
|
662 ^| |
|
|
|
663 η(U(a))||U(ε(a)) |ε(a)
|
|
|
664 |v v
|
|
|
665 U(a) <---------------- (a)
|
|
|
666 U
|
|
|
667
|
|
|
668 F
|
|
|
669 FUF(a) <--------------- UF(a)
|
|
|
670 ^| ^
|
|
|
671 Fη(a)||εF(a) |η(a)
|
|
|
672 |v |
|
|
|
673 F(a) <---------------- (a)
|
|
|
674 F
|
|
|
675
|
|
31
|
676 ----end-comment:
|
|
0
|
677
|
|
|
678 \begin{tikzcd}
|
|
|
679 UFU(a) \arrow[leftarrow]{r}{U} \arrow[bend left]{d}{U(ε(a))} & FU(a) \arrow{d}{ε(a)} & \mbox{} \\
|
|
|
680 U(a) \arrow[leftarrow]{r}[swap]{U} \arrow[bend left]{u}{η(U(a))} & (a) & \mbox{} \\
|
|
|
681 FUF(a) \arrow[leftarrow]{r}{F} \arrow[bend left]{d}{εF(a)} & UF(a) & \mbox{} \\
|
|
|
682 F(a) \arrow[leftarrow]{r}[swap]{F} \arrow[bend left]{u}{Fη(a)} & (a) \arrow{u}[swap]{η(a)} & \mbox{} \\
|
|
|
683 \end{tikzcd}
|
|
|
684
|
|
|
685
|
|
|
686
|
|
|
687 なら、 $ FU(ε(F(a))) = εF(a) $ ?
|
|
|
688
|
|
31
|
689 ----begin-comment:
|
|
0
|
690 U
|
|
|
691 UFU(F(a)) <--------------- FU(F(a))
|
|
|
692 ^| |
|
|
|
693 η(U(a))||U(ε(F(a))) |ε(F(a))
|
|
|
694 |v v
|
|
|
695 U(F(a)) <---------------- F(a)
|
|
|
696 U
|
|
|
697
|
|
|
698 FU
|
|
|
699 FUFU(F(a)) <--------------- FU(F(a))
|
|
|
700 ^| |
|
|
|
701 Fη(U(a))||FU(ε(F(a))) |ε(F(a))
|
|
|
702 |v v
|
|
|
703 FU(F(a)) <---------------- F(a)
|
|
|
704 FU
|
|
|
705
|
|
|
706 F
|
|
|
707 FUF(a) <--------------- UF(a)
|
|
|
708 ^| ^
|
|
|
709 Fη(a)||εF(a) |η(a)
|
|
|
710 |v |
|
|
|
711 F(a) <---------------- (a)
|
|
|
712 F
|
|
31
|
713 ----end-comment:
|
|
0
|
714
|
|
|
715 \begin{tikzcd}
|
|
|
716 UFU(F(a)) \arrow[leftarrow]{r}{U} \arrow[bend left]{d}{U(ε(F(a)))} & FU(F(a)) \arrow{d}{ε(F(a))} & \mbox{} \\
|
|
|
717 U(F(a)) \arrow[leftarrow]{r}[swap]{U} \arrow[bend left]{u}{η(U(a))} & F(a) & \mbox{} \\
|
|
|
718 FUFU(F(a)) \arrow[leftarrow]{r}{FU} \arrow[bend left]{d}{FU(ε(F(a)))} & FU(F(a)) \arrow{d}{ε(F(a))} & \mbox{} \\
|
|
|
719 FU(F(a)) \arrow[leftarrow]{r}[swap]{FU} \arrow[bend left]{u}{Fη(U(a))} & F(a) & \mbox{} \\
|
|
|
720 FUF(a) \arrow[leftarrow]{r}{F} \arrow[bend left]{d}{εF(a)} & UF(a) & \mbox{} \\
|
|
|
721 F(a) \arrow[leftarrow]{r}[swap]{F} \arrow[bend left]{u}{Fη(a)} & (a) \arrow{u}[swap]{η(a)} & \mbox{} \\
|
|
|
722 \end{tikzcd}
|
|
|
723
|
|
|
724 --Monad
|
|
|
725
|
|
|
726 $(T,η,μ)$
|
|
|
727
|
|
|
728 $ T: A -> A $
|
|
|
729
|
|
|
730 $ η: 1_A -> T $
|
|
|
731
|
|
|
732 $ μ: T^2 -> T $
|
|
|
733
|
|
|
734 $ μ○Tη = 1_T = μ○ηT $ Unity law
|
|
|
735
|
|
|
736 $ μ○μT = μ○Tμ $ association law
|
|
|
737
|
|
31
|
738 ----begin-comment:
|
|
0
|
739 Tη μT
|
|
|
740 T ---------> T^2 T^3---------> T^2
|
|
|
741 |・ | | |
|
|
|
742 | ・1_T | | |
|
|
|
743 ηT| ・ |μ Tμ| |μ
|
|
|
744 | ・ | | |
|
|
|
745 v ・ v v v
|
|
|
746 T^2 -------> T T^2 --------> T
|
|
|
747 μ μ
|
|
31
|
748 ----end-comment:
|
|
0
|
749
|
|
|
750 \begin{tikzcd}
|
|
|
751 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{} \\
|
|
|
752 T^2 \arrow{r}[swap]{μ} & T & T^2 \arrow{r}[swap]{μ} & T & \mbox{} \\
|
|
|
753 \end{tikzcd}
|
|
|
754
|
|
|
755
|
|
|
756 --Adjoint to Monad
|
|
|
757
|
|
|
758 Monad (UF, η, UεF) on adjoint (U,F, η, ε)
|
|
|
759
|
|
|
760 \begin{eqnarray*}
|
|
|
761 εF○Fμ & = & 1_F \\
|
|
|
762 Uε○μU & = & 1_U \\
|
|
|
763 \end{eqnarray*}
|
|
|
764
|
|
|
765 \begin{eqnarray*}
|
|
|
766 μ○Tη & = & (UεF)○(UFη) = U (εF○Fη) = U 1_F = 1_{UF} \\
|
|
|
767 μ○ηT & = & (UεF)○(ηUF) = (Uε○ηU) F = 1_U F = 1_{UF} \\
|
|
|
768 \end{eqnarray*}
|
|
|
769
|
|
|
770 \begin{eqnarray*}
|
|
|
771 (UεF)○(ηUF) & = & (U(ε(F(b))))(UF(η(b))) \\
|
|
|
772 & = & U(ε(F(b))F(η(b))) = U(1_F) \\
|
|
|
773 \end{eqnarray*}
|
|
|
774
|
|
31
|
775 ----begin-comment:
|
|
0
|
776
|
|
|
777 UεFUF εFUF ε(a)
|
|
|
778 UFUFUF-------> UFUF FUFUF-------> FUF FU(a)---------->a
|
|
|
779 | | | | | |
|
|
|
780 | | | | | |
|
|
|
781 UFUεF| |UεF FUεF| |εF FU(f)| |f
|
|
|
782 | | | | | |
|
|
|
783 v v v v v v
|
|
|
784 UFUF --------> UF FUF --------> F FU(b)---------> b
|
|
|
785 UεF εF ε(b)
|
|
|
786
|
|
31
|
787 ----end-comment:
|
|
0
|
788
|
|
|
789 \begin{tikzcd}
|
|
|
790 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{} \\
|
|
|
791 UFUF \arrow{r}{UεF} & UF & FUF \arrow{r}[swap]{εF} & F & FU(b) \arrow{r}[swap]{ε(b)} & b & \mbox{} \\
|
|
|
792 \end{tikzcd}
|
|
|
793
|
|
|
794 association law
|
|
|
795
|
|
|
796 \begin{eqnarray*}
|
|
|
797 μ ○ μ T & = & μ ○ T μ \\
|
|
|
798 Uε(a)F ○ Uε(a)F FU & = & Uε(a)F ○ FU Uε(a)F \\
|
|
|
799 \end{eqnarray*}
|
|
|
800
|
|
|
801 $UεF○UεFFU=UεF○FUUεF$
|
|
|
802
|
|
|
803 naturality of $ε$
|
|
|
804
|
|
|
805 $ ε(b)FU(f)(a) = fε(a) $
|
|
|
806
|
|
|
807 $ a = FUF(a), b = F(a), f = εF $
|
|
|
808
|
|
|
809 \begin{eqnarray*}
|
|
|
810 ε(F(a))(FU(εF))(a) & = & (εF)(εFUF(a)) \\
|
|
|
811 U(ε(F(a))(FU(εF))(a)) & = & U((εF)(εFUF(a))) \\
|
|
|
812 U(ε(F(a))(FU(εF))(a)) & = & U((εF)(εFUF(a))) \\
|
|
|
813 UεF○FUUεF & = UεF○UεFFU \\
|
|
|
814 \end{eqnarray*}
|
|
|
815
|
|
31
|
816 ----begin-comment:
|
|
0
|
817
|
|
|
818 FU(ε(F(a)))
|
|
|
819 FUF(a) <-------------FUFUF(a)
|
|
|
820 | |
|
|
|
821 |ε(F(a)) |ε(FUF(a))
|
|
|
822 | |
|
|
|
823 v v
|
|
|
824 F(a) <------------- FUF(a)
|
|
|
825 ε(F(a))
|
|
|
826
|
|
31
|
827 ----end-comment:
|
|
0
|
828
|
|
|
829 \begin{tikzcd}
|
|
|
830 FUF(a) \arrow[leftarrow]{r}{FU(ε(F(a)))} \arrow{d}{ε(F(a))} & FUFUF(a) \arrow{d}{ε(FUF(a))} & \mbox{} \\
|
|
|
831 F(a) \arrow[leftarrow]{r}[swap]{ε(F(a))} & FUF(a) & \mbox{} \\
|
|
|
832 \end{tikzcd}
|
|
|
833
|
|
|
834 --Eilenberg-Moore category
|
|
|
835
|
|
|
836 $(T,η,μ)$
|
|
|
837
|
|
|
838 $A^T$ object $(A,φ)$
|
|
|
839
|
|
|
840 $ φη(A) = 1_A, φμ(A) = φT(φ) $
|
|
|
841
|
|
|
842 arrow $f$.
|
|
|
843
|
|
|
844 $ φT(f) = fφ $
|
|
|
845
|
|
|
846
|
|
31
|
847 ----begin-comment:
|
|
0
|
848
|
|
|
849 η(a) μ(a) T(f)
|
|
|
850 a-----------> T(a) T^2(a)--------> T(a) T(a)---------->T(b)
|
|
|
851 | | | | |
|
|
|
852 | | | | |
|
|
|
853 |φ T(φ)| |φ φ| |φ'
|
|
|
854 | | | | |
|
|
|
855 v v v v v
|
|
|
856 _ a T(a)-------->T(a) a------------> b
|
|
|
857 φ f
|
|
|
858
|
|
31
|
859 ----end-comment:
|
|
0
|
860
|
|
|
861 \begin{tikzcd}
|
|
|
862 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{} \\
|
|
|
863 \mbox{} & a & T(a) \arrow{r}[swap]{φ} & T(a) & a \arrow{r}[swap]{f} & b & \mbox{} \\
|
|
|
864 \end{tikzcd}
|
|
|
865
|
|
|
866 --EM on monoid
|
|
|
867
|
|
|
868 $f: a-> b$
|
|
|
869
|
|
|
870 $T: a -> (m,a) $
|
|
|
871
|
|
|
872 $η: a -> (1,a) $
|
|
|
873
|
|
|
874 $μ: (m,(m',a)) -> (mm',a) $
|
|
|
875
|
|
|
876 $φ: (m,a) -> φ(m,a) = ma $
|
|
|
877
|
|
31
|
878 ----begin-comment:
|
|
0
|
879
|
|
|
880 η(a) μ(a) T(f)
|
|
|
881 a----------->(1,a) (m,(m',a))-----> (mm',a) (m,a)----------->(m,f(a))
|
|
|
882 | | | | |
|
|
|
883 | | | | |
|
|
|
884 |φ T(φ)| |φ φ| |φ'
|
|
|
885 | | | | |
|
|
|
886 v v v v v
|
|
|
887 _ 1a (m,m'a)-------->mm'a ma------------> mf(a)=f(ma)
|
|
|
888 φ f
|
|
31
|
889 ----end-comment:
|
|
0
|
890
|
|
|
891 \begin{tikzcd}
|
|
|
892 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{} \\
|
|
|
893 \mbox{} & 1a & (m,m'a) \arrow{r}[swap]{φ} & mm'a & ma \arrow{r}[swap]{f} & mf(a)=f(ma) & \mbox{} \\
|
|
|
894 \end{tikzcd}
|
|
|
895
|
|
|
896 object $(a,φ)$. arrow $f$.
|
|
|
897
|
|
|
898 $ φT(f)(m,a) = fφ(m,a) $
|
|
|
899
|
|
|
900 $ φ(m,f(a)) = f(a) $
|
|
|
901
|
|
|
902 $ U^T : A^T->A $
|
|
|
903
|
|
|
904 $ U^T(a,φ) = a, U^T(f) = f $
|
|
|
905
|
|
|
906 $ F^T : A->A^T$
|
|
|
907
|
|
|
908 $ F^T(a) = (T(a),μ(a)), F^T(f) = T(F) $
|
|
|
909
|
|
|
910 --Comparison Functor $K^T$
|
|
|
911
|
|
|
912 $ K^T(B) = (U(B),Uε(B))a, K^T(f) = U(g) $
|
|
|
913
|
|
|
914 $ U^T K^T (b) = U(b) $
|
|
|
915
|
|
|
916 $ U^TK^T(f) = U^TU(f) = U(f) $
|
|
|
917
|
|
|
918 $ K^TF(a) = (UF(a),Uε(F(a))) = (T(a), μ(a)) = F^T(a) $
|
|
|
919
|
|
|
920 $ K^TF(f) = UF(f) = T(f) = F^T(f) $
|
|
|
921
|
|
|
922 $ ηU(a,φ) = η(a), Uε(a,φ) = ε^TK^T(b) = Uε(b) $
|
|
|
923
|
|
31
|
924 ----begin-comment:
|
|
0
|
925
|
|
|
926
|
|
|
927 _ Ba _
|
|
|
928 |^
|
|
|
929 ||
|
|
|
930 ||
|
|
|
931 K_T F||U K^T
|
|
|
932 ||
|
|
|
933 ||
|
|
|
934 ||
|
|
|
935 U_T v| F^T
|
|
|
936 A_T---------> A ---------> A^T
|
|
|
937 <--------- <--------
|
|
|
938 F_T U^T
|
|
|
939
|
|
31
|
940 ----end-comment:
|
|
0
|
941
|
|
|
942
|
|
|
943 \begin{tikzcd}
|
|
|
944 \mbox{} & B \arrow{r}{K^T} \arrow{rd}{F} \arrow[leftarrow]{rd}[swap]{U} & A^T \arrow{d}{U^T} & \mbox{} \\
|
|
|
945 \mbox{} & A_T \arrow{r}[swap]{U_T} \arrow[leftarrow]{r}{F_T} \arrow{u}[swap]{K_T} & A \arrow{u}{F^T} & \mbox{} \\
|
|
|
946 \\
|
|
|
947 \mbox{} & B \arrow{d}{F} \arrow{rd}{K^T} & \mbox{} \\
|
|
|
948 A_T \arrow{r}{U_T} \arrow{ru}[leftarrow]{K_T} & A \arrow{r}{F^T} \arrow{u}{U} & A^T & \mbox{} \\
|
|
|
949 \end{tikzcd}
|
|
|
950
|
|
|
951 --Kleisli Category
|
|
|
952
|
|
|
953 Object of $A$.
|
|
|
954
|
|
4
|
955 Arrow $f: a -> T(a)$ in $A$. In $A_T$, $f: b -> c, g: c -> d$,
|
|
0
|
956
|
|
|
957 $ g * f = μ(d)T(g)f $
|
|
|
958
|
|
|
959 $η(b):b->T(b)$ is an identity.
|
|
|
960
|
|
|
961 $ f * η(b) = μ(c)T(f)η(b) = μ(c)η(T(c))f = 1_T(c) f = f $
|
|
|
962
|
|
|
963 and
|
|
|
964
|
|
|
965 $ η(c) * f = μ(c)Tη(c)f = 1_T(c) f = f $
|
|
|
966
|
|
|
967 association law $ g * (f * h) = (g * f) * h $,
|
|
|
968
|
|
|
969 $h: a -> T(b), f: b -> T(c), g: c -> T(d) $,
|
|
|
970
|
|
|
971 naturality of $μ$
|
|
|
972
|
|
31
|
973 ----begin-comment:
|
|
0
|
974
|
|
|
975 μ(c) T(f) h
|
|
|
976 f*h _ _ T(c) <---------------- T^2(c) <------- T(b) <----------- a
|
|
|
977
|
|
|
978
|
|
|
979 μ(d) T(g) μ(c) T(f) h
|
|
|
980 g*(f*h) T(d)<--------T^2(d) <-------------- T(c) <---------------- T^2(c) <------- T(b) <----------- a
|
|
|
981
|
|
|
982
|
|
|
983 μ(d) μ(d)T T^2(g) T(f) h
|
|
|
984 (g*f)*h T(d)<--------T^2(d) <---------------T^3(d) <-------------- T^2(c) <------- T(b) <----------- a
|
|
|
985
|
|
|
986
|
|
|
987 μ(d) Tμ(d) T^2(g) T(f) h
|
|
|
988 (g*f)*h T(d)<--------T^2(d) <---------------T^3(d) <-------------- T^2(c) <------- T(b) <----------- a
|
|
|
989
|
|
|
990
|
|
|
991 μ(d) T(g) f
|
|
|
992 (g*f) _ T(d) <---------------T^2(d) <-------------- T(c) <----------- b _
|
|
|
993
|
|
|
994
|
|
|
995
|
|
|
996
|
|
|
997 Tμ(d) T^2(g)
|
|
|
998 T^2(d)<-----------T^2(T(d))<-------- T^2(c)
|
|
|
999 | | |
|
|
|
1000 | | |
|
|
|
1001 μ(d)| |μ(T(d)) |μ(c)
|
|
|
1002 | | |
|
|
|
1003 v μ(d) v T(g) v
|
|
|
1004 T(d) <----------- T(T(d)) <---------- T(c)
|
|
|
1005
|
|
|
1006
|
|
|
1007
|
|
31
|
1008 ----end-comment:
|
|
0
|
1009
|
|
|
1010 \begin{tikzcd}
|
|
|
1011 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{} \\
|
|
|
1012 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{} \\
|
|
|
1013 (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{} \\
|
|
|
1014 (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{} \\
|
|
|
1015 g*f & T(d) \arrow[leftarrow]{r}{μ(d)} & T^2(d) \arrow[leftarrow]{r}{T(g)} & T(c) \arrow[leftarrow]{r}{f} & b & \mbox{} \\
|
|
|
1016 \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{} \\
|
|
|
1017 \mbox{} & T(d) \arrow[leftarrow]{r}{μ(d)} & T(T(d)) \arrow[leftarrow]{r}{T(g)} & T(c) & \mbox{} \\
|
|
|
1018 \end{tikzcd}
|
|
|
1019
|
|
|
1020
|
|
|
1021 \begin{eqnarray*}
|
|
|
1022 g * (f * h) & = & g * (μ(c)T(f)h) \\
|
|
|
1023 \mbox{} & = & μ(d)(T(g))(μ(c)T(f)h) \\
|
|
|
1024 \mbox{} & = & μ(d) T(g)μ(c) T(f)h \\
|
|
|
1025 \\
|
|
|
1026 (g * f) * h & = & (μ(d)T(g)f) * h \\
|
|
|
1027 \mbox{} & = & μ(d)T(μ(d)T(g)f)h \\
|
|
|
1028 \mbox{} & = & μ(d) T(μ(d))T^2(g) T(f)h \\
|
|
|
1029 \end{eqnarray*}
|
|
|
1030
|
|
|
1031 $ μ(d)μ(d)T = μ(d)Tμ(d) $
|
|
|
1032
|
|
|
1033 $ μ(T(d))T^2(g) = T(g)μ(c) $ naturality of $μ$.
|
|
|
1034
|
|
|
1035 $ μ(d)Tμ(d)T^2(g) = μ(d)μ(T(d))T^2(g) = μ(d)T(g)μ(c) $
|
|
|
1036
|
|
31
|
1037 ----begin-comment:
|
|
0
|
1038
|
|
|
1039 T^2(g)
|
|
|
1040 T^3(d) <----------- T^2(c)
|
|
|
1041 | |
|
|
|
1042 |μ(T(d)) |μ(c)
|
|
|
1043 | |
|
|
|
1044 v v
|
|
|
1045 T^2(d)<------------ T(c)
|
|
|
1046 T(g)
|
|
|
1047
|
|
31
|
1048 ----end-comment:
|
|
0
|
1049
|
|
|
1050 \begin{tikzcd}
|
|
|
1051 T^3(d) \arrow[leftarrow]{r}{T^2(g)} \arrow{d}{μ(T(d))} & T^2(c) & \mbox{} \\
|
|
|
1052 T^2(d) \arrow[leftarrow]{r}[swap]{T(g)} & T(c) \arrow{u}{μ(c)} & \mbox{} \\
|
|
|
1053 \end{tikzcd}
|
|
|
1054
|
|
|
1055 $ μ(T(d)) = Tμ(d) ? $
|
|
|
1056
|
|
|
1057 $ (m,(m'm'',a)) = (mm',(m'',a))$ No, but
|
|
|
1058
|
|
|
1059 $ μμ(T(d)) = μTμ(d) $.
|
|
|
1060
|
|
|
1061
|
|
|
1062 --Ok
|
|
|
1063
|
|
|
1064 $ T(g)μ(c) = T(μ(d))T^2(g) $ であれば良いが。
|
|
|
1065
|
|
|
1066 $ μ(d)T^2(g) = T(g)μ(c) $
|
|
|
1067
|
|
|
1068 ちょっと違う。 $ μ(d) T(μ(d))T^2(g) $ が、
|
|
|
1069
|
|
|
1070 $ μ(d) μ(d)T^2(g) $
|
|
|
1071
|
|
|
1072 となると良いが。
|
|
|
1073
|
|
|
1074 $ μ(d)T(μ(d)) = μ(d)μ(T(d)) $
|
|
|
1075
|
|
|
1076
|
|
|
1077 --monoid in Kleisli category
|
|
|
1078
|
|
|
1079 $ T : a -> (m,a) $
|
|
|
1080
|
|
|
1081 $ T : f -> ((m,a)->(m,f(a))) $
|
|
|
1082
|
|
|
1083 $ μ(a) : (m,(m',a)) -> (mm',a) $
|
|
|
1084
|
|
|
1085 $ f: a -> (m,f(a)) $
|
|
|
1086
|
|
|
1087 \begin{eqnarray*}
|
|
4
|
1088 g * f (b) & = & μ(d)T(g)f(b) = μ(d)T(g)(m,f(b)) \\ & = & μ(m,(m',gf(b))) = (mm',gf(b)) \\
|
|
|
1089 (g * f) * h(a) & = & μ(d)T(μ(d)T(g)f)h(a) = μ(d)T(μ(d))(TT(g))T(f)(m,h(a)) \\
|
|
|
1090 \mbox{} & = & μ(d)T(μ(d))(TT(g))(m,(m',fh(a))) \\ & = & μ(d)T(μ(d)(m,(m',(m'',gfh(a)))) = (mm'm'',gfh(a)) \\
|
|
|
1091 g * (f * h)(a) & = & (μ(d)(T(g)))μ(c)T(f)h(a) = (μ(d)(T(g)))μ(c)T(f)(m,h(a)) \\
|
|
|
1092 \mbox{} & = & (μ(d)(T(g)))μ(c)(m,(m',fh(a))) \\ & = & μ(d)T(g)(mm',fh(a)) = (mm'm'',gfh(a)) \\
|
|
0
|
1093 \end{eqnarray*}
|
|
|
1094
|
|
|
1095
|
|
|
1096 --Resolution of Kleiseli category
|
|
|
1097
|
|
|
1098 $f : a-> b, g: b->c $
|
|
|
1099
|
|
|
1100 $ U_T : A_T -> A $
|
|
|
1101
|
|
|
1102 $ U_T(a) = T(a) $
|
|
|
1103
|
|
|
1104 $ U_T(f) = μ(b)T(f) $
|
|
|
1105
|
|
|
1106 $ g * f = μ(d)T(g)f $
|
|
|
1107
|
|
|
1108 \begin{eqnarray*}
|
|
|
1109 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} \\
|
|
|
1110 U_T(g)U_T(f) & = & μ(c)T(g)μ(b)T(f) = μ(c) μ(c) TT(g) T(f) \\
|
|
|
1111 T(g)μ(b) & = & μ(c)TT(g) \\
|
|
|
1112 \end{eqnarray*}
|
|
|
1113
|
|
|
1114
|
|
|
1115
|
|
31
|
1116 ----begin-comment:
|
|
0
|
1117
|
|
|
1118 TT(g)
|
|
|
1119 TT <--------------TT
|
|
|
1120 | |
|
|
|
1121 |μ(c) |μ(b)
|
|
|
1122 | |
|
|
|
1123 v T(g) v
|
|
|
1124 T<---------------T
|
|
|
1125
|
|
31
|
1126 ----end-comment:
|
|
0
|
1127
|
|
|
1128 \begin{tikzcd}
|
|
|
1129 TT \arrow[leftarrow]{r}{TT(g)} \arrow{d}{μ(c)} & TT \arrow{d}{μ(b)} & \mbox{} \\
|
|
|
1130 T \arrow[leftarrow]{r}{T(g)} & T & \mbox{} \\
|
|
|
1131 \end{tikzcd}
|
|
|
1132
|
|
|
1133
|
|
|
1134 $ F_T : A -> A_T $
|
|
|
1135
|
|
|
1136 $ F_T(a) = a $
|
|
|
1137
|
|
|
1138 $ F_T(f) = η(b) f $
|
|
|
1139
|
|
|
1140 $ F_T(1_a) = η(a) = 1_{F_T(a)} $
|
|
|
1141
|
|
|
1142 \begin{eqnarray*}
|
|
|
1143 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} \\
|
|
|
1144 \mbox{} & = & η(c)gf = F_T(gf)
|
|
|
1145 \end{eqnarray*}
|
|
|
1146
|
|
|
1147 $ η(c)g = T(g)η(b) $
|
|
|
1148
|
|
31
|
1149 ----begin-comment:
|
|
0
|
1150
|
|
|
1151 g
|
|
|
1152 c<---------------b
|
|
|
1153 | |
|
|
|
1154 |η(c) |η(b)
|
|
|
1155 | |
|
|
|
1156 v T(g) v
|
|
|
1157 T(b)<-------------T(b)
|
|
|
1158
|
|
31
|
1159 ----end-comment:
|
|
0
|
1160
|
|
|
1161 \begin{tikzcd}
|
|
|
1162 c \arrow[leftarrow]{r}{g} \arrow{d}{η(c)} & b \arrow{d}{η(b)} & \mbox{} \\
|
|
|
1163 T \arrow[leftarrow]{r}{T(g)} & T & \mbox{} \\
|
|
|
1164 \end{tikzcd}
|
|
|
1165
|
|
|
1166
|
|
|
1167 $ μ○Tη = 1_T = μ○ηT $ Unity law
|
|
|
1168
|
|
|
1169 \begin{eqnarray*}
|
|
|
1170 \mbox{} ε_T(a) & = & 1_{T(a)} \\
|
|
|
1171 \mbox{}\\
|
|
|
1172 \mbox{}\\
|
|
|
1173 \mbox{} U_T ε_T F_T & = & μ \\
|
|
|
1174 \mbox{}\\
|
|
|
1175 \mbox{} U_T ε_T F_Ta(a) & = & U_T ε_T (a) = U_T(1_{T(a)} = μ(a) \\
|
|
|
1176 \mbox{}\\
|
|
|
1177 \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))) \\
|
|
|
1178 \mbox{} & = & μ(T(a)) T (1_{T(a)} ) (η(T(a))η(a))) \\ & = & μ(T(a))η(T(a))η(a) \\
|
|
|
1179 \mbox{} & = & η(a) = 1_{F_T} \\
|
|
|
1180 \end{eqnarray*}
|
|
|
1181
|
|
|
1182
|
|
|
1183
|
|
|
1184 \begin{eqnarray*}
|
|
|
1185 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)} \\
|
|
|
1186 & = & 1_{T(a)} = T(1_a) = 1_{U_T} \\
|
|
|
1187 \end{eqnarray*}
|
|
|
1188
|
|
|
1189
|
|
|
1190
|
|
|
1191 ---Comparison functor $K_T$
|
|
|
1192
|
|
|
1193 Adjoint $(B,U,F,ε)$, $K_T : A_T -> B $,
|
|
|
1194
|
|
|
1195 $ g : b -> c$.
|
|
|
1196
|
|
|
1197
|
|
|
1198 \begin{eqnarray*}
|
|
|
1199 K_T(a) & = & F(a) \\
|
|
|
1200 K_T(g) & = & ε(F(c)) F(g) \\
|
|
|
1201 K_T F_T(a) & = & K_T(a) = F(a) \\
|
|
|
1202 K_T F_T(f) & = & K_T(η(b) f) \\& = & ε(F(b))F(μ(b)f) \\ & = & ε(F(b))F(μ(b))F(f) = F(f) \\
|
|
|
1203 \end{eqnarray*}
|
|
|
1204
|
|
|
1205
|
|
|
1206 \begin{eqnarray*}
|
|
|
1207 K_T (η(b)) & = & ε(F(b))F(η(b)) = 1_{F(b)} \\
|
|
|
1208 K_T (η(T(c))g) & = & ε(F(T(c)))F(η(T(c))g) = F(g) \\
|
|
|
1209 K_T (g) K_T(f) & = & ε(F(c))F(g) ε(F(b))F(f) = ε(F(c)) ε(F(c)) FUF(g) F(f) \\
|
|
|
1210 K_T (g*f) & = & ε(F(c)) F(μ(c)UF(g)f) = ε(F(c)) F(μ(c)) FUF(g) F(f) \\
|
|
|
1211 ε(F(c))FUF(g) & = & F(g) ε(F(b)) \\
|
|
|
1212 \end{eqnarray*}
|
|
|
1213
|
|
31
|
1214 ----begin-comment:
|
|
0
|
1215
|
|
|
1216 FU(F(g))
|
|
|
1217 FU(F(c))<-------------FU(F(b))
|
|
|
1218 | |
|
|
|
1219 |ε(F(c)) |ε(F(b))
|
|
|
1220 | |
|
|
|
1221 v F(g) v
|
|
|
1222 F(c)<----------------F(b)
|
|
|
1223
|
|
31
|
1224 ----end-comment:
|
|
0
|
1225
|
|
|
1226 \begin{tikzcd}
|
|
|
1227 FU(F(c)) \arrow[leftarrow]{r}{FU(F(g))} \arrow{d}{ε(F(c))} & FU(F(b)) \arrow{d}{ε(F(b))} & \mbox{} \\
|
|
|
1228 F(c) \arrow[leftarrow]{r}{F(g)} & F(b) & \mbox{} \\
|
|
|
1229 \end{tikzcd}
|
|
|
1230
|
|
|
1231 $ ε(F(c)) F(μ(c)) = ε(F(c)) ε(F(c)) $ ?
|
|
|
1232
|
|
|
1233 $ ε(F(c)) F(μ(c)) = ε(F(c)) FUε(F(c)) $
|
|
|
1234
|
|
31
|
1235 ----begin-comment:
|
|
0
|
1236
|
|
|
1237 FUε(F(c))
|
|
|
1238 FUFU(c)<---------------FUFU(F(c))
|
|
|
1239 | |
|
|
|
1240 |εF(c)) |ε(F(c))
|
|
|
1241 | |
|
|
|
1242 v ε(F(c)) v
|
|
|
1243 FU(c)<----------------FU(F(c))
|
|
|
1244
|
|
|
1245
|
|
31
|
1246 ----end-comment:
|
|
0
|
1247
|
|
|
1248 \begin{tikzcd}
|
|
|
1249 FUFU(c) \arrow[leftarrow]{r}{FUε(F(c))} \arrow{d}{εF(c))} & FUFU(F(c)) \arrow{d}{ε(F(c))} & \mbox{} \\
|
|
|
1250 FU(c) \arrow[leftarrow]{r}{ε(F(c))} & FU(F(c)) & \mbox{} \\
|
|
|
1251 \end{tikzcd}
|
|
|
1252
|
|
|
1253
|
|
|
1254
|
|
|
1255 $ UK_T(a) = UF(a) = T(a) = U_T(a) $
|
|
|
1256
|
|
|
1257 $ UK_T(g) = U(ε((F(c))F(g))) = U(ε(F(c)))UF(g) = μ(c)T(g) = U_T(g) $
|
|
|
1258
|
|
|
1259
|
|
|
1260
|
|
|
1261
|
|
|
1262
|
|
|
1263
|
|
|
1264 --Monoid
|
|
|
1265
|
|
|
1266
|
|
|
1267 $T : A -> M x A$
|
|
|
1268
|
|
|
1269 $T(a) = (m,a)$
|
|
|
1270
|
|
|
1271 $T(f) : T(A) -> T(f(A))$
|
|
|
1272
|
|
|
1273 $T(f)(m,a) = (m,f(a))$
|
|
|
1274
|
|
|
1275 $T(fg)(m,a) = (m,fg(a)) $
|
|
|
1276
|
|
|
1277 -- association of Functor
|
|
|
1278
|
|
|
1279 $T(f)T(g)(m,a) = T(f)(m,g(a)) = (m,fg(a)) = T(fg)(m,a)$
|
|
|
1280
|
|
|
1281
|
|
|
1282 $μ : T x T -> T$
|
|
|
1283
|
|
|
1284 $μ_a(T(T(a)) = μ_A((m,(m',a))) = (m*m',a) $
|
|
|
1285
|
|
|
1286 -- $TT$
|
|
|
1287
|
|
|
1288 $TT(a) = (m,(m',a))$
|
|
|
1289
|
|
|
1290 $TT(f)(m,(m',a)) = (m,(m',f(a))$
|
|
|
1291
|
|
|
1292
|
|
|
1293
|
|
|
1294 -- naturality of $μ$
|
|
|
1295
|
|
31
|
1296 ----begin-comment:
|
|
4
|
1297 μ(a)
|
|
0
|
1298 TT(a) ---------> T(a)
|
|
|
1299 | |
|
|
|
1300 TT(f)| |T(f)
|
|
|
1301 | |
|
|
4
|
1302 v μ(b) v
|
|
0
|
1303 TT(b) ---------> T(b)
|
|
31
|
1304 ----end-comment:
|
|
0
|
1305
|
|
|
1306 \begin{tikzcd}
|
|
4
|
1307 TT(a) \arrow{r}{μ(a)} \arrow{d}{TT(f)} & T(a) \arrow{d}{T(f)} \\
|
|
|
1308 TT(b) \arrow{r}{μ(b)} & T(b)
|
|
0
|
1309 \end{tikzcd}
|
|
|
1310
|
|
|
1311
|
|
4
|
1312 $ μ(b)TT(f)TT(a) = T(f)μ(a)TT(a)$
|
|
0
|
1313
|
|
4
|
1314 $ μ(b)TT(f)TT(a) = μ(b)((m,(m',f(a))) = (m*m',f(a))$
|
|
0
|
1315
|
|
4
|
1316 $ T(f)μ(a)(TT(a)) = T(f)(m*m',a) = (m*m',f(a))$
|
|
0
|
1317
|
|
|
1318 --μ○μ
|
|
|
1319
|
|
|
1320 Horizontal composition of $μ$
|
|
|
1321
|
|
|
1322 $f -> μ_TT(a)$
|
|
|
1323
|
|
|
1324 $a -> TT(a)$
|
|
|
1325
|
|
|
1326 $μ_T(a) TTT(a) = μ_T(a) (m,(m',(m'',a))) = (m*m',(m'',a)) $
|
|
|
1327
|
|
31
|
1328 ----begin-comment:
|
|
4
|
1329 μ(TTT(a))
|
|
|
1330 TTTT(a) ----------> TTT(a)
|
|
|
1331 | |
|
|
|
1332 TT(μ(T(a))| |T(μ(T(a)))
|
|
|
1333 | |
|
|
|
1334 v μ(TT(a)) v
|
|
|
1335 TTT(a) -----------> TT(a)
|
|
31
|
1336 ----end-comment:
|
|
0
|
1337
|
|
|
1338 \begin{tikzcd}
|
|
4
|
1339 TTTT(a) \arrow{r}{μ(TTT(a))} \arrow{d}[swap]{TT(μ)} & TTT(a) \arrow{d}{T(μ)} & \mbox{} \\
|
|
|
1340 TTT(a) \arrow{r}{μ(TT(a))} & TT(a) & \mbox{} \\
|
|
0
|
1341 \end{tikzcd}
|
|
|
1342
|
|
|
1343
|
|
|
1344 \begin{eqnarray*}
|
|
|
1345 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)) \\
|
|
|
1346 μ_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)) \\
|
|
|
1347 \end{eqnarray*}
|
|
|
1348
|
|
|
1349 -Horizontal composition of natural transformation
|
|
|
1350
|
|
|
1351
|
|
|
1352 --Natural transformation $ε$ and Functor $F: A->B, U:B->A$
|
|
|
1353
|
|
|
1354
|
|
|
1355 $ ε: FUFU->FU$
|
|
|
1356
|
|
|
1357 $ ε: FU->1_B$
|
|
|
1358
|
|
|
1359 Naturality of $ε$
|
|
|
1360
|
|
31
|
1361 ----begin-comment:
|
|
0
|
1362 ε(a)
|
|
|
1363 FU(a) ------> a
|
|
|
1364 FU(f)| |f
|
|
|
1365 v ε(b) v
|
|
|
1366 FU(b) ------> b ε(b)FU(f)a = fε(a)a
|
|
|
1367
|
|
|
1368 ε(FU(a))
|
|
|
1369 FUFU(a) -----------> FU(a)
|
|
|
1370 FUFU(f)| |FU(f)
|
|
|
1371 v ε(FU(b)) v
|
|
|
1372 FUFU(b) -----------> FU(b)
|
|
|
1373
|
|
|
1374 ε((FU(b))FUFU(f)FU(a) = FU(f)ε(FU(a))FU(a)
|
|
31
|
1375 ----end-comment:
|
|
0
|
1376
|
|
|
1377 \begin{tikzcd}
|
|
|
1378 FU(a) \arrow{r}{ε(a)} \arrow{d}{FU(f)} & a \arrow{d}{f} \\
|
|
|
1379 FU(b) \arrow{r}{ε(b)} & b & ε(b)FU(f)a = fε(a)a \\
|
|
|
1380 FUFU(a) \arrow{r}{ε(FU(a))} \arrow{d}{FUFU(f)}& FU(a) \arrow{d}{FU(f)} \\
|
|
|
1381 FUFU(b) \arrow{r}{ε(FU(b))} & FU(b) \\
|
|
|
1382 & & ε((FU(b))FUFU(f)FU(a) = FU(f)ε(FU(a))FU(a) \\
|
|
|
1383 \end{tikzcd}
|
|
|
1384
|
|
|
1385
|
|
|
1386 --Vertial Compositon $ε・ε$
|
|
|
1387
|
|
|
1388 $ ε・ε : FUFU -> 1B$
|
|
|
1389
|
|
31
|
1390 ----begin-comment:
|
|
0
|
1391 ε(FU(a)) ε(a)
|
|
|
1392 FUFU(a) ---------> FU(a) ------> a
|
|
|
1393 FUFU(f)| |FU(f) |f
|
|
|
1394 v ε(FU(b)) v ε(b) v
|
|
|
1395 FUFU(b) ---------> FU(b) ------> b
|
|
31
|
1396 ----end-comment:
|
|
0
|
1397
|
|
|
1398 \begin{tikzcd}
|
|
|
1399 FUFU(a) \arrow{r}{ε(FU(a))} \arrow{d}{FUFU(f)} & FU(a) \arrow{r}{ε(a)}\arrow{d}{FU(f)} & a\arrow{d}{f} \\
|
|
|
1400 FUFU(b) \arrow{r}{ε(FU(b))} & FU(b) \arrow{r}{ε(b)} & b
|
|
|
1401 \end{tikzcd}
|
|
|
1402
|
|
|
1403
|
|
|
1404 --Horizontal Composition $ε○ε$
|
|
|
1405
|
|
31
|
1406 ----begin-comment:
|
|
0
|
1407 FUFU <----- FU <------ B
|
|
|
1408 FU FU
|
|
|
1409 | |
|
|
|
1410 |ε |ε
|
|
|
1411 v v
|
|
|
1412 1_B 1_B
|
|
|
1413 B <----- B <------ B
|
|
31
|
1414 ----end-comment:
|
|
0
|
1415
|
|
|
1416 \begin{tikzcd}
|
|
|
1417 FUFU \arrow[leftarrow]{rr} & & FU \arrow[leftarrow]{rr} & & B \\
|
|
|
1418 & FU \arrow{d}{ε} & & FU \arrow{d}{ε}& & \\
|
|
|
1419 & 1_B & & 1_B & & \\
|
|
|
1420 B \arrow[leftarrow]{rr} & & B \arrow[leftarrow]{rr} & & B \\
|
|
|
1421 \end{tikzcd}
|
|
|
1422
|
|
|
1423 cf. $FUFU, FU$ has objects of $B$.
|
|
|
1424
|
|
|
1425 $ ε○ε : FUFU -> 1_B 1_B$
|
|
|
1426
|
|
31
|
1427 ----begin-comment:
|
|
0
|
1428 εFU(b)
|
|
|
1429 FUFU(b) ------------> 1_AFU(b)
|
|
|
1430 | |
|
|
|
1431 |FUε(b) |1_aε(b)
|
|
|
1432 | |
|
|
|
1433 v ε(b) v
|
|
|
1434 FU1_B(b) ------------> 1_B1_B(b)
|
|
|
1435
|
|
31
|
1436 ----end-comment:
|
|
0
|
1437
|
|
|
1438 \begin{tikzcd}
|
|
|
1439 FUFU(b) \arrow{r}{εFU(b)} \arrow{d}{FUε(b)} & 1_A \arrow{d}{1_aε(b)} & \mbox{} \\
|
|
|
1440 FU1_B(b) \arrow{r}{ε(b)} & 1_B & \mbox{} \\
|
|
|
1441 \end{tikzcd}
|
|
|
1442
|
|
|
1443 that is
|
|
|
1444
|
|
31
|
1445 ----begin-comment:
|
|
0
|
1446 εFU(b)
|
|
|
1447 FUFU(b) ------------> FU(b)
|
|
|
1448 | |
|
|
|
1449 |FUε(b) |ε(b)
|
|
|
1450 | |
|
|
|
1451 v ε(b) v
|
|
|
1452 FU(b) ------------> b
|
|
31
|
1453 ----end-comment:
|
|
0
|
1454
|
|
|
1455 \begin{tikzcd}
|
|
|
1456 FUFU(b) \arrow{r}{εFU(b)} \arrow{d}{FUε(b)} & FU(b) \arrow{d}{ε(b)} & \mbox{} \\
|
|
|
1457 FU(b) \arrow{r}{ε(b)} & b & \mbox{} \\
|
|
|
1458 \end{tikzcd}
|
|
|
1459
|
|
|
1460
|
|
|
1461 $ε(b) : b -> ε(b)$ arrow of $B$
|
|
|
1462
|
|
|
1463 $ ε: FU -> 1_B$
|
|
|
1464
|
|
|
1465 $ ε(b) : FU(b) -> b$
|
|
|
1466
|
|
31
|
1467 ----begin-comment:
|
|
0
|
1468 U F ε(b)
|
|
|
1469 b ----> U(b) ----> FU(b) -------> b
|
|
31
|
1470 ----end-comment:
|
|
0
|
1471
|
|
|
1472 \begin{tikzcd}
|
|
|
1473 b \arrow{r}{U} & U(b) \arrow{r}{F} & FU(b) \arrow{r}{ε(b)} & b & \mbox{} \\
|
|
|
1474 \end{tikzcd}
|
|
|
1475
|
|
|
1476 replace $f$ by $ε(b)$, $a$ by $FU(b)$ in naturality $ε(b)FU(f)a = fε(a)a$
|
|
|
1477
|
|
|
1478 $ ε(b)FU(ε(b))FU(b) = εε(FU(b))FU(b)$
|
|
|
1479
|
|
|
1480 remove $FU(b)$ on right,
|
|
|
1481
|
|
|
1482 $ ε(b)FU(ε(b)) = ε(b)ε(FU(b))$
|
|
|
1483
|
|
|
1484 this shows commutativity of previous diagram
|
|
|
1485
|
|
|
1486 $ ε(b)ε(FU(b)) = ε(b)FU(ε(b))$
|
|
|
1487
|
|
|
1488 that is
|
|
|
1489
|
|
|
1490 $ εεFU = εFUε$
|
|
|
1491
|
|
|
1492
|
|
|
1493
|
|
|
1494 --Yoneda Functor
|
|
|
1495
|
|
|
1496
|
|
|
1497 $ Y: A -> Sets^{A^{op}} $
|
|
|
1498
|
|
|
1499 $ Hom_A : A^{op} \times A -> Sets $
|
|
|
1500
|
|
|
1501 $ g:a'->a, h:b->b' $
|
|
|
1502
|
|
|
1503 $ Hom_A((g,h)) : Home_A(a,b) -> \{hfg | f \in Home_A(a,b) \} $
|
|
|
1504
|
|
|
1505 $ Hom_A((g,h)○(g',h') : Home_A(a,b) -> \{hh'fgg' | f \in Home_A(a,b) \} $
|
|
|
1506
|
|
|
1507 $ 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) \} $
|
|
|
1508
|
|
31
|
1509 ----begin-comment:
|
|
0
|
1510
|
|
|
1511 g' g
|
|
|
1512 a -----> a' -----> a''
|
|
|
1513 | |
|
|
|
1514 | |f
|
|
|
1515 h' v h v
|
|
|
1516 b<-------b' <----- b''
|
|
|
1517
|
|
31
|
1518 ----end-comment:
|
|
0
|
1519
|
|
|
1520 \begin{tikzcd}
|
|
|
1521 a \arrow{r}{g'} & a' \arrow{r}{g} \arrow{d}{} & a'' \arrow{d}{f} & \mbox{} \\
|
|
|
1522 b \arrow[leftarrow]{r}{h'} & b' \arrow[leftarrow]{r}{h} & b'' & \mbox{} \\
|
|
|
1523 \end{tikzcd}
|
|
|
1524
|
|
|
1525 $ Hom^*_A : A^{op} -> Sets^{A} $
|
|
|
1526
|
|
|
1527 $ f^{op}: a->c ( f : c->a ) $
|
|
|
1528
|
|
|
1529 $ g^{op}: c->d ( g : d->c ) $
|
|
|
1530
|
|
|
1531 $ Home^*_A(a) : a -> λ b . Hom_A(a,b) $
|
|
|
1532
|
|
|
1533 $ Home^*_A(f^{op}) : (a -> λ b . Hom_A(a,b)) -> (c -> λ b . Hom_A(f(c),b)) $
|
|
|
1534
|
|
|
1535 $ Home^*_A(g^{op}f^{op}) : (a -> λ b . Hom_A(a,b)) -> (d -> λ b . Hom_A(fg(d),b)) $
|
|
|
1536
|
|
|
1537 $ 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)) $
|
|
|
1538
|
|
|
1539
|
|
|
1540 $ Hom^*_{A^{op}} : A -> Sets^{A^{op}} $
|
|
|
1541
|
|
|
1542 $ f : c->b $
|
|
|
1543 $ g : d->c $
|
|
|
1544
|
|
|
1545 $ Home^*_{A^{op}}(b) : b -> λ a . Hom_{A^{op}}(a,b) $
|
|
|
1546
|
|
|
1547 $ Home^*_{A^{op}}(f) : (b -> λ a . Hom_{A^{op}}(a,b)) -> (c -> λ a . Hom_{A^{op}}(a,f(c))) $
|
|
|
1548
|
|
|
1549 $ Home^*_{A^{op}}(gf) : (b -> λ a . Hom_{A^{op}}(a,b)) -> (d -> λ a . Hom_{A^{op}}(a,gf(d))) $
|
|
|
1550
|
|
|
1551 $ 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))) $
|
|
|
1552
|
|
|
1553
|
|
|
1554 Arrows in $ Set^{A^{op}} $?
|
|
|
1555
|
|
|
1556 $ f: b->c = (b -> λ a . Hom_{A^{op}}(a,b)) -> (c -> λ a . Hom_{A^{op}}(a,f(c))) $
|
|
|
1557
|
|
|
1558 $ Set^{A^{op}} : A^{op} -> Set $
|
|
|
1559
|
|
|
1560 an object $ b = λ a . Hom_{A^{op}}(a,b) $ is a functor from $A^{op}$ to $ Set $.
|
|
|
1561
|
|
|
1562 $ t: (λ a . Hom_{A^{op}}(a,b)) -> (λ a . Hom_{A^{op}}(a,t(c))) $ should be a natural transformatin.
|
|
|
1563
|
|
|
1564 $ f^{op}: (b : A^{op}) -> (c : A^{op} ) = f : c->b $
|
|
|
1565
|
|
|
1566
|
|
31
|
1567 ----begin-comment:
|
|
0
|
1568
|
|
|
1569 t(c)
|
|
|
1570 Hom_{A^{op}}(a,c) ------------------------->Hom_{A^{op}}(a,t(c))
|
|
|
1571 | ^
|
|
|
1572 | |
|
|
|
1573 |Home^*{A^{op}}(a,f) |Home^*{A^{op}}(a,f)
|
|
|
1574 | |
|
|
|
1575 v t(b) |
|
|
|
1576 Hom_{A^{op}}(a,b) ------------------------->Hom_{A^{op}}(a,t(b))
|
|
|
1577
|
|
|
1578
|
|
|
1579
|
|
31
|
1580 ----end-comment:
|
|
0
|
1581
|
|
|
1582 \begin{tikzcd}
|
|
|
1583 Hom_{A^{op}}(a,c) \arrow{r}{t(c)} \arrow{d}{Home^*{A^{op}}(a,f)} & Hom_{A^{op}}(a,t(c)) & \mbox{} \\
|
|
|
1584 Hom_{A^{op}}(a,b) \arrow{r}{t(b)} & Hom_{A^{op}}(a,t(b)) \arrow{u}[swap]{Home^*{A^{op}}(a,f)} & \mbox{} \\
|
|
|
1585 \end{tikzcd}
|
|
|
1586
|
|
|
1587
|
|
|
1588 ---Contravariant functor
|
|
|
1589
|
|
|
1590 $ h_a = Hom_A(-,a) $
|
|
|
1591
|
|
|
1592 $ f:b->c, Hom_A(f,1_a): Hom_A(c,a) -> Hom_A(b,a) $
|
|
|
1593
|
|
|
1594
|
|
|
1595
|
|
|
1596
|
|
|
1597
|
|
|
1598
|
|
|
1599
|
|
|
1600
|
