From 5d6598c0aeafc26b5fd4c41d70284758e657f470 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 22 Mar 2017 20:35:50 -0600 Subject: [PATCH] notes smash --- Notes/smash.tex | 214 ++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 178 insertions(+), 36 deletions(-) diff --git a/Notes/smash.tex b/Notes/smash.tex index 7c6ccee..6986787 100644 --- a/Notes/smash.tex +++ b/Notes/smash.tex @@ -16,6 +16,8 @@ \newcommand{\auxr}{\mathsf{auxr}} \newcommand{\gluel}{\mathsf{gluel}} \newcommand{\gluer}{\mathsf{gluer}} +\newcommand{\sy}{^{-1}} +\newcommand{\const}{\ensuremath{\mathbf{0}}\xspace} \begin{document} @@ -47,7 +49,11 @@ started with. In diagrams, we will denote pointed homotopies by equalities, but we always mean pointed homotopies. \item The type $A\to B$ of pointed maps from $A$ to $B$ is itself pointed, with as basepoint the - constant map $0\equiv0_{A,B}:A\to B$ which has as underlying function $\lam{a:A}b_0$. We have $0\o g \sim 0$ and $f \o 0 \sim 0$. + constant map $0\equiv0_{A,B}:A\to B$ which has as underlying function $\lam{a:A}b_0$. We have + $0\o g \sim 0$ and $f \o 0 \sim 0$. +\item A pointed equivalence is a pointed map $f : A \to B$ whose underlying map is an + equivalence. In this case, we can find a pointed map $f\sy:B\to A$ with pointed homotopies + $f\o f\sy\sim0$ and $f\sy\o f\sim0$. \end{rmk} \begin{lem} @@ -67,12 +73,31 @@ \section{Smash Product} +\begin{defn} + The smash of $A$ and $B$ is the HIT generated by the point constructor $(a,b)$ for $a:A$ and $b:B$ + and two auxilliary points $\auxl,\auxr:A\smash B$ and path constructors $\gluel_a:(a,b_0)=\auxl$ + and $\gluer_b:(a_0,b)=\auxr$ (for $a:A$ and $b:B$). $A\smash B$ is pointed with point $(a_0,b_0)$. +\end{defn} +\begin{rmk} +\item This definition of $A\smash B$ is basically the pushout of + $\bool\leftarrow A+B\to A \times B$. A more traditional definition of $A\smash B$ is the pushout + $\unit\leftarrow A\vee B\to A \times B$. Here $\vee$ denotes the wedge product, which can be + equivalently described as either the pushout $A\leftarrow \unit\to B$ or + $\unit\leftarrow \bool\to A + B$. These two definitions of $A\smash B$ are equivalent, because in + the following diagram the top-left square and the top rectangle are pushout squares, hence the + top-right square is a pushout square by applying the pushout lemma. Another application of the + pushout lemma now states that the two definitions of $A\smash B$ are equivalent. +\begin{center} +\begin{tikzcd} +\bool \arrow[r]\arrow[d] & A+B \arrow[r]\arrow[d] & \bool \arrow[d] \\ +\unit \arrow[r] & A\vee B \arrow[r]\arrow[d] & \unit \arrow[d] \\ + & A\times B \arrow[r] & A\smash B +\end{tikzcd} +\end{center} + +\end{rmk} \begin{lem}\mbox{}\label{lem:smash-general} \begin{itemize} - \item The smash of $A$ and $B$ is the HIT generated by point constructor - $({-},{-}):A\to B \to A\smash B$ and two auxilliary points $\auxl,\auxr:A\smash B$ and path - constructors $\gluel:\prd{a:A}(a,b_0)=\auxl$ and $\gluer:\prd{b:B}(a_0,b)=\auxr$ (the - constructors are given as unpointed maps). $A\smash B$ is pointed with point $(a_0,b_0)$. \item The smash is functorial: if $f:A\pmap A'$ and $g:B\pmap B'$ then $f\smash g:A\smash B\pmap A'\smash B'$. We write $A\smash g$ or $f\smash B$ if one of the functions is the identity function. @@ -101,47 +126,95 @@ f'\smash 0\arrow[dl,equals] \\ \begin{lem}\label{lem:smash-coh} Suppose that we have maps $A_1\lpmap{f_1}A_2\lpmap{f_2}A_3$ and $B_1\lpmap{g_1}B_2\lpmap{g_2}B_3$ - and suppose that either $g_1$ or $g_2$ is constant. Then there are two homotopies + and suppose that either $f_1$ or $f_2$ is constant. Then there are two homotopies $(f_2 \o f_1)\smash (g_2 \o g_1)\sim 0$, one which uses interchange and one which doesn't. These two - homotopies are equal. Specifically, the following two diagrams commute: %% TODO: reformulate + homotopies are equal. Specifically, the following two diagrams commute: \begin{center} \begin{tikzcd} -(f_2 \o f_1)\smash (g_2 \o 0) \arrow[r, equals]\arrow[dd,equals] & -(f_2 \smash g_2)\o (f_1 \smash 0)\arrow[d,equals] \\ +(f_2 \o 0)\smash (g_2 \o g_1) \arrow[r, equals]\arrow[dd,equals] & +(f_2 \smash g_2)\o (0 \smash g_1)\arrow[d,equals] \\ & (f_2 \smash g_2)\o 0\arrow[d,equals] \\ -(f_2 \o f_1)\smash 0 \arrow[r,equals] & +0\smash (g_2 \o g_1) \arrow[r,equals] & 0 \end{tikzcd} \qquad \begin{tikzcd} -(f_2 \o f_1)\smash (0 \o g_1) \arrow[r, equals]\arrow[dd,equals] & -(f_2 \smash 0)\o (f_1 \smash g_1)\arrow[d,equals] \\ +(0 \o f_1)\smash (g_2 \o g_1) \arrow[r, equals]\arrow[dd,equals] & +(0 \smash g_2)\o (f_1 \smash g_1)\arrow[d,equals] \\ & 0\o (f_1 \smash g_1)\arrow[d,equals] \\ -(f_2 \o f_1)\smash 0 \arrow[r,equals] & +0\smash (g_2 \o g_1) \arrow[r,equals] & 0 \end{tikzcd} \end{center} \end{lem} \begin{proof} - We will only do the case where $g_1\jdeq 0$, i.e. fill the diagram on the left. The other case is - similar (but slightly easier). First apply induction on the paths that $f_2$, $f_1$ and $g_2$ - respect the basepoint. In this case $g_2\o0$ is definitionally equal to $0$, and the canonical - proof that $g_2\o 0~0$ is (definitionally) equal to reflexivity. This means that the homotopy - $(f_2 \o f_1)\smash (g_2 \o 0)~(f_2 \o f_1)\smash 0$ is also equal to reflexivity. + We will only do the case where $f_1\jdeq 0$, i.e. fill the diagram on the left. The other case is + similar (and slightly easier). First apply induction on the paths that $f_2$, $g_1$ and $g_2$ + respect the basepoint. In this case $f_2\o0$ is definitionally equal to $0$, and the canonical + proof that $f_2\o 0\sim0$ is (definitionally) equal to reflexivity. This means that the homotopy + $(f_2 \o 0)\smash (g_2 \o g_1)\sim0\smash (g_2 \o g_1)$ is also equal to reflexivity, and also the + path that $f_2 \smash g_2$ respects the basepoint is reflexivity, hence the homotopy + $(f_2 \smash g_2)\o 0\sim0$ is also reflexivity. This means we need to fill the following square, + where $q$ is the proof that $0\smash f\sim 0$. +\begin{center} +\begin{tikzcd} +(f_2 \o 0)\smash (g_2 \o g_1) \arrow[r, equals,"i"]\arrow[d,equals,"1"] & +(f_2 \smash g_2)\o (0 \smash g_1)\arrow[d,equals,"(f_2\smash g_2)\o q"] \\ +0\smash (g_2 \o g_1) \arrow[r,equals,"q"] & +0 +\end{tikzcd} +\end{center} - For the underlying homotopy, take $x : A_1\smash B_1$. We apply induction on $x$. - Suppose $x\equiv(a,b)$ for $a:A_1$ and $b:B_1$. Then we have to fill the square (denote the basepoints of $A_i$ and $B_i$ by $a_i$ and $b_i$) - + For the underlying homotopy, take $x : A_1\smash B_1$ and apply induction on $x$. Suppose + $x\equiv(a,b)$ for $a:A_1$ and $b:B_1$. Then we have to fill the square (denote the basepoints of + $A_i$ and $B_i$ by $a_i$ and $b_i$ and we suppress the arguments of $\gluer$). Now + $\mapfunc{h\smash k}(\gluer_z)=\gluer_{k(z)}$, so by general groupoid laws we see that the path on + the bottom is equal to the path on the right, which means we can fill the square. \begin{center} \begin{tikzcd} - (f_2(f_1(a)),g_2(b_2))\arrow[r, equals,"1"]\arrow[dd,equals,"1"] & - (f_2(f_1(a)),g_2(b_2))\arrow[d,equals] \\ - & (f_2(a_2),g_2(b_2))\o (f_1 \smash g_1)\arrow[d,equals] \\ - (f_2(f_1(a)),y_0) \arrow[r,equals,"1"] & - (x_0,y_0) + (f_2(a_2),g_2(g_1(b)))\arrow[r, equals,"1"] + \arrow[d,equals,"1"] & + % \arrow[d,equals,"\gluer_{g_2(g_1(b))}\tr\gluer_{g_2(g_1(b_1))}\sy"] & + (f_2(a_2),g_2(g_1(b)))\arrow[d,equals,"\mapfunc{f_2\smash g_2}(\gluer\tr\gluer\sy)"] \\ + (a_3,g_2(g_1(b))) \arrow[r,equals,"\gluer\tr\gluer\sy"] & + (a_3,b_3) \end{tikzcd} \end{center} + If $x$ is either $\auxl$ or $\auxr$ it is similar but easier. For completeness, we will write down the square we have to fill in the case that $x$ is $\auxr$. + \begin{center} + \begin{tikzcd} + \auxr \arrow[r, equals,"1"] + \arrow[d,equals,"1"] & + \auxr \arrow[d,equals,"\mapfunc{f_2\smash g_2}(\gluer_{b_2}\sy)"] \\ + \auxr \arrow[r,equals,"\gluer_{g_2(b_2)}\sy"] & + (a_3,b_3) + \end{tikzcd} + \end{center} + + If $x$ varies over $\gluer_b$, we need to fill the cube below. The front and the back are the + squares we just filled, the left square is a degenerate square, and the other three squares are + the squares in the definition of $q$ and $i$ to show that they respect $\gluer_b$ (and on the + right we apply $f_2\smash g_2$ to that square). + \begin{center} + \begin{tikzcd} + & \auxr \arrow[rr, equals,"1"] \arrow[dd,equals,near start,"1"] & & + \auxr \arrow[dd,equals,"\mapfunc{f_2\smash g_2}(\gluer_{b_2}\sy)"] \\ + (f_2(a_2),g_2(g_1(b)))\arrow[rr, equals, near start, crossing over, "1"] + \arrow[dd,equals,"1"] \arrow[ur,equals] & & + (f_2(a_2),g_2(g_1(b))) \arrow[ur,equals] & \\ + & \auxr \arrow[rr,equals,near start, "\gluer_{g_2(b_2)}\sy"] & & (a_3,b_3) \\ + (a_3,g_2(g_1(b))) \arrow[rr,equals,"\gluer\tr\gluer\sy"] \arrow[ur,equals] & & + (a_3,b_3) \arrow[from=uu, equals, crossing over, very near start, "\mapfunc{f_2\smash g_2}(\gluer\tr\gluer\sy)"] \arrow[ur,equals] & + \end{tikzcd} + \end{center} + After canceling applications of + $\mapfunc{h\smash k}(\gluer_z)=\gluer_{k(z)}$ on various sides of the squares (TODO). + + + If $x$ varies over $\gluel_a$ the proof is very similar. Only in the end we need to fill the + following cube instead (TODO). + \end{proof} \begin{thm}\label{thm:smash-functor-right} @@ -224,26 +297,76 @@ are filled by (corollaries of) \autoref{lem:smash-general}. \section{Adjunction} -\begin{defn} -There is a unit $\eta:A\pmap B\pmap A\smash B$ and counit $\epsilon : (B\pmap C)\smash B \pmap C$ -\end{defn} +\begin{lem} + There is a unit $\eta_{A,B}\equiv\eta:A\pmap B\pmap A\smash B$ and counit + $\epsilon_{B,C}\equiv\epsilon : (B\pmap C)\smash B \pmap C$ which are natural in both arguments + and 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\smash C}\o \eta_{A,B}\smash B\sim\idfunc[A\smash B].$$ + +\end{lem} +\begin{proof} + We define $\eta ab=(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\sim0$. The underlying maps are homotopic, since $(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)\smash 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 + need to show that $0(b)=c_0$ which is true by reflexivity. $\epsilon$ is trivially a pointed map, + which defines the counit. + + Now we need to show that the unit and counit are natural. (TODO). + + Finally we need to show that 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_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\eta0\sim\epsilon\o0\sim0$ is equal to $p$ for $f\equiv 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 + $$\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\smash B$ that + $\epsilon(\eta\smash B(x))=x$, which we prove by induction to $x$. (TODO). + +\end{proof} \begin{defn} The function $e\jdeq e_{A,B,C}:(A\pmap B\pmap C)\pmap(A\smash B\pmap C)$ is defined as the composite $$(A\pmap B\pmap C)\lpmap{({-})\smash B}(A\smash B\pmap (B\pmap C)\smash B)\lpmap{A\smash B \pmap\epsilon}(A\smash B\pmap C)).$$ +\end{defn} \begin{lem} -$e$ has an inverse $\inv e\jdeq \inv{e}_{A,B,C}:(A\smash B\pmap C)\pmap(A\pmap B\pmap C)$ which is defined as -$$(A\smash B\pmap C)\lpmap{B\pmap({-})}((B\pmap A\smash B)\pmap (B\pmap C))\lpmap{\eta\pmap(B\pmap C)}(A\pmap B\pmap C).$$ -\begin{proof} -We do not actually use that $\inv{e}_{A,B,C}$ has this form in later proofs, we only use that $e$ is invertible (the former fact is also not formalized). Proof to do. -\end{proof} + $e$ is invertible, hence gives a pointed equivalence $$(A\pmap B\pmap C)\simeq(A\smash B\pmap C).$$ \end{lem} -\end{defn} -\begin{lem} +\begin{proof} + Define + $$\inv{e}_{A,B,C}:(A\smash B\pmap C)\lpmap{B\pmap({-})}((B\pmap A\smash B)\pmap (B\pmap + C))\lpmap{\eta\pmap(B\pmap C)}(A\pmap B\pmap C).$$ It is easy to show that $e$ and $\inv{e}$ are + inverses as unpointed maps from the unit-counit laws and naturality of $\eta$ and $\epsilon$. +\end{proof} +\begin{lem}\label{e-natural} $e$ is natural in $A$, $B$ and $C$. \end{lem} +\begin{rmk} +\item Instead of showing that $e$ is natural, we could instead show that $e^{-1}$ is natural. In + that case we need to show that the map $A\to({-}):(B\to C)\to(A\to B)\to(A\to C)$ is natural in + $A$, $B$ and $C$. This might actually be easier, since we don't need to work with any higher + inductive type to prove that. +\end{rmk} \begin{proof} \textbf{$e$ is natural in $A$}. Suppose that $f:A'\pmap A$. Then the following diagram commutes. The left square commutes by naturality of $({-})\smash B$ in the first argument and the right square commutes because composition on the left commutes with composition on the right. \begin{center} @@ -281,6 +404,25 @@ $e$ is natural in $A$, $B$ and $C$. \end{proof} +\begin{thm} + The smash product is associative: there is an equivalence $f : A \smash (B \smash C) \simeq (A \smash B) \smash C$ which is natural in $A$, $B$ and $C$. +\end{thm} +\begin{proof} + Let $\phi_X$ be the composite of the following equivalences: + \begin{align*} + A \smash (B \smash C)\to X&\simeq A \to B\smash C\to X\\ + &\simeq A \to B\to C\to X\\ + &\simeq A \smash B\to C\to X\\ + &\simeq (A \smash B)\smash C\to X. + \end{align*} + $\phi_X$ is natural in $A,B,C,X$ by repeatedly applying \autoref{e-natural}. Let + $f\defeq\phi_{A \smash (B \smash C)}(\idfunc)$ and + $f\sy\defeq\phi\sy_{(A \smash B) \smash C}(\idfunc)$. Now these maps are inverses by naturality of + $\phi$ in $X$: + $$f\sy\o f\equiv f\sy\o \phi(\idfunc)\sim \phi(f\sy\o\idfunc)\sim \phi(\phi\sy(\idfunc))\sim\idfunc.$$ + The other composition is the identity by a similar argument. Lastly, $f$ is natural in $A$, $B$ + and $C$, since $\phi_X$ is. +\end{proof} \section{Notes on the formalization}