wip: ring and altring

Author: Marc Bezem

fields.tex

@@ -122,69 +122,90 @@ \section{Rings, abstract and concrete}
 \end{enumerate}
 Moreover, the following equations should hold:
     \begin{enumerate}
-    \item $\ev\circ(\USym(\mu\circ{1_R})(\Sloop)) = \B\id_R \approx \MB{TBD}$ 
+    \item\label{ring:unit-laws}
+    $\ev\circ(\USym(\mu\circ{1_R})(\Sloop)) = \B\id_R \approx \MB{TBD}$ 
     (the \emph{multiplicative unit laws})\footnote{%
 \MB{Not great:} $\USym(\mu\circ{1_R})$ is an abstract homomorphism
 from $\USym\ZZ$ to $\USym\Hom(R,R)$ and the latter type
 is equivalent to $(\BR\ptdto\loops\BB R)$. Finally by postcomposition
 with $\ev$, we get equivalence with $(\BR\ptdto\BR)$.
 The other unit law is probably worse.}
-    \item \MB{TBD} (the \emph{associative law}). %for all $z : \BR$
+    \item\label{ring:assoc-law} \MB{TBD} (the \emph{associative law}). %for all $z : \BR$
     \end{enumerate}
+The properties \ref{ring:unit-laws}-\ref{ring:assoc-law} 
+are together denoted by $\RingProps(R,1_R,\mu)$.
 The ring $R$ is called \emph{commutative} if \MB{TBD}, 
 and \emph{non-trivial} if $1_R$ is not trivial.\footnote{%
 A homomorphism is trivial if it classified by the constant function
 at the shape to the target group. Or, equivalently, if it factors
 through the trivial group.}
 \end{definition}
 
-\begin{xca}\label{xca:UR-abstractring}
-Let $(R,1_r,\mu)$ be a ring. Show that $\USymR$ is an abstract ring with
-multiplicative unit $\USym 1_R$ and multiplication $\USym\mu$. \MB{TBD}
-\end{xca}
-%Solution: 
+\begin{definition}\label{def:typering}
+The type of rings is defined as
+\[
+\typering\defeq\sum_{R:\AbGroup}\sum_{1_R:\Hom(\ZZ,R)}
+                \sum_{\mu:\Hom(R,\Hom(R,R))} \RingProps(R,1_R,\mu).
+\]
+The type $\typecommring$ of commutative rings is similar to the type
+of rings but with $\RingProps(R,1_R,\mu) \times \MB{TBD}$. 
+\end{definition}
 
 We proceed by giving the standard example of the integers as a ring
 in the sense of \cref{def:ring}.
 
 %\MB{CURSOR}
 
 \begin{example}
-Consider the abelian group $\ZZ$ of the integers classified by the circle.
-We use the same notation $\ZZ$ also for the ring of the integers.
+We take the group $\ZZ$ of the integers classified by the circle
+as the abelian group for the ring of the integers.
+We take $1_\ZZ \defeq \id_\ZZ$, the identity homomorphism.
+For defining $\mu$ we first elaborate $\Hom(\ZZ,\ZZ)$ as a group.
 Unfolding the definition we get (leaving the points implicit)
 $\B\Hom(\ZZ,\ZZ) \jdeq(\Sc\ptdto\sum_{X:\UU}\setTrunc{\Sc\eqto X})$.
 The shape of $\Hom(\ZZ,\ZZ)$ is the constant map 
 that sends any $z:\Sc$ to $(\Sc,\settrunc{\id_{\Sc}})$, pointed by reflexivity.
 
