Mercurial > hg > Members > kono > Proof > category
diff category.ind @ 31:17b8bafebad7
add universal mapping
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 22 Jul 2013 14:30:27 +0900 |
| parents | 05087d3aeac0 |
| children | e9fa5c95eff7 |
line wrap: on
line diff
--- a/category.ind Sat Jul 13 18:12:57 2013 +0900 +++ b/category.ind Mon Jul 22 14:30:27 2013 +0900 @@ -12,28 +12,28 @@ $f: a -> Ub $ ---begin-comment: - FU(b) - ・ | - ・ | - F(f) ・ | - ・ ε(b) - ・ | - ・ f* v - F(a) -----------------> b +----begin-comment: + FU(b) + ・ | + ・ | + F(f) ・ | + ・ ε(b) + ・ | + ・ f* v + F(a) -----------------> b - U(f*) - UF(a) -----------------> Ub - ^ ・ - | ・ - | ・ - η(a) ・ f - | ・ - | ・ f = U(f*)η - |・ - a + U(f*) + UF(a) -----------------> Ub + ^ ・ + | ・ + | ・ +η(a) ・ f + | ・ + | ・ f = U(f*)η + |・ + a ---end-comment: +----end-comment: \begin{tikzcd} \mbox{} & FU(b) \arrow{d}{ε(b)} \\ @@ -88,16 +88,16 @@ because of naturality of $η$ ---begin-comment: - η(a) - UF(a) <------- a UF(f)η(a) = η(b)f - | | - |UF(f) f| - v v - UF(b) <------- b - η(b) +----begin-comment: + η(a) +UF(a) <------- a UF(f)η(a) = η(b)f +| | +|UF(f) f| +v v +UF(b) <------- b + η(b) ---end-comment: +----end-comment: \begin{tikzcd} UF(a) \arrow[leftarrow]{r}{η(a)} \arrow{d}{UF(f)} & a \arrow{d}{f} & UF(f)η(a) = η(b)f \\ @@ -111,23 +111,23 @@ $ Uε○ηU = 1_U $ ---begin-comment: - F(f) ε(b) - F(a) ---------> FU(b) --------> b +----begin-comment: + F(f) ε(b) +F(a) ---------> FU(b) --------> b - UF(f) U(ε(b)) - UF(a) --------> UFU(b) --------> U(b) + UF(f) U(ε(b)) +UF(a) --------> UFU(b) --------> U(b) - η(a) UF(f) U(ε(b)) - a ---------> UF(a) --------> UFU(b) --------> U(b) + η(a) UF(f) U(ε(b)) +a ---------> UF(a) --------> UFU(b) --------> U(b) - f η(Ub) U(ε(b)) - a ---------> Ub --------> UFU(b) --------> U(b) + f η(Ub) U(ε(b)) +a ---------> Ub --------> UFU(b) --------> U(b) - η(Ub) U(ε(b)) = 1 - ∵ Uε○ηU = 1_U + η(Ub) U(ε(b)) = 1 + ∵ Uε○ηU = 1_U ---end-comment: +----end-comment: \begin{tikzcd} F(a) \arrow{r}{F(f)} & FU(b) \arrow{r}{ε(b)} & b & \\ @@ -141,34 +141,34 @@ naturality of $f:a->Ub$ ---begin-comment: +----begin-comment: - η(Ub) - Ub ---------> UF(Ub) - ^ ^ - | | - f| |UF(f) - | η(a) | - a ---------> UF(a) + η(Ub) +Ub ---------> UF(Ub) +^ ^ +| | +f| |UF(f) +| η(a) | +a ---------> UF(a) ---end-comment: +----end-comment: \begin{tikzcd} Ub \arrow{r}{η(Ub)} & UF(Ub) \\ a \arrow{u}{f} \arrow{r}{η(a)} & UF(a) \arrow{u}[swap]{UF(f)} \end{tikzcd} ---begin-comment: +----begin-comment: - UF(f) - UF(a) ------------->UF(U(b)) UF(U(b)) - ^ ^ | - | | | + UF(f) +UF(a) ------------->UF(U(b)) UF(U(b)) +^ ^ | +| | | η(a)| η(U(b))| |U(ε(U(b))) - | f | v - a --------------->U(b) U(b) +| f | v +a --------------->U(b) U(b) ---end-comment: +----end-comment: \begin{tikzcd} UF(a) \arrow{r}{UF(f)} & UF(U(b)) & UF(U(b)) \arrow{d}{U(ε(U(b)))} & \mbox{} \\ @@ -177,17 +177,17 @@ Solution of universal mapping yields naturality of $Uε○ηU = 1_U$. ---begin-comment: +----begin-comment: - F(η(a)) - UF(a) F(a) ----------> FUF(a) - ^ | - | | + F(η(a)) +UF(a) F(a) ----------> FUF(a) +^ | +| | η(a)| |ε(F(a)) - | η(a) v - a --------------->UF(a) F(a) +| η(a) v +a --------------->UF(a) F(a) ---end-comment: +----end-comment: $εF○Fη = 1_F$. @@ -209,21 +209,21 @@ \[ ε : FU -> 1_B \] \[ ε(b) = (1_{U(b)})* \] ---begin-comment: - f* - F(a) -----------------> b +----begin-comment: + f* + F(a) -----------------> b - U(f*) - UF(a) -----------------> Ub - ^ ・ - | ・ - | ・ - η(a) ・ f - | ・ - | ・ f = U(f*)η - |・ - a ---end-comment: + U(f*) + UF(a) -----------------> Ub + ^ ・ + | ・ + | ・ +η(a) ・ f + | ・ + | ・ f = U(f*)η + |・ + a +----end-comment: \begin{tikzcd} F(a) \arrow{r}{f*} & b \\ @@ -252,28 +252,28 @@ definition of $ε$ \[ ε(b) = (1_{U(b)})* \] ---begin-comment: +----begin-comment: - FU(f*) - FUF(a)------------->FU(b) - ^| | - ||ε(F(a)) | - F(η(a))|| |ε(b)=(1_U(b))* - || (η(Ub)f)*=F(f) | - |v v - F(a) --------------->b - f* - UF(f) - UF(a)------------->UFU(b) - ^ ^| - | U(f*) || - η(a)| η(U(b))||U(ε(b)) - | || - | |v - a --------------->U(b) - f + FU(f*) + FUF(a)------------->FU(b) + ^| | + ||ε(F(a)) | +F(η(a))|| |ε(b)=(1_U(b))* + || (η(Ub)f)*=F(f) | + |v v + F(a) --------------->b + f* + UF(f) + UF(a)------------->UFU(b) + ^ ^| + | U(f*) || + η(a)| η(U(b))||U(ε(b)) + | || + | |v + a --------------->U(b) + f ---end-comment: +----end-comment: \begin{tikzcd} FUF(a) \arrow{r}{FU(f*)} \arrow{d}{ε(F(a))} & FU(b) \arrow{d}{ε(b)=(1_U(b))*} & \mbox{} \\ @@ -288,19 +288,19 @@ $ ε(F(a)) = (1_{UF(a)})* $ ---begin-comment: +----begin-comment: - F(η(a)) - UF(a) F(a) --------------> FUF(a) - ^ |^ - | || - η(a)| U(1_{F(a)}) 1_{F(a)} ε(F(a))||F(η(a)) - | || - | v| - a ---------------> U(F(a)) F(a) - η(a) + F(η(a)) +UF(a) F(a) --------------> FUF(a) + ^ |^ + | || +η(a)| U(1_{F(a)}) 1_{F(a)} ε(F(a))||F(η(a)) + | || + | v| + a ---------------> U(F(a)) F(a) + η(a) ---end-comment: +----end-comment: \begin{tikzcd} UF(a) \arrow{rd}{U(1_{F(a)}) } & F(a) \arrow{r}{F(η(a))} \arrow{rd}[swap]{1_{F(a)}} & FUF(a) \arrow{d}[swap]{ε(F(a))} & \mbox{} \\ @@ -321,10 +321,10 @@ show $F(fg) = F(f)F(g)$ ---begin-comment: - g f - a -----> Ub ----> UUc ---end-comment: +----begin-comment: + g f +a -----> Ub ----> UUc +----end-comment: \begin{tikzcd} a \arrow{r}{g} & Ub \arrow{r}{f} & UUc @@ -349,28 +349,28 @@ \end{eqnarray*} \mbox{Q.E.D.} ---begin-comment: - FU(f) - FU(b) -------------> FUU(c) - ・ | | - ・ | | - F(g) ・ | | - ・ ε(b) ε(Uc) | - ・ | | - ・ g* v f* v - F(a) -----------------> b ---------------> c +----begin-comment: + FU(f) + FU(b) -------------> FUU(c) + ・ | | + ・ | | + F(g) ・ | | + ・ ε(b) ε(Uc) | + ・ | | + ・ g* v f* v + F(a) -----------------> b ---------------> c - U(F(f)) - UF(a) UFUb - ^ ・ ^ ・ - | ・ | ・ - | ・ | ・ - η(a) ・ UFg | ・ UFf - | ・ η(Ub) ・ - | ・ | ・ - | g ・ | f ・ - a -----------------> Ub ---------------> UU(c) ---end-comment: + U(F(f)) + UF(a) UFUb + ^ ・ ^ ・ + | ・ | ・ + | ・ | ・ +η(a) ・ UFg | ・ UFf + | ・ η(Ub) ・ + | ・ | ・ + | g ・ | f ・ + a -----------------> Ub ---------------> UU(c) +----end-comment: \begin{tikzcd} @@ -385,17 +385,17 @@ $ η: 1->UB $ ---begin-comment: +----begin-comment: - UF(a)-----------------> UFb - ^ UF(f) ^ - | | - | | - η(a) η(b) - | | - | f | - a -----------------> b ---end-comment: + UF(a)-----------------> UFb + ^ UF(f) ^ + | | + | | +η(a) η(b) + | | + | f | + a -----------------> b +----end-comment: \begin{tikzcd} UF(a) \arrow{r}[swap]{UF(f)} & UFb \\ @@ -426,16 +426,16 @@ $ U(ε(b))η(U(b))U(b) = U(b)$ ---begin-comment: - FU(f) - FU(b) -------------> FU(c) - | | - | | - ε(b) | ε(c) - | | - v f v - b ---------------> c ---end-comment: +----begin-comment: + FU(f) +FU(b) -------------> FU(c) + | | + | | +ε(b) | ε(c) + | | + v f v + b ---------------> c +----end-comment: \begin{tikzcd} FU(b) \arrow{r}{FU(f)} \arrow{d}{ε(b)} & FU(c) \arrow{d}{ε(c)}\\ @@ -447,28 +447,28 @@ \[ f = Ub -> Uc \] ---begin-comment: +----begin-comment: - FU(f) (1_U(c))* - F(Ub) --------------> FU(c) ---------------> c + FU(f) (1_U(c))* + F(Ub) --------------> FU(c) ---------------> c - (1_U(b))* f - F(Ub) ----------------> b -----------------> c + (1_U(b))* f + F(Ub) ----------------> b -----------------> c - U(1_U(b)*) U(f) - UF(Ub) ----------------> Ub -----------------> U(c) - || ・ || - || ・ || - || UFU(f) ・ U(1_U(c)*) || - UF(Ub) ----- ・ ------> UFUc ---------------> U(c) - ^ ・ ^ || - | ・ | || - η(Ub) ・ 1_Ub η(Uc) | || - |・ | 1_Uc || - Ub ------------------> Uc -----------------> U(c) - U(f) + U(1_U(b)*) U(f) + UF(Ub) ----------------> Ub -----------------> U(c) + || ・ || + || ・ || + || UFU(f) ・ U(1_U(c)*) || + UF(Ub) ----- ・ ------> UFUc ---------------> U(c) + ^ ・ ^ || + | ・ | || +η(Ub) ・ 1_Ub η(Uc) | || + |・ | 1_Uc || + Ub ------------------> Uc -----------------> U(c) + U(f) ---end-comment: +----end-comment: \begin{tikzcd} F(Ub) \arrow{r}{(1_{U(b)})*} & b \arrow{r}{f} & c \\ @@ -478,7 +478,7 @@ F(Ub) \arrow{r}{FU(f)} & FU(c) \arrow{r}{(1_{U(c)})*} & c \\ \end{tikzcd} ---begin-comment: +----begin-comment: \begin{tikzcd} \mbox{} & Ub \arrow{r}{U(f)} & U(c) \\ @@ -493,7 +493,7 @@ Ub \arrow{r}{U(f)} \arrow{u}{1_Ub} \arrow[bend left]{uu}{η(Ub)} & Uc \arrow{u}[swap]{1_Uc} \arrow[bend right]{uu}[swap]{η(Uc)} \end{tikzcd} ---end-comment: +----end-comment: show $ε(c)FU(f)$ and $fε(b)$ are both solution of $(1_{Uc})U(f) ( = U(f)(1_{Ub}))$ @@ -522,15 +522,15 @@ end of proof. ---begin-comment: - U(f*) - c U(c) <- ----------- U(b) b - ^ ^| |^ ^ - | U(ε(c))||η(U(c)) η(U(b))||U(ε(b)) | - |ε(c) || || ε(b)| - | |v UFU(f) v| | - FU(c) UFU(c) <----------- UFU(b) FU(b) ---end-comment: +----begin-comment: + U(f*) +c U(c) <- ----------- U(b) b +^ ^| |^ ^ +| U(ε(c))||η(U(c)) η(U(b))||U(ε(b)) | +|ε(c) || || ε(b)| +| |v UFU(f) v| | +FU(c) UFU(c) <----------- UFU(b) FU(b) +----end-comment: \begin{tikzcd} c \arrow[bend left,leftarrow]{rrr}{f} @@ -579,17 +579,17 @@ \[ ε(F(a))Fη(a) = 1_F(a) \] ---begin-comment: +----begin-comment: - F U - UF(a) --------> FUF(a) ----------> UFUF(a) FUF(a) - ^ ^| |^ ^| - | || || || - |η(a) F(η(a))||ε(F(a)) U(εF(a))||η(UF(a)) ||ε(F(a)) - | || || || - | F |v U v| |v - a ------------> F(a) ------------> UF(a) F(a) ---end-comment: + F U +UF(a) --------> FUF(a) ----------> UFUF(a) FUF(a) +^ ^| |^ ^| +| || || || +|η(a) F(η(a))||ε(F(a)) U(εF(a))||η(UF(a)) ||ε(F(a)) +| || || || +| F |v U v| |v +a ------------> F(a) ------------> UF(a) F(a) +----end-comment: \begin{tikzcd} @@ -603,7 +603,7 @@ a \arrow{r}{F} \arrow{u}[swap]{η(a)} & F(a) \arrow{r}{U} \arrow[bend left]{u}{F(η(a))} & UF(a) \arrow[bend right]{u}[swap]{η(UF(a))} & F(a) \arrow{u}{} & \mbox{} \\ \end{tikzcd} ---begin-comment: +----begin-comment: UUF(a) ^ | @@ -611,7 +611,7 @@ η(UF(a))| |U(ε(Fa)) U(ε(F(a))η(UF(a)) = 1_UF(a) | v ε(F(a) = (1_UF(a))* UF(a) ---end-comment: +----end-comment: \begin{tikzcd} UUF(a) \arrow[bend left]{d}{U(ε(Fa))} \\ @@ -621,13 +621,13 @@ $ ε(F(a)) = (1_UF(a))* $ ---begin-comment: +----begin-comment: FA -------->UFA | | | Fη(A) | UFηA v v FUFA ------>UFUFA ---end-comment: +----end-comment: \begin{tikzcd} FA \arrow{r} \arrow{d}{Fη(A)} & UFA \arrow{d}{UFηA} \\ @@ -655,7 +655,7 @@ --おまけ $ εF○Fη=1_F, Uε○ηU = 1_U $ ---begin-comment: +----begin-comment: U UFU(a) <--------------- FU(a) @@ -673,7 +673,7 @@ F(a) <---------------- (a) F ---end-comment: +----end-comment: \begin{tikzcd} UFU(a) \arrow[leftarrow]{r}{U} \arrow[bend left]{d}{U(ε(a))} & FU(a) \arrow{d}{ε(a)} & \mbox{} \\ @@ -686,7 +686,7 @@ なら、 $ FU(ε(F(a))) = εF(a) $ ? ---begin-comment: +----begin-comment: U UFU(F(a)) <--------------- FU(F(a)) ^| | @@ -710,7 +710,7 @@ |v | F(a) <---------------- (a) F ---end-comment: +----end-comment: \begin{tikzcd} UFU(F(a)) \arrow[leftarrow]{r}{U} \arrow[bend left]{d}{U(ε(F(a)))} & FU(F(a)) \arrow{d}{ε(F(a))} & \mbox{} \\ @@ -735,7 +735,7 @@ $ μ○μT = μ○Tμ $ association law ---begin-comment: +----begin-comment: Tη μT T ---------> T^2 T^3---------> T^2 |・ | | | @@ -745,7 +745,7 @@ v ・ v v v T^2 -------> T T^2 --------> T μ μ ---end-comment: +----end-comment: \begin{tikzcd} T \arrow{r}{Tη} \arrow{d}[swap]{ηT} \arrow{rd}{1_T} & T^2 \arrow{d}{μ} & T^3 \arrow{r}{μT} \arrow{d}[swap]{Tμ}& T^2 \arrow{d}{μ} & \mbox{} \\ @@ -772,7 +772,7 @@ & = & U(ε(F(b))F(η(b))) = U(1_F) \\ \end{eqnarray*} ---begin-comment: +----begin-comment: UεFUF εFUF ε(a) UFUFUF-------> UFUF FUFUF-------> FUF FU(a)---------->a @@ -784,7 +784,7 @@ UFUF --------> UF FUF --------> F FU(b)---------> b UεF εF ε(b) ---end-comment: +----end-comment: \begin{tikzcd} UFUFUF \arrow{r}{UεFUF} \arrow{d}[swap]{UFUεF} & UFUF \arrow{d}{UεF} & FUFUF \arrow{r}{εFUF} \arrow{d}[swap]{FUεF} & FUF \arrow{d}{εF} & FU(a) \arrow{r}{ε(a)} \arrow{d}[swap]{FU(f)} & a \arrow{d}[swap]{f} & \mbox{} \\ @@ -813,7 +813,7 @@ UεF○FUUεF & = UεF○UεFFU \\ \end{eqnarray*} ---begin-comment: +----begin-comment: FU(ε(F(a))) FUF(a) <-------------FUFUF(a) @@ -824,7 +824,7 @@ F(a) <------------- FUF(a) ε(F(a)) ---end-comment: +----end-comment: \begin{tikzcd} FUF(a) \arrow[leftarrow]{r}{FU(ε(F(a)))} \arrow{d}{ε(F(a))} & FUFUF(a) \arrow{d}{ε(FUF(a))} & \mbox{} \\ @@ -844,7 +844,7 @@ $ φT(f) = fφ $ ---begin-comment: +----begin-comment: η(a) μ(a) T(f) a-----------> T(a) T^2(a)--------> T(a) T(a)---------->T(b) @@ -856,7 +856,7 @@ _ a T(a)-------->T(a) a------------> b φ f ---end-comment: +----end-comment: \begin{tikzcd} a \arrow{r}{η(a)} \arrow{rd}{1_a} & T(a) \arrow{d}{φ} & T^2(a) \arrow{r}{μ(a)} \arrow{d}[swap]{T(φ)} & T(a) \arrow{d}{φ} & T(a) \arrow{r}{T(f)} \arrow{d}[swap]{φ} & T(b) \arrow{d}{φ'} & \mbox{} \\ @@ -875,7 +875,7 @@ $φ: (m,a) -> φ(m,a) = ma $ ---begin-comment: +----begin-comment: η(a) μ(a) T(f) a----------->(1,a) (m,(m',a))-----> (mm',a) (m,a)----------->(m,f(a)) @@ -886,7 +886,7 @@ v v v v v _ 1a (m,m'a)-------->mm'a ma------------> mf(a)=f(ma) φ f ---end-comment: +----end-comment: \begin{tikzcd} a \arrow{r}{η(a)} \arrow{rd}{1_a} & (1,a) \arrow{d}{φ} & (m,(m',a)) \arrow{r}{μ(a)} \arrow{d}[swap]{T(φ)} & (mm',a) \arrow{d}{φ} & (m,a) \arrow{r}{T(f)} \arrow{d}[swap]{φ} & (m,f(a)) \arrow{d}{φ'} & \mbox{} \\ @@ -921,7 +921,7 @@ $ ηU(a,φ) = η(a), Uε(a,φ) = ε^TK^T(b) = Uε(b) $ ---begin-comment: +----begin-comment: _ Ba _ @@ -937,7 +937,7 @@ <--------- <-------- F_T U^T ---end-comment: +----end-comment: \begin{tikzcd} @@ -970,7 +970,7 @@ naturality of $μ$ ---begin-comment: +----begin-comment: μ(c) T(f) h f*h _ _ T(c) <---------------- T^2(c) <------- T(b) <----------- a @@ -1005,7 +1005,7 @@ ---end-comment: +----end-comment: \begin{tikzcd} f*h & \mbox{} & \mbox{} & T(c) \arrow[leftarrow]{r}{μ(c)} & T^2(c) \arrow[leftarrow]{r}{T(f)} & T(b) \arrow[leftarrow]{r}{h} & a & \mbox{} \\ @@ -1034,7 +1034,7 @@ $ μ(d)Tμ(d)T^2(g) = μ(d)μ(T(d))T^2(g) = μ(d)T(g)μ(c) $ ---begin-comment: +----begin-comment: T^2(g) T^3(d) <----------- T^2(c) @@ -1045,7 +1045,7 @@ T^2(d)<------------ T(c) T(g) ---end-comment: +----end-comment: \begin{tikzcd} T^3(d) \arrow[leftarrow]{r}{T^2(g)} \arrow{d}{μ(T(d))} & T^2(c) & \mbox{} \\ @@ -1113,7 +1113,7 @@ ---begin-comment: +----begin-comment: TT(g) TT <--------------TT @@ -1123,7 +1123,7 @@ v T(g) v T<---------------T ---end-comment: +----end-comment: \begin{tikzcd} TT \arrow[leftarrow]{r}{TT(g)} \arrow{d}{μ(c)} & TT \arrow{d}{μ(b)} & \mbox{} \\ @@ -1146,7 +1146,7 @@ $ η(c)g = T(g)η(b) $ ---begin-comment: +----begin-comment: g c<---------------b @@ -1156,7 +1156,7 @@ v T(g) v T(b)<-------------T(b) ---end-comment: +----end-comment: \begin{tikzcd} c \arrow[leftarrow]{r}{g} \arrow{d}{η(c)} & b \arrow{d}{η(b)} & \mbox{} \\ @@ -1211,7 +1211,7 @@ ε(F(c))FUF(g) & = & F(g) ε(F(b)) \\ \end{eqnarray*} ---begin-comment: +----begin-comment: FU(F(g)) FU(F(c))<-------------FU(F(b)) @@ -1221,7 +1221,7 @@ v F(g) v F(c)<----------------F(b) ---end-comment: +----end-comment: \begin{tikzcd} FU(F(c)) \arrow[leftarrow]{r}{FU(F(g))} \arrow{d}{ε(F(c))} & FU(F(b)) \arrow{d}{ε(F(b))} & \mbox{} \\ @@ -1232,7 +1232,7 @@ $ ε(F(c)) F(μ(c)) = ε(F(c)) FUε(F(c)) $ ---begin-comment: +----begin-comment: FUε(F(c)) FUFU(c)<---------------FUFU(F(c)) @@ -1243,7 +1243,7 @@ FU(c)<----------------FU(F(c)) ---end-comment: +----end-comment: \begin{tikzcd} FUFU(c) \arrow[leftarrow]{r}{FUε(F(c))} \arrow{d}{εF(c))} & FUFU(F(c)) \arrow{d}{ε(F(c))} & \mbox{} \\ @@ -1293,7 +1293,7 @@ -- naturality of $μ$ ---begin-comment: +----begin-comment: μ(a) TT(a) ---------> T(a) | | @@ -1301,7 +1301,7 @@ | | v μ(b) v TT(b) ---------> T(b) ---end-comment: +----end-comment: \begin{tikzcd} TT(a) \arrow{r}{μ(a)} \arrow{d}{TT(f)} & T(a) \arrow{d}{T(f)} \\ @@ -1325,7 +1325,7 @@ $μ_T(a) TTT(a) = μ_T(a) (m,(m',(m'',a))) = (m*m',(m'',a)) $ ---begin-comment: +----begin-comment: μ(TTT(a)) TTTT(a) ----------> TTT(a) | | @@ -1333,7 +1333,7 @@ | | v μ(TT(a)) v TTT(a) -----------> TT(a) ---end-comment: +----end-comment: \begin{tikzcd} TTTT(a) \arrow{r}{μ(TTT(a))} \arrow{d}[swap]{TT(μ)} & TTT(a) \arrow{d}{T(μ)} & \mbox{} \\ @@ -1358,7 +1358,7 @@ Naturality of $ε$ ---begin-comment: +----begin-comment: ε(a) FU(a) ------> a FU(f)| |f @@ -1372,7 +1372,7 @@ FUFU(b) -----------> FU(b) ε((FU(b))FUFU(f)FU(a) = FU(f)ε(FU(a))FU(a) ---end-comment: +----end-comment: \begin{tikzcd} FU(a) \arrow{r}{ε(a)} \arrow{d}{FU(f)} & a \arrow{d}{f} \\ @@ -1387,13 +1387,13 @@ $ ε・ε : FUFU -> 1B$ ---begin-comment: +----begin-comment: ε(FU(a)) ε(a) FUFU(a) ---------> FU(a) ------> a FUFU(f)| |FU(f) |f v ε(FU(b)) v ε(b) v FUFU(b) ---------> FU(b) ------> b ---end-comment: +----end-comment: \begin{tikzcd} FUFU(a) \arrow{r}{ε(FU(a))} \arrow{d}{FUFU(f)} & FU(a) \arrow{r}{ε(a)}\arrow{d}{FU(f)} & a\arrow{d}{f} \\ @@ -1403,7 +1403,7 @@ --Horizontal Composition $ε○ε$ ---begin-comment: +----begin-comment: FUFU <----- FU <------ B FU FU | | @@ -1411,7 +1411,7 @@ v v 1_B 1_B B <----- B <------ B ---end-comment: +----end-comment: \begin{tikzcd} FUFU \arrow[leftarrow]{rr} & & FU \arrow[leftarrow]{rr} & & B \\ @@ -1424,7 +1424,7 @@ $ ε○ε : FUFU -> 1_B 1_B$ ---begin-comment: +----begin-comment: εFU(b) FUFU(b) ------------> 1_AFU(b) | | @@ -1433,7 +1433,7 @@ v ε(b) v FU1_B(b) ------------> 1_B1_B(b) ---end-comment: +----end-comment: \begin{tikzcd} FUFU(b) \arrow{r}{εFU(b)} \arrow{d}{FUε(b)} & 1_A \arrow{d}{1_aε(b)} & \mbox{} \\ @@ -1442,7 +1442,7 @@ that is ---begin-comment: +----begin-comment: εFU(b) FUFU(b) ------------> FU(b) | | @@ -1450,7 +1450,7 @@ | | v ε(b) v FU(b) ------------> b ---end-comment: +----end-comment: \begin{tikzcd} FUFU(b) \arrow{r}{εFU(b)} \arrow{d}{FUε(b)} & FU(b) \arrow{d}{ε(b)} & \mbox{} \\ @@ -1464,10 +1464,10 @@ $ ε(b) : FU(b) -> b$ ---begin-comment: +----begin-comment: U F ε(b) b ----> U(b) ----> FU(b) -------> b ---end-comment: +----end-comment: \begin{tikzcd} b \arrow{r}{U} & U(b) \arrow{r}{F} & FU(b) \arrow{r}{ε(b)} & b & \mbox{} \\ @@ -1506,7 +1506,7 @@ $ Hom_A((g,h)) Hom_A((g',h')) : Home_A(a,b) -> \{h'fg' | f \in Home_A(a,b) \} -> \{hh'fgg' | f \in Home_A(a,b) \} $ ---begin-comment: +----begin-comment: g' g a -----> a' -----> a'' @@ -1515,7 +1515,7 @@ h' v h v b<-------b' <----- b'' ---end-comment: +----end-comment: \begin{tikzcd} a \arrow{r}{g'} & a' \arrow{r}{g} \arrow{d}{} & a'' \arrow{d}{f} & \mbox{} \\ @@ -1564,7 +1564,7 @@ $ f^{op}: (b : A^{op}) -> (c : A^{op} ) = f : c->b $ ---begin-comment: +----begin-comment: t(c) Hom_{A^{op}}(a,c) ------------------------->Hom_{A^{op}}(a,t(c)) @@ -1577,7 +1577,7 @@ ---end-comment: +----end-comment: \begin{tikzcd} Hom_{A^{op}}(a,c) \arrow{r}{t(c)} \arrow{d}{Home^*{A^{op}}(a,f)} & Hom_{A^{op}}(a,t(c)) & \mbox{} \\