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