-For defining $1_\ZZ$, we
-recall \cref{xca:(S1->S1)_(f)-eqv-S1,xca:S1=S1-components},
-which give an equivalence $e:\Sc\to(\Sc\eqto\Sc)_{\id_\Sc}$
-which maps $\base$ to $\id_\Sc$.%
-\footnote{\MB{Isn't this $\inv\ev$ as $\ZZ$ is $Z(\ZZ)$?}}
-We take $1_\ZZ$ to be the homomorphism from $\ZZ$ to $\Hom(\ZZ,\ZZ)$
-classified by the map $\B 1_\ZZ$ sending $\base$ to $\sh_{\Hom(\ZZ,\ZZ)}$
-and $\Sloop$ to 
-and $\ell: (\base\eqto\base)\to\Hom(\ZZ,\ZZ)$ defined as follows.
-For every $g:\base\eqto\base$, let $\ell_g$ be the homomorphism
-classified by the map $\B\ell_g(\base)\defeq\base$, 
-$\B\ell_g(\Sloop)\defis g$, and pointed by reflexivity.\footnote{%
-The reader may recognize the degree $m$
-map from \cref{def:mfoldS1cover} as a special case.}
-Take $r\defeq\ell$. Now the unit laws, the coherence law and
-the associativity law can easily be verified. It follows that
+Recall that $\BB\ZZ \jdeq \sum_{X:\UU}\setTrunc{\Sc\eqto X})$,
+pointed at $\sh_{\BB\ZZ}\jdeq (\Sc,\settrunc{\id_\Sc})$.
+For $\mu: \Hom(\ZZ,\Hom(\ZZ,\ZZ))$ we take,\footnote{\MB{Exercise material?}
+Define $s:\id_\Sc\eqto\id_\Sc$ by function extensionality,
+setting $s(\base)\defeq\Sloop$, $s(\Sloop)\defis {!}$.
+Now define $e_z: \Sc\eqto\Sc$ by $e_z(\base)\defeq z$,
+$e_z(\Sloop) \defis s(z) : (z\eqto z)$. Indeed, $e_\base = \id_\Sc$
+and, by path induction $e_p(\base)=p$ for all $p:\base\eqto z$,
+so $e_{\Sloop} = s$.}
+with $\ve$ from \cref{lem:freeloopspace},
+\[
+\B\mu \defeq (z:\Sc) \mapsto \ve_{\BB\ZZ}(\sh_{\BB\ZZ},(e_z,!)).
+\]
+In this succint definition, $\ve_{\BB\ZZ}(\sh_{\BB\ZZ},\settrunc{e_z})$
+can be identified as the function from $\Sc$ to $\BB\ZZ$ that sends 
+$\base$ to $\Sc$ and $\Sloop$ to $(e_z,!)$ where $e_z:(\Sc\eqto\Sc)$,
+$!: \Trunc{e_z\eqto\id_\Sc}$. In the following we focus on first components,
+that is, on $\Sc$ and $e_z$, analyzing how $\B\mu$ applies to paths.
+
+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)$.
+\MB{Almost there! Use $\ev$ to get to $\USym\ZZ$?}
+
+
+
+
+%\cref{xca:(S1->S1)_(f)-eqv-S1,xca:S1=S1-components},
+%which give an equivalence $e:\Sc\to(\Sc\eqto\Sc)_{\id_\Sc}$
+%which maps $\base$ to $\id_\Sc$.%
+It follows that
 $(\ZZ,1_\ZZ,\mu)$ is a non-trivial commutative ring.
 \end{example}
 
-\begin{definition}\label{def:typering}
-The type of rings is defined as
-\[
-\typering\defeq\sum_{R:\AbGroup}\sum_{1_R:\Hom(\ZZ,R)}
-                \sum_{\mu:\Hom(R,\Hom(R,R))} \RingProps(R,1_R,\mu).
-\]
-The type $\typecommring$ of commutative rings is similar to the type
-of rings but with $\RingProps(R,1_R,\mu) \times \MB{TBD}$. 
-\end{definition}
+\begin{xca}\label{xca:UR-abstractring}
+Let $(R,1_r,\mu)$ be a ring. Show that $\USymR$ is an abstract ring with
+multiplicative unit $\USym 1_R$ and multiplication $\USym\mu$. \MB{TBD}
+\end{xca}
+%Solution: 
 
 \subsection{Yet another \MB{(experimental)} definition of rings}
 \label{ssec:altring}
@@ -199,7 +220,7 @@ \subsection{Yet another \MB{(experimental)} definition of rings}
 abstract homomorphisms
 of the additive group $(R,0,+,-)$ 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:altring}\ref{ring:lr-coherence-law}.}
+see the coherence law in \cref{def:altring}\ref{altring:lr-coherence-law}.}
 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.
@@ -217,25 +238,25 @@ \subsection{Yet another \MB{(experimental)} definition of rings}
 $r_g$ for $r(g)$.
 Moreover, the following equations should hold.
     \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)$, 
+    \item\label{altring:unit-laws} $\ell_{1_R} = \id_G = r_{1_R}$ (the \emph{multiplicative unit laws})
+    \item\label{altring:lr-coherence-law} $(\USym\ell_g)(h) = (\USymr_h)(g)$, 
     for all $g,h : \USymR$ (the \emph{coherence law})
-        \item\label{ring:associativity-law} $\ell\circ r= r\circ\ell$ (the \emph{associativity law})
+        \item\label{altring:assoc-law} $\ell\circ r= r\circ\ell$ (the \emph{associativity law})
     \end{enumerate}
-The properties \ref{ring:unit-laws}-\ref{ring:associativity-law} 
+The properties \ref{altring:unit-laws}-\ref{altring:assoc-law} 
 are together denoted by $\RingProps(R,1_R,\ell,r)$.
 The ring $R$ is called \emph{commutative} if $\ell=r$,
 and \emph{non-trivial} if $1_R \neq \refl{R}$.
 \end{definition}
 
-The coherence law \ref{ring:lr-coherence-law} allows us to abbreviate both 
+The coherence law \ref{altring:lr-coherence-law} allows us to abbreviate both 
 $(\USym\ell_g)(h)$ and $(\USymr_h)(g)$ by $g\cdot h$. We will do this when
 no confusion can occur. Then, $\ell=r$ 
 amounts to $g\cdot h = h\cdot g$, for all $g,h : \USymG$,
 as could be expected from the abstract case.
 
 We proceed by giving the standard example of the integers as a ring
-in the sense of \cref{def:ring}.
+in the sense of \cref{def:altring}.
 \begin{example}
 Consider the group $\ZZ$ classified by the circle.
 Using the same notation $\ZZ$ also for the ring, take $1_\ZZ \defeq\Sloop$