wip prove lemmas in 12.1

Author: Marc Bezem

fields.tex

@@ -177,12 +177,12 @@ \subsection{Concrete rings}\label{sec:concrings}
 obvious first step to replace the abstract additive group by a 
 (concrete) group. Since monoids have no concrete counterpart in our set up,
 we replaced in \cref{def:altring} the multiplicative monoid 
-by the half abstract $\ell,r: : \USymR\to\Hom(R,R)$.
+by the half abstract $\ell,r:\USymR\to\Hom(R,R)$.
 
 The use of $\ell,r$ was based on the observation that, 
 for any abstract ring $\mathscr R$, left and right multiplication
-by a fixed but arbitrary element of $R$ is 
-an abstract homomorphism from the additive group $(R,0,+,-)$ of 
+by a fixed but arbitrary element of $R$ are 
+abstract homomorphisms from the additive group $(R,0,+,-)$ of 
 $\mathscr R$ to itself. 
 Even more so, the map $a\mapsto(a\cdot\blank)$ is an abstract homomorphism
 from $(R,0,+,-)$ to the abstract group $\absHom_{\ptw}(R,R)$
@@ -227,17 +227,43 @@ \subsection{Concrete rings}\label{sec:concrings}
 \begin{definition}\label{def:AbHomgroup}
 Let $G:\AbGroup$ be an abelian group. Define the abelian group $\grpHom(G,G)$
 of homomorphisms from $G$ to $G$ as the group classified
-by $\B\grpHom(G,G) \defeq ((\BG\ptdto\BB G),(z\mapsto (\BB G)_\pt))$.
+by $\B\grpHom(G,G) \defeq ((\BG\ptdto\BB G),((z\mapsto \pt_{\BB G}),\refl{}))$.
 \end{definition}
 
 The above definition of $\grpHom(G,G)$ is indeed serving its purpose:
 
 \begin{lemma}\label{lem:grpHomOK}
-Let $G:\AbGroup$ be an abelian group. Then we have an abstract isomorphism
+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}$
+from \cref{sec:center-group}, which is an equivalence since $G$ is abelian.
+The third is essentially $\abstr$ from \cref{def:abstrisfunctor}.}
+\begin{align*}
+(\sh\eqto\sh) &\equivto 
+\sum_{h:\BG_\div\to(\pt_{\BB G}\eqto\pt_{\BB G})} 
+  (\refl{\pt_{\BB G}}\eqto h(\sh_G)) \\
+              &~\jdeq \qquad \bigl(\BG\ptdto((\pt_{\BB G}\eqto\pt_{\BB G}),\refl{\pt_{\BB G}})\bigr)\\
+ &\equivto \qquad\! \bigl(\BG\ptdto\BG\bigr)\\
+% &\jdeq\qquad~\BHom(G,G)\\
+ &\equivto \qquad \absHom(\abstr(G),\abstr(G)).
+\end{align*}
+Then the composite of the above chain defines an abstract isomorphism
 from $\USym\grpHom(G,G)$ to $\absHom_{\ptw}(\abstr(G),\abstr(G))$.
 \end{lemma}
 \begin{proof}
-\MB{TBDiscussed}
+%$\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
+\[ 
+p \mapsto 
+\bigl(z\mapsto p(z)\bigr) \mapsto 
+\bigl(z\mapsto p(z)(\sh_G))\bigr)\mapsto 
+\bigl(\loops(z\mapsto p(z)(\sh_G))\bigr)
+\]
+
+\MB{TBD}
 \end{proof}
 
 \begin{definition}\label{def:ring}
@@ -306,7 +332,7 @@ \subsection{Concrete rings}\label{sec:concrings}
 For any $z:\Sc$ and $k:\zet$ we have that 
 $\B\mu(z,{\Sloop}^k)= e_z^k : (\Sc\eqto\Sc)$.
 Hence for any $j:\zet$ we have that 
-$\B\mu({\Sloop}^j,{\Sloop}^k )= e_{{\Sloop}^j}^k = s^{jk}: (\Sc\eqto\Sc)$.
+$\B\mu({\Sloop}^j,{\Sloop}^k )= e_{{\Sloop}^j}^k = s^{jk}: (\id_\Sc\eqto\id_\Sc)$.
 \MB{Almost there! Use $\ev$ to get to $\USym\ZZ$?}