minor

Author: Marc Bezem

fields.tex

@@ -234,8 +234,8 @@ \subsection{Concrete rings}\label{sec:concrings}
 Let $G:\AbGroup$ be an abelian group. Abbreviate the shape
 $((z\mapsto \pt_{\BB G}),\refl{\pt_{\BB G}})$ of $\grpHom(G,G)$ by $\sh$. 
 Consider the following chain of equivalences\footnote{%
-The first combines \cref{lem:isEq-pair=} and \cref{def:funext} with
-elementary path algebra. The second is composition with $\ev_{\sh_G}$
+The first is \cref{con:identity-ptd-maps} (with path inverted). 
+The second is composition with $\ev_{\sh_G}$
 from \cref{sec:center-group}, which is an equivalence since $G$ is abelian.
 The third is essentially $\abstr$ from \cref{def:abstrisfunctor}.}
 \begin{align*}
@@ -253,18 +253,18 @@ \subsection{Concrete rings}\label{sec:concrings}
 \begin{proof}
 %$\pathpair{h}{h_\pt}:\sh\eqto\sh$
 Ignoring pointing paths, we can trace a given $p:(\sh\eqto\sh)$ through 
-the chain of equivalences as
+the chain of equivalences. Abbreviating $p' \defeq \ptw(\fst(p))$ we get
 \[ 
 p \mapsto 
-\bigl(z\mapsto p(z)\bigr) \mapsto 
-\bigl(z\mapsto \ev_{\sh_G}(p(z)))\bigr)\mapsto 
-\bigl(\loops(z\mapsto \ev_{\sh_G}(p(z)))\bigr)
+\bigl(z\mapsto p'(z)\bigr) \mapsto 
+\bigl(z\mapsto \ev_{\sh_G}(p'(z)))\bigr)\mapsto 
+\bigl(\loops(z\mapsto \ev_{\sh_G}(p'(z)))\bigr)
 \]
 The goal is to prove, for any $p,q:(\sh\eqto\sh)$ and $g:\USymG$, that
 \begin{align*}
-&\bigl(\loops(z\mapsto \ev_{\sh_G}(pq(z)))\bigr)(g) = \\
-&\bigl(\loops(z\mapsto \ev_{\sh_G}(p(z)))\bigr)(g)
-\bigl(\loops(z\mapsto \ev_{\sh_G}(q(z)))\bigr)(g).
+&\bigl(\loops(z\mapsto \ev_{\sh_G}((pq)'(z)))\bigr)(g) = \\
+&\bigl(\loops(z\mapsto \ev_{\sh_G}(p'(z)))\bigr)(g)
+\bigl(\loops(z\mapsto \ev_{\sh_G}(q'(z)))\bigr)(g).
 \end{align*}
 \MB{TBD}
 \end{proof}