notes smash

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 \o 0)\smash (g_2 \o g_1) \arrow[r, equals]\arrow[dd,equals] &
-(f_2 \smash g_2)\o (f_1 \smash 0)\arrow[d,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] &
+(0 \o f_1)\smash (g_2 \o g_1) \arrow[r, equals]\arrow[dd,equals] &
-(f_2 \smash 0)\o (f_1 \smash g_1)\arrow[d,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
+  We will only do the case where $f_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$
+  similar (and slightly easier). First apply induction on the paths that $f_2$, $g_1$ and $g_2$
-  respect the basepoint. In this case $g_2\o0$ is definitionally equal to $0$, and the canonical
+  respect the basepoint. In this case $f_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
+  proof that $f_2\o 0\sim0$ 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.
+  $(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
-  For the underlying homotopy, take $x : A_1\smash B_1$. We apply induction on $x$.
+  $(f_2 \smash g_2)\o 0\sim0$ is also reflexivity. This means we need to fill the following square,
-  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$)
+  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$ 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(a_2),g_2(g_1(b)))\arrow[r, equals,"1"]
-      (f_2(f_1(a)),g_2(b_2))\arrow[d,equals] \\
+      \arrow[d,equals,"1"] &
-      & (f_2(a_2),g_2(b_2))\o (f_1 \smash g_1)\arrow[d,equals] \\
+      % \arrow[d,equals,"\gluer_{g_2(g_1(b))}\tr\gluer_{g_2(g_1(b_1))}\sy"] &
-      (f_2(f_1(a)),y_0) \arrow[r,equals,"1"] &
+      (f_2(a_2),g_2(g_1(b)))\arrow[d,equals,"\mapfunc{f_2\smash g_2}(\gluer\tr\gluer\sy)"] \\
-      (x_0,y_0)
+      (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}
+\begin{lem}
-There is a unit $\eta:A\pmap B\pmap A\smash B$ and counit $\epsilon : (B\pmap C)\smash B \pmap C$
+  There is a unit $\eta_{A,B}\equiv\eta:A\pmap B\pmap A\smash B$ and counit
-\end{defn}
+  $\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
+  $e$ is invertible, hence gives a pointed equivalence $$(A\pmap B\pmap C)\simeq(A\smash B\pmap 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).$$
-\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}
 \end{lem}
-\end{defn}
+\begin{proof}
-\begin{lem}
+  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}