wip 12.1

Author: Marc Bezem

abelian.tex

@@ -397,7 +397,7 @@ \subsection{Abelian groups and simply connected $2$-types}
 
 \begin{theorem}\label{thm:abelian-groups-weq-sc2types}%
   The type $\typeabgroup$ of abelian groups is equivalent to the type
-  of pointed simply connected $2$-types.
+  of pointed simply connected $2$-types. \MB{Give equivalences here.}
 \end{theorem}
 \begin{proof}
   Define the map $\BB : \typeabgroup \to \UUp$ by

absgroup.tex

@@ -400,7 +400,7 @@ \section{Abstract homomorphisms}\label{sec:abshom}
   for every $g:\USymG$.
 \end{example}
 
-\begin{xca}\label{xca:abshomaddition}
+\begin{xca}\label{xca:abs-homgroup}
 Let $\agp G\defequi(S,e_{\agp G},\cdot_{\agp G},\iota_{\agp G})$
 and $\agp H\defequi(T,e_{\agp H},\cdot_{\agp H},\iota_{\agp H})$
 be abstract groups and consider the set $\absHom(\agp H,\agp G)$
@@ -719,9 +719,9 @@ \section{Homomorphisms, from abstract to concrete and back}
 for all $\omega:\sh_G \eqto \sh_G$ (so that $g:\Hom(G,H)$ is a ``delooping'' of $f$, 
 that is, $f=\abstr(g)$).%
 \footnote{We will thus have displayed a map
-$\mathrm{deloop}:\absHom(\abstr(G),\abstr(H))\to\Hom(G,H)$ with 
-$({\abstr}\circ\mathrm{deloop})=\id$. We leave it to the reader 
-to prove that $\mathrm{deloop}\circ{\abstr}=\id$. }
+$\deloop:\absHom(\abstr(G),\abstr(H))\to\Hom(G,H)$ with 
+$({\abstr}\circ\deloop)=\id$. We leave it to the reader 
+to prove that $\deloop\circ{\abstr}=\id$. }
 
 To get an idea of our strategy, let us assume the problem solved. The map $\Bg:\BG\rightarrow \BH$
 will then send any path $\alpha:\sh_G \eqto x$ to a path $\Bg(\alpha):\Bg(\sh_G) \eqto \Bg(x)$

fields.tex

@@ -54,12 +54,64 @@ \section{Rings, abstract and concrete}
 of $\mathscr R$ is abelian. Hint: elaborate $(a+1)\cdot(b+1)$.
 \end{xca}
 
