From ac7e75bb9ee7ce4bdaec6bc901738871652e3939 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 7 Dec 2017 13:32:11 +0100 Subject: [PATCH] continue on unit-counit --- Notes/smash.tex | 62 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 45 insertions(+), 17 deletions(-) diff --git a/Notes/smash.tex b/Notes/smash.tex index 6b585e3..47103de 100644 --- a/Notes/smash.tex +++ b/Notes/smash.tex @@ -411,20 +411,42 @@ \section{Adjunction} \begin{lem}\label{lem:unit-counit} There is a unit $\eta_{A,B}\equiv\eta:A\pmap B\pmap A\smsh B$ natural in $A$ and counit - $\epsilon_{B,C}\equiv\epsilon : (B\pmap C)\smsh B \pmap C$ dinatural in $B$ and natural in $C$. + $\epsilon_{B,C}\equiv\epsilon : (B\pmap C)\smsh B \pmap C$ dinatural in $B$ and pointed natural in $C$. These maps satisfy the unit-counit laws: $$(A\to\epsilon_{A,B})\o \eta_{A\to B,A}\sim \idfunc[A\to B]\qquad \epsilon_{B,B\smsh C}\o \eta_{A,B}\smsh B\sim\idfunc[A\smsh B].$$ \end{lem} Note: $\eta$ is also dinatural in $B$, but we don't need this. \begin{proof} - We define $\eta (a)(b)=(a,b)$. Then $\eta (a)$ respects the basepoint because - $(a,b_0)=(a_0,b_0)$. Also, $\eta$ itself respects the basepoint. To show this, we need to show - that $\eta (a_0)\sim 0$. The underlying maps are homotopic, since $(a_0,b)=(a_0,b_0)$. To show that + We define $\eta ab=(a,b)$. We define the path that $\eta a$ respects the basepoint as + $$(\eta a)_0\defeq\gluel_a\tr\gluel_{a_0}\sy:(a,b_0)=(a_0,b_0).$$ Also, $\eta$ itself respects the basepoint. To show this, we need to give $\eta_0:\eta (a_0)\sim 0$. The underlying maps are homotopic, by $$\eta_0b\defeq\gluer_b\cdot\gluer_{b_0}\sy:(a_0,b)=(a_0,b_0).$$ To show that this homotopy is pointed, we need to show that the two given proofs of $(a_0,b_0)=(a_0,b_0)$ are equal, but they are both equal to reflexivity: - $$\gluel_{a_0}\tr\gluel_{a_0}\sy=1=\gluer_{b_0}\tr\gluer_{b_0}\sy.$$ - This defines the unit. To define the counit, given $x:(B\pmap C)\smsh B$, we construct + $$\eta_{00}:\gluel_{a_0}\tr\gluel_{a_0}\sy=1=\gluer_{b_0}\tr\gluer_{b_0}\sy.$$ + This defines the unit. To show that it is natural in $A$, we need to give the following pointed homotopy $p_\eta(f)$ for $f:A\to A'$. + \begin{center} + \begin{tikzcd} + A \arrow[r,"\eta"]\arrow[d,"f"] & + (B\pmap A \smsh B)\arrow[d,"B\to f\smsh B"] \\ + A' \arrow[r,"\eta"] & + (B\pmap A'\smsh B) + \end{tikzcd} + \end{center} + We may assume that $f_0$ is reflexivity. For the underlying homotopy we need to define for $a:A$ that $p_\eta(f,a):\eta(fa)\sim f\smsh B \circ \eta a$, which is another pointed homotopy. For $b:B$ we have $\eta(fa,b)\equiv(fa,b)\equiv(f\smsh B)(\eta ab).$ + The homotopy $p_\eta(f,a)$ is pointed, since $$(f\smsh B \circ \eta a)_0=\apfunc{f\smsh B}(\gluel_a\cdot\gluel_{a_0}\sy)=\gluel_{fa}\cdot\gluel_{a_0'}\sy=(\eta(fa))_0.$$ + Now we need to show that $p_\eta(f)$ is pointed, for which we need to fill the following diagram. + \begin{center} + \begin{tikzcd} + \eta(fa_0) \arrow[equals,rr,"{p_\eta(f,a_0)}"]\arrow[dr,equals,"{\eta_0}"] & & + f\smsh B \circ \eta a_0\arrow[dl,equals,"{f\smsh B\circ\eta_0}"] \\ + & 0_{B,A'\smsh B} & + \end{tikzcd} + \end{center} + These pointed homotopies have equal underlying homotopies, since for $b:B$ we have + $$p_\eta(f,a_0,b)\cdot\apfunc{f\smsh B}(\eta_0 b)=1\cdot\apfunc{f\smsh B}(\gluer_b\cdot\gluer_{b_0}\sy)=\gluer_{b}\cdot\gluer_{b_0}\sy=\eta_0b.$$ + The homotopies are pointed in the same way (TODO). + + To define the counit, given $x:(B\pmap C)\smsh B$, we construct $\epsilon (x):C$ by induction on $x$. If $x\jdeq(f,b)$ we set $\epsilon(f,b)\defeq f(b)$. If $x$ is either $\auxl$ or $\auxr$ then we set $\epsilon (x)\defeq c_0:C$. If $x$ varies over $\gluel_f$ then we need to show that $f(b_0)=c_0$, which is true by $f_0$. If $x$ varies over $\gluer_b$ we @@ -434,24 +456,30 @@ \section{Adjunction} Now we need to show that the unit and counit are (di)natural. (TODO). Finally, we need to show the unit-counit laws. For the underlying homotopy of the first one, let - $f:A\to B$. We need to show that $p:\epsilon\o\eta f\sim f$. For the underlying homotopy of $p$, - let $a:A$, and we need to show that $\epsilon(f,a)=f(a)$, which is true by reflexivity. To show - that $p$ is a pointed homotopy, we need to show that - $p(a_0)\tr f_0=\mapfunc{\epsilon}(\eta f)_0\tr \epsilon_0$, which reduces to + $f:A\to B$. We need to show that $p_f:\epsilon\o\eta f\sim f$. We define $p_f(a)=1:\epsilon(f,a)=f(a)$. To show that $p_f$ is a pointed homotopy, we need to show that + $p_f(a_0)\tr f_0=\mapfunc{\epsilon}(\eta f)_0\tr \epsilon_0$, which reduces to $f_0=\mapfunc{\epsilon}(\gluel_f\tr\gluel_0\sy)$, but we can reduce the right hand side: (note: $0_0$ denotes the proof that $0(a_0)=b_0$, which is reflexivity) $$\mapfunc{\epsilon}(\gluel_f\tr\gluel_0\sy)=\mapfunc{\epsilon}(\gluel_f)\tr(\mapfunc{\epsilon}(\gluel_0))\sy=f_0\tr 0_0\sy=f_0.$$ Now we need to show that $p$ itself respects the basepoint of $A\to B$, i.e. that the composite - $\epsilon\o\eta(0)\sim\epsilon\o0\sim0$ is equal to $p$ for $f\equiv 0_{A,B}$. The underlying + $\epsilon\o\eta(0)\sim\epsilon\o0\sim0$ is equal to $p_{0_{A,B}}$. The underlying homotopies are the same for $a : A$; on the one side we have $\mapfunc{\epsilon}(\gluer_{a}\tr\gluer_{a_0}\sy)$ and on the other side we have reflexivity - (note: this typechecks, since $0_{A,B}a\equiv0_{A,B}a_0$). These paths are equal, since + (note: this typechecks since $0_{A,B}a\equiv0_{A,B}a_0$). These paths are equal, since $$\mapfunc{\epsilon}(\gluer_{a}\tr\gluer_{a_0}\sy)=\mapfunc{\epsilon}(\gluer_{a})\tr(\mapfunc\epsilon(\gluer_{a_0}))\sy=1\cdot1\sy\equiv1.$$ - Both pointed homotopies are pointed in the same way, which requires some path-algebra, and we skip - the proof here. - - For the underlying homotopy of the second one, we need to show for $x:A\smsh B$ that - $\epsilon(\eta\smsh B(x))=x$, which we prove by induction to $x$. (TODO). + Both pointed homotopies are pointed in the same way, which requires some path-algebra, and we skip the proof here. + + For the underlying homotopy of the second unit-counit law, we need to show for $x:A\smsh B$ that + $q(x):\epsilon((\eta\smsh B)x)=x$, which we prove by induction to $x$. If $x\equiv(a,b)$ then we can define $q(a,b)\defeq1_{(a,b)}$. If $x$ is $\auxl$ or $\auxr$ then the left-hand side reduces to $(a_0,b_0)$, so we can define $q(\auxl)\defeq\gluel_{a_0}$ and $q(\auxr)\defeq\gluer_{b_0}$. The following computation shows that $q$ respects $\gluel_a$: + $$\apfunc{\epsilon\circ\eta\smsh B}(\gluel_a)\cdot\gluel_{a_0}= \apfunc{\epsilon}(\gluel_{\eta a})\cdot\gluel_{a_0}=(\eta a)_0\cdot\gluel_{a_0}=\gluel_a\cdot\gluel_{a_0}\sy\cdot\gluel_{a_0}=\gluel_a.$$ + To show that it respects $\gluer_b$ we compute + $$\apfunc{\epsilon\circ\eta\smsh B}(\gluer_b)\cdot\gluer_{b_0}= + \apfunc{\epsilon({-},b)}(\eta_0)\cdot\apfunc{\epsilon}(\gluer_b)\cdot\gluer_{b_0}= + \apfunc{\lam{f}fb}(\eta_0)\cdot\gluer_{b_0}= + \eta_0b\cdot\gluer_{b_0}= + %\gluer_b\cdot\gluer_{b_0}\sy\cdot\gluer_{b_0}= + \gluer_b.$$ + To show that $q$ is a pointed homotopy, we need to show that $(\epsilon\circ\eta\smsh B)_0=1$, For this we compute $$(\epsilon\circ\eta\smsh B)_0=\apfunc{\epsilon({-},b_0)}(\eta_0)=\eta_0b_0=\gluer_{b_0}\cdot\gluer_{b_0}\sy=1.$$ \end{proof} \begin{defn}