wip 3.8

circle.tex

@@ -2746,7 +2746,7 @@ \section{The \texorpdfstring{$m$\th}{mᵗʰ} root:
 
 The first part is easy, since the product of $\bn m$ with an $n$-element set
 is an $mn$-element set.
-\begin{lemma}
+\begin{lemma} \label{lem:deg-m-on-Cyc}
   The degree $m$ function restricts to give pointed maps
   \[
     \cdg{m} : \Cyc_n \ptdto \Cyc_{mn} \quad\text{and}\quad
@@ -2796,17 +2796,16 @@ \section{The \texorpdfstring{$m$\th}{mᵗʰ} root:
 
 Why does $\cdg{m}:\Cyc_0\to\Cyc_0$
 correspond to the $m$-fold \covering we defined in \cref{def:mfoldS1cover}?
-This is encapsulated by the fact that under the equivalence $c:\Sc\to C$, the two $m$-fold covers agree in the sense that the two functions given as composites in
+Recall the equivalence $c:\Sc\to C$ from \cref{def:S1toC}.
+For the two $m$-fold covers to correspond under this equivalence
+we need an element in the identity type represented by
 \[
   \begin{tikzcd}
     \Sc\ar[r,"c"]\ar[d,"\dg{m}"'] & \Cyc_0\ar[d,"\cdg{m}"] \\
-    \Sc\ar[r,"c"] & \Cyc_0
+    \Sc\ar[r,"c"] & \Cyc_0.
   \end{tikzcd}
 \]
-are equal; we need an element in
-\[
-  \cdg{m}c\eqto_{\Sc\to\Cyc_0}c\,\dg{m}.
-\]
+That is, we need an element in $\cdg{m}c\eqto_{\Sc\to\Cyc_0}c\,\dg{m}$.
 Under the equivalence
 \[
   \ev_{\Cyc_0}:(\Sc\to\Cyc_0)\we \sum_{(X,t):\Cyc_0}\bigl((X,t)=(X,t)\bigr)
@@ -2818,20 +2817,23 @@ \section{The \texorpdfstring{$m$\th}{mᵗʰ} root:
 we must produce an element in
 \[
   \Bigl((\bn m\times\zet,\sqrt[\uproot{2}m]{\zs}),\id\times\zs^{-1}\Bigr)
-  = \bigl((\zet,\zs),\zs^{-m}\bigr).
+  \eqto \bigl((\zet,\zs),\zs^{-m}\bigr).
 \]
-Consider the equivalence  $\varphi: (\bn m\times \zet)\to\zet$ with $\varphi(k,n)=k+mn$ discussed above.
-Transport of $\sqrt[\uproot{2}m]\zs$ along $\varphi$ is exactly $\zs$.
-(I.e., $\varphi\!\sqrt[\uproot{2}m]\zs=\zs\varphi$;
-note the way we formulate this so that we don't need to talk about the inverse of $\varphi$\footnote{%
-  Of course, the inverse of $\varphi$ maps $z:\zet$ to the remainder and the integer quotient of $z$ under Euclidean division by $m$, cf.~\cref{lem:euclid-div}.}.)
+Consider the equivalence  $\varphi: (\bn m\times \zet)\we\zet$ with $\varphi(k,n)\defeq k+mn$
+also used in \cref{lem:deg-m-on-Cyc}. discussed above.
+Transport of $\sqrt[\uproot{2}m]\zs$ along $\varphi$ is exactly $\zs$,
+\ie $\varphi\!\sqrt[\uproot{2}m]\zs=\zs\varphi$.\footnote{%
+Note that we formulate this in such a way that we don't need to talk about the inverse of $\varphi$.
+Of course, the inverse of $\varphi$ maps $z:\zet$ to the remainder and the integer quotient of $z$
+under Euclidean division by $m$, cf.~\cref{lem:euclid-div}.}
 Likewise, transport of $\id\times\zs^{-1}$ along $\varphi$ is $\zs^{-m}$,
 so that $\varphi$ lifts to an element in
 $\bigl((\bn m\times\zet,\sqrt[\uproot{2}m]{\zs}), \id\times\zs^{-1}\bigr)
-= \bigl((\zet,\zs),\zs^{-m}\bigr)$.
+\eqto \bigl((\zet,\zs),\zs^{-m}\bigr)$.
 
 \begin{xca}\label{xca:pointed-maps-circle}
-Verify $\cdg{m}c\eqto_{\Sc\ptdto\Cyc_0}c\,\dg{m}$ in case all maps are taken to be pointed.
+Extend the above construction to an identification of type $\cdg{m}c\eqto_{\Sc\ptdto\Cyc_0}c\,\dg{m}$ 
+in case all these maps are taken to be pointed.
 \end{xca}
 
 So we know that the fiber of $\cdg{m}$ at an infinite cycle $(X,t)$
@@ -2842,11 +2844,11 @@ \section{The \texorpdfstring{$m$\th}{mᵗʰ} root:
 (Such an $r$ is unique if it exists.)
 Indeed, the fiber is
 \[
-  \sum_{(Y,u):\Cyc_0}\bigl((X,t) = (\bn m\times Y, \sqrt[\uproot{2}m]{u})\bigr).
+  \sum_{(Y,u):\Cyc_0}\bigl((X,t) \eqto (\bn m\times Y, \sqrt[\uproot{2}m]{u})\bigr).
 \]
 The equivalence is obtained by sending an equivalence class $Y$ of $X/m$ to
 the corresponding infinite cycle $(Y,u^m)$ together with the
-natural identification $(X,t) = (\bn m\times Y, \sqrt[\uproot{2}m]{u^m})$.
+natural identification $(X,t) \eqto (\bn m\times Y, \sqrt[\uproot{2}m]{u^m})$.
 See \cref{thm:fiber-cdg} below for a careful proof of a more general statement.
 
 The reader will no doubt have noticed that $X/m$ is a \emph{finite cycle}.
@@ -2868,10 +2870,10 @@ \section{The \texorpdfstring{$m$\th}{mᵗʰ} root:
   The type in question is nonempty since all cycles have a nonempty underlying set,
   so it suffices to prove the type is a proposition.
   So let $(X,t),(X',t')$ be cycles of order $o$, and take $x:X$ and $x':X$.
-  An identification $((X,t),x) = ((X',t'),x')$ is given by an equivalence of
-  cycles $e : (X,t)=(X',t')$ with $e(x)=x'$.
-  But evaluation at $x$ induces an equivalence
-  $\bigl((X,t)=(X',t')\bigr) \simeq X'$,
+  An identification of $((X,t),x)$ and $((X',t'),x')$ is given by an identification 
+  of cycles $e : (X,t) \eqto (X',t')$ such that $e(x)=x'$.
+  But evaluation at $x$ induces an equivalence of type
+  $\bigl((X,t) \eqto (X',t')\bigr) \equivto X'$,
   so there exists a unique $e$ with $e(x)=x'$.
 \end{proof}
 \begin{lemma}\label{lem:m-root-id}