Mercurial > hg > Members > kono > Proof > category
annotate doc/category.ind @ 1105:3cf570d5c285
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 25 Jan 2023 10:59:28 +0900 |
| parents | 4c686e19db60 |
| children |
| rev | line source |
|---|---|
| 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 | |
|
128
276f33602700
Comparison Functor all done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
65
diff
changeset
|
1388 --Vertcial Compositon $ε・ε$ |
| 0 | 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 |