-Note that, for any abstract ring $\mathscr R$ and elements $a,b:R$,
-both the left multiplication function $(a\cdot\blank)$ 
-and the right multiplication function $(\blank\cdot b)$ 
-are abstract homomorphisms of the additive group of $\mathscr R$ to itself.%
-\footnote{These functions provide two ways to write the product $a\cdot b$,
-see the coherence law in \cref{def:ring}\ref{ring:lr-coherence-law}.}
+We will now elaborate an approach to rings that is more in line
+with our set up. The obvious first step is to replace the abstract
+additive group by a (concrete) group. The multiplicative monoid
+poses some challenge, since monoids have no concrete counterpart in our set up.
+However, for any abstract ring $\mathscr R$ and element $a:R$,
+the left multiplication function $(a\cdot\blank)$ is an abstract homomorphism 
+of the additive group $(R,0,+,-)$ of $\mathscr R$ to itself.\footnote{%
+The same is true for the right multiplication function $(\blank\cdot a)$,
+which will play a role later, in \cref{rem:concrabsring}.}
+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)$
+of abstract homomorphisms from $(R,0,+,-)$ to itself.\footnote{%
+The operations of $\absHom_{\ptw}(R,R)$ are pointwise,
+induced by $(R,0,+,-)$. It is an abstract abelian group by
+\cref{xca:abs-homgroup} and \cref{xca:abstract-group-of-maps}.}
+
+Given that we have replaced $(R,0,+,-)$ by an abelian group $G:\Group$,
+the plan is to deloop $\absHom_{\ptw}(\abstr(G),\abstr(G))$. 
+Denoting the result of the delooping by $\Hom(G,G)$,\footnote{%
+It will always be clear from the context whether this denotes
+the \emph{set} of homomorphisms from $G$ to $G$, or the \emph{group}
+with this set of homomorphisms as underlying set.}
+we can then define the multiplication as a homomorphism
+$\mu: \Hom(G,\Hom(G,G))$.
+
+One way of delooping $\absHom_{\ptw}(\abstr(G),\abstr(G))$ would be
+to use the inverse of $\abstr$ in \cref{lem:homomabstrconcr}.
+This involves torsors and, though equivalent, is not close to $G$.  
+A better option is to use \cref{thm:abelian-groups-weq-sc2types},
+which we will do now.
+
+Recall from \cref{thm:abelian-groups-weq-sc2types} the equivalence
+$\BB$ from the type of abelian groups to the type of pointed
+simply connected $2$-types. Let $G:\AbGroup$ be an abelian group.
+Then the type $\BG\ptdto\BB G$ is a connected $1$-type\footnote{%
+Note that the maps are pointed.}, pointed at the constant map that sends
+$z:\BG$ to the point $(\BB G)_\pt\defeq (\BG_\div,\settrunc{\id_{\BG_\div}})$ 
+of $\BB G$.\footnote{Itself pointed by reflexivity.}
+Thus the type $\BG\ptdto\BB G$ classifies a group: 
+
+\begin{definition}\label{def:groupHom}
+Let $G:\AbGroup$ be an abelian group. Define the abelian group $\Hom(G,G)$
+of homomorphisms from $G$ to $G$ as the group classified
+by $\BHom(G,G) \defeq ((\BG\ptdto\BB G),(z\mapsto (\BB G)_\pt))$.
+\end{definition}
+
+The above definition of $\Hom(G,G)$ is indeed serving its purpose:
+
+\begin{construction}\label{cons:groupHomOK}
+Let $G:\AbGroup$ be an abelian group. Then we have an abstract isomorphism
+from $\USym\Hom(G,G)$ to $\absHom_{\ptw}(\abstr(G),\abstr(G))$.
+\end{construction}
+\begin{implementation}{cons:groupHomOK}
+TBD
+\end{implementation}
+
+\MB{{\color{red}CURSOR}}
+
 There are two ways to compose them: $(a\cdot(\blank\cdot b))$
 and $((a\cdot\blank)\cdot b)$. Equality of the latter two functions is
 an elegant way of expressing associativity.
@@ -77,7 +129,9 @@ \section{Rings, abstract and concrete}
     \begin{enumerate}
     \item\label{ring:unit-laws} $\ell_{1_R} = \id_G = r_{1_R}$ (the \emph{multiplicative unit laws})
     \item\label{ring:lr-coherence-law} $(\USym\ell_g)(h) = (\USymr_h)(g)$, 
-    for all $g,h : \USymR$ (the \emph{coherence law})
+    for all $g,h : \USymR$ (the \emph{coherence law})\footnote{%
+    These functions provide two ways to write the product $a\cdot b$,
+see the coherence law in \cref{def:ring}\ref{ring:lr-coherence-law}.}
         \item\label{ring:associativity-law} $\ell\circ r= r\circ\ell$ (the \emph{associativity law})
     \end{enumerate}
 The properties \ref{ring:unit-laws}-\ref{ring:associativity-law} 

group.tex

@@ -906,7 +906,8 @@ \section{Abstract groups}
 Let $\agp G$ be an abstract group with underlying set $S$.
 Let $X$ be a set. Show that the set $X\to S$ of functions
 from $X$ to $S$, together with pointwise operations induced by
-$\agp G$, forms and abstract group.
+$\agp G$, forms and abstract group which is abelian if and only
+if $\agp G$ is.
 \end{xca}
 
 

macros.tex

@@ -851,6 +851,7 @@
 \newcommand*{\pathsp}[1]{\constant{\mathbb P}_{\!#1}} % NB negative thin space
 \newcommand*{\uc}[1]{{\pathsp{#1}}}%universal set bundle
 \newcommand*{\abstr}{\casop{\constant{abs}}}
+\newcommand*{\deloop}{\casop{\constant{deloop}}}
 \newcommand*{\agp}[1]{\mathcal #1} %generic abstract group
 \newcommand*{\grpcenterinc}[1]{\mathrm z_{{#1}}} %