continue notes

Notes/smash.tex

@@ -27,7 +27,7 @@
   write $A\pmap B$ for pointed maps and $A\pmap B\pmap C$ means $A\pmap (B\pmap C)$.
 \item 2-cells pointed homotopies. A pointed homotopy $h:f\sim g$ is a homotopy with a chosen 2-path
   $h(a_0) \tr g_0 = f_0$.
-\item As 3-cells (and higher cells) we take equalities between pointed homotopies.
+\item As 3-cells (or higher cells) we take equalities between 2-cells (or higher cells).
 \end{itemize}
 \end{defn}
 
@@ -36,11 +36,12 @@
   otherwise. Whenever we say that a diagram of $n$-cells commutes we mean it in the sense that there
   is an $(n+1)$-cell witnessing it.
 \item Pointed homotopies are equivalent to equalities of pointed types: $(f\sim g)\equiv (f=g)$. So
-  we could have chosen to define our 2-cells as equalities between 1-cells, but since the
-  aforementioned equivalence requires function extensionality, it is better to define the type of
-  pointed homotopies manually in a type theory where function extensionality doesn't compute (like
-  Lean). In diagrams, we will denote pointed homotopies by equalities, but we always mean pointed
-  homotopies.
+  we could have chosen to define our 2-cells as equalities between 1-cells. We choose not to, since
+  the aforementioned equivalence requires function extensionality. In a type theory where function
+  extensionality doesn't compute (like Lean) it is better to define the type of pointed homotopies
+  manually so that the underlying homotopy of a 2-cell is definitionally equal to the homotopy we
+  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$. In these
   notes we will not use $0$ for the empty type (since that is not pointed, we will not use the empty
@@ -78,33 +79,102 @@
   \end{itemize}
 \end{lem}
 
-\begin{lem}
+\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
   $(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.
-\end{lem}
-\begin{proof}
-We will only do the case where $g_1\jdeq 0$, the other case is similar (but slightly easier). In this case, we need to show that the following diagram commutes.
+  homotopies are equal. Specifically, the following two diagrams commute: %% TODO: reformulate
 \begin{center}
 \begin{tikzcd}
 (f_2 \o f_1)\smash (g_2 \o 0) \arrow[r, equals]\arrow[dd,equals] &
-(f_2 \smash g_1)\o (f_1 \o 0)\arrow[d,equals] \\
+(f_2 \smash g_1)\o (f_1 \smash 0)\arrow[d,equals] \\
 & (f_2 \smash g_1)\o 0\arrow[d,equals] \\
 (f_2 \o f_1)\smash 0 \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_1)\arrow[d,equals] \\
+(f_2 \o f_1)\smash 0 \arrow[r,equals] &
+0
+\end{tikzcd}
 \end{center}
+
+\end{lem}
+\begin{proof}
+We will only do the case where $g_1\jdeq 0$, the other case is similar (but slightly easier). In this case, we need to show that the following diagram commutes.
 Proof to do.
 \end{proof}
 
 \begin{thm}\label{thm:smash-functor-right}
-Given pointed types $A$, $A'$ and $B$, the functorial action of the smash product induces a map
-$$({-})\smash B:(A\pmap A')\pmap(A\smash B\pmap A'\smash B)$$
-which is natural in $A$, $A'$ and $B$. (note: it's both covariant and contravariant in $B$).
+Given pointed types $A$, $B$ and $C$, the functorial action of the smash product induces a map
+$$({-})\smash C:(A\pmap B)\pmap(A\smash C\pmap B\smash C)$$
+which is natural in $A$, $B$ and $C$. (note: $(A\smash C\pmap B\smash C)$ is both covariant and contravariant in $C$).
 \end{thm}
 \begin{proof}
-First note that $\lam{f}f\smash B$ preserves the basepoint so that the map is indeed pointed.
+  First note that $\lam{f}f\smash C$ preserves the basepoint so that the map is indeed pointed. We
+  show that this map is natural in each of its arguments individually, which means we need to fill
+  the following squares for $f : A' \to A$ $g:B\to B'$ and $h:C\to C'$.
+\begin{center}
+\begin{tikzcd}
+(A\pmap B) \arrow[r,"({-})\smash C"]\arrow[d,"f\pmap B"] &
+(A\smash C\pmap B\smash C)\arrow[d,"f\smash C\pmap B\smash C"] \\
+(A'\pmap B) \arrow[r,"({-})\smash C"] &
+(A'\smash C\pmap B\smash C)
+\end{tikzcd}
+\begin{tikzcd}
+(A\pmap B) \arrow[r,"({-})\smash C"]\arrow[d,"A\pmap g"] &
+(A\smash C\pmap B\smash C)\arrow[d,"A\smash C\pmap g\smash C"] \\
+(A\pmap B') \arrow[r,"({-})\smash C"] &
+(A\smash C\pmap B'\smash C)
+\end{tikzcd}
+\begin{tikzcd}[column sep=large]
+(A\pmap B) \arrow[r,"({-})\smash C"]\arrow[d,"({-})\smash C'"] &
+(A\smash C\pmap B\smash C)\arrow[d,"A\smash C\pmap B\smash h"] \\
+(A\smash C'\pmap B\smash C') \arrow[r,"A\smash h\pmap B\smash C'"] &
+(A\smash C\pmap B\smash C')
+\end{tikzcd}
+\end{center}
+Let $k:A\pmap B$. Then as homotopy the naturality in $A$ becomes
+$(k\o f)\smash C=k\smash C\o f\smash C$. To prove an equality between pointed maps, we need to give a pointed homotopy, which is given by interchange. To show that this homotopy
+is pointed, we need to fill the following square, which follows from \autoref{lem:smash-coh}.
+\begin{center}
+\begin{tikzcd}
+(0 \o f)\smash C \arrow[r, equals]\arrow[dd,equals] &
+(0 \smash C)\o (f \smash C)\arrow[d,equals] \\
+& 0 \o (f \smash C)\arrow[d,equals] \\
+0\smash C \arrow[r,equals] &
+0
+\end{tikzcd}
+\end{center}
+The naturality in $B$ is almost the same: for the underlying homotopy we need to show
+$(g \o k)\smash C = g\smash C \o k\smash C$. For the pointedness we need to fill the following
+square, which follows from \autoref{lem:smash-coh}.
+\begin{center}
+\begin{tikzcd}
+(g \o 0)\smash C \arrow[r, equals]\arrow[dd,equals] &
+(g \smash C)\o (0 \smash C)\arrow[d,equals] \\
+& (g\smash C) \o 0\arrow[d,equals] \\
+0\smash C \arrow[r,equals] &
+0
+\end{tikzcd}
+\end{center}
+The naturality in $C$ is harder. For the underlying homotopy we need to show
+$B\smash h\o g\smash C=g\smash C'\o A\smash h$. This follows by applying interchange twice:
+$$B\smash h\o g\smash C\sim(\idfunc[B]\o g)\smash(h\o\idfunc[C])\sim(g\o\idfunc[A])\smash(\idfunc[C']\o h)\sim g\smash C'\o A\smash h.$$
+To show that this homotopy is pointed, we need to fill the following square:
+% \begin{center}
+% \begin{tikzcd}
+% (B\smash h\o g\smash C) \arrow[r, equals]\arrow[dd,equals] &
+% (g \smash C)\o (0 \smash C)\arrow[d,equals] \\
+% & (g\smash C) \o 0\arrow[d,equals] \\
+% 0\smash C \arrow[r,equals] &
+% 0
+% \end{tikzcd}
+% \end{center}
+
 \end{proof}
 
 \section{Adjunction}