290 lines
13 KiB
TeX
290 lines
13 KiB
TeX
\documentclass{article}
|
|
|
|
\input{preamble-articles}
|
|
|
|
\title{Notes on the smash product}
|
|
\date{\today}
|
|
\usepackage{fullpage}
|
|
\newcommand{\pmap}{\to}
|
|
\newcommand{\lpmap}{\xrightarrow}
|
|
\renewcommand{\smash}{\wedge}
|
|
\renewcommand{\phi}{\varphi}
|
|
\renewcommand{\epsilon}{\varepsilon}
|
|
\newcommand{\tr}{\cdot}
|
|
\renewcommand{\o}{\ensuremath{\circ}}
|
|
\newcommand{\auxl}{\mathsf{auxl}}
|
|
\newcommand{\auxr}{\mathsf{auxr}}
|
|
\newcommand{\gluel}{\mathsf{gluel}}
|
|
\newcommand{\gluer}{\mathsf{gluer}}
|
|
|
|
\begin{document}
|
|
|
|
\maketitle
|
|
|
|
\section{Pointed Types}
|
|
|
|
\begin{defn}
|
|
We work in the $(\infty,1)$-category of pointed types.
|
|
\begin{itemize}
|
|
\item The objects are pointed types $A$, types together with a basepoint $a_0:A$.
|
|
\item 1-cells are pointed maps $f:A\to B$ which are maps with a chosen path $f_0:f(a_0)=b_0$. We
|
|
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 (or higher cells) we take equalities between 2-cells (or higher cells).
|
|
\end{itemize}
|
|
\end{defn}
|
|
|
|
\begin{rmk}
|
|
\item All types, maps and homotopies in these notes are pointed, unless explicitly mentioned
|
|
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. 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$. We have $0\o g \sim 0$ and $f \o 0 \sim 0$.
|
|
\end{rmk}
|
|
|
|
\begin{lem}
|
|
Given maps $f:A'\pmap A$ and $g:B\pmap B'$. Then there are maps
|
|
$(f\pmap C):(A\pmap C)\pmap(A'\pmap C)$ and $(C\pmap g):(C\pmap B)\pmap(C\pmap B')$ given by
|
|
precomposition with $f$, resp. postcomposition with $g$. The map $\lam{g}C\pmap g$ preserves the basepoint, giving rise to a map $$(C\pmap ({-})):(B\pmap B')\pmap(C\pmap B)\pmap(C\pmap B').$$
|
|
Also, the following square commutes
|
|
\begin{center}
|
|
\begin{tikzcd}
|
|
(A\pmap B) \arrow[r,"A\pmap g"]\arrow[d,"f\pmap B"] & (A\pmap B')\arrow[d,"f\pmap B'"] \\
|
|
(A'\pmap B) \arrow[r,"A'\pmap g"] & (A'\pmap B')
|
|
\end{tikzcd}
|
|
\end{center}
|
|
|
|
\end{lem}
|
|
|
|
|
|
\section{Smash Product}
|
|
|
|
\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.
|
|
\item Smash preserves composition, which gives rise to the interchange law:
|
|
$i:(f' \o f)\smash (g' \o g) \sim f' \smash g' \o f \smash g$
|
|
\item If $p:f\sim f'$ and $q:g\sim g'$ then $p\smash q:f\smash g\sim f'\smash g'$. This operation
|
|
preserves reflexivities, symmetries and transitivies.
|
|
\item There are homotopies $f\smash0\sim0$ and $0\smash g\sim 0$ such that the following diagrams
|
|
commute for given homotopies $p : f\sim f'$ and $q : g\sim g'$.
|
|
\begin{center}
|
|
\begin{tikzcd}
|
|
f\smash 0 \arrow[rr, equals,"p\smash1"]\arrow[dr,equals] & &
|
|
f'\smash 0\arrow[dl,equals] \\
|
|
& 0 &
|
|
\end{tikzcd}
|
|
\qquad
|
|
\begin{tikzcd}
|
|
0\smash g\arrow[rr, equals,"1\smash q"]\arrow[dr,equals] & &
|
|
0\smash g'\arrow[dl,equals] \\
|
|
& 0 &
|
|
\end{tikzcd}
|
|
\end{center}
|
|
|
|
\end{itemize}
|
|
\end{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. 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_2)\o (f_1 \smash 0)\arrow[d,equals] \\
|
|
& (f_2 \smash g_2)\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$, 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.
|
|
|
|
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$)
|
|
|
|
\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)
|
|
\end{tikzcd}
|
|
\end{center}
|
|
\end{proof}
|
|
|
|
\begin{thm}\label{thm:smash-functor-right}
|
|
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 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 (after reducing out the applications of function extensinality), 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 a bit harder. For the underlying homotopy we need to show
|
|
$B\smash h\o k\smash C=k\smash C'\o A\smash h$. This follows by applying interchange twice:
|
|
$$B\smash h\o k\smash C\sim(\idfunc[B]\o k)\smash(h\o\idfunc[C])\sim(k\o\idfunc[A])\smash(\idfunc[C']\o h)\sim k\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 0\smash C \arrow[r, equals]\arrow[d,equals] &
|
|
(\idfunc[B]\o 0)\smash(h\o\idfunc[C]) \arrow[r, equals]\arrow[d,equals] &
|
|
(0\o\idfunc[A])\smash(\idfunc[C']\o h)\arrow[r, equals]\arrow[d,equals] &
|
|
0\smash C'\o A\smash h\arrow[d,equals] \\
|
|
B\smash h\o 0 \arrow[d,equals] &
|
|
0\smash(h\o\idfunc[C]) \arrow[r, equals]\arrow[d,equals] &
|
|
0\smash(\idfunc[C']\o h) \arrow[d,equals] &
|
|
0\o A\smash h\arrow[d,equals] \\
|
|
B\smash h\o 0 \arrow[r, equals] &
|
|
0 \arrow[r, equals] &
|
|
0 \arrow[r, equals] &
|
|
0
|
|
\end{tikzcd}
|
|
\end{center}
|
|
The left and the right squares are filled by \autoref{lem:smash-coh}. The squares in the middle
|
|
are filled by (corollaries of) \autoref{lem:smash-general}.
|
|
\end{proof}
|
|
|
|
\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{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)).$$
|
|
|
|
\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}
|
|
\end{lem}
|
|
\end{defn}
|
|
\begin{lem}
|
|
$e$ is natural in $A$, $B$ and $C$.
|
|
\end{lem}
|
|
\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}
|
|
\begin{tikzcd}
|
|
(A\pmap B\pmap C) \arrow[r,"({-})\smash B"]\arrow[d,"f\pmap B\pmap C"] &
|
|
(A\smash B\pmap (B\pmap C)\smash B) \arrow[r,"A\smash B\pmap\epsilon"]\arrow[d,"f\smash B\pmap\cdots"] &
|
|
(A\smash B\pmap C)\arrow[d,"f\smash B\pmap C"] \\
|
|
(A'\pmap B\pmap C) \arrow[r,"({-})\smash B"] &
|
|
(A'\smash B\pmap (B\pmap C)\smash B) \arrow[r,"A\smash B\pmap\epsilon"] &
|
|
(A'\smash B\pmap C)
|
|
\end{tikzcd}
|
|
\end{center}
|
|
|
|
\textbf{$e$ is natural in $C$}. Suppose that $f:C\pmap C'$. Then in the following diagram the left square commutes by naturality of $({-})\smash B$ in the second argument (applied to $B\pmap f$) and the right square commutes by applying the functor $A\smash B \pmap({-})$ to the naturality of $\epsilon$ in the second argument.
|
|
\begin{center}
|
|
\begin{tikzcd}
|
|
(A\pmap B\pmap C) \arrow[r]\arrow[d] &
|
|
(A\smash B\pmap (B\pmap C)\smash B) \arrow[r]\arrow[d] &
|
|
(A\smash B\pmap C)\arrow[d] \\
|
|
(A\pmap B\pmap C') \arrow[r] &
|
|
(A\smash B\pmap (B\pmap C')\smash B) \arrow[r] &
|
|
(A\smash B\pmap C')
|
|
\end{tikzcd}
|
|
\end{center}
|
|
|
|
\textbf{$e$ is natural in $B$}. Suppose that $f:B'\pmap B$. The diagram looks weird since $({-})\smash B$ is both contravariant and covariant in $B$. Then we get the following diagram. The front square commutes by naturality of $({-})\smash B$ in the second argument (applied to $f\pmap C$). The top square commutes by naturality of $({-})\smash B$ in the third argument, the back square commutes because composition on the left commutes with composition on the right, and finally the right square commutes by applying the functor $A\smash B' \pmap({-})$ to the naturality of $\epsilon$ in the first argument.
|
|
\begin{center}
|
|
\begin{tikzcd}[row sep=scriptsize, column sep=-4em]
|
|
& (A\smash B\pmap (B\pmap C)\smash B) \arrow[rr] \arrow[dd] & & (A\smash B'\pmap (B\pmap C)\smash B)\arrow[dd] \\
|
|
(A\pmap B\pmap C) \arrow[ur] \arrow[rr, crossing over] \arrow[dd] & & (A\smash B'\pmap (B\pmap C)\smash B') \arrow[ur] \\
|
|
& (A\smash B\pmap C)\arrow[rr] & & (A\smash B'\pmap C) \\
|
|
(A\pmap B'\pmap C) \arrow[rr] & & (A\smash B'\pmap (B'\pmap C)\smash B') \arrow[ur] \arrow[from=uu, crossing over]\\
|
|
\end{tikzcd}
|
|
\end{center}
|
|
|
|
\end{proof}
|
|
|
|
|
|
\section{Notes on the formalization}
|
|
|
|
The order of arguments are different in the formalization here and there.
|
|
Also, some smashes are commuted. This is because some unfortunate choices have been made in the formalization. Reversing these choices is possible, but probably more work than it's worth (the final result is exactly the same).
|
|
|
|
\end{document}
|