fix bug in Thm 7.4.8 found by Jon Sterling on mathstodon

Author: UlrikBuchholtz

absgroup.tex

@@ -461,20 +461,22 @@ \section{Groups: from abstract to concrete and back}
 Given an abstract group ${\agp G}\jdeq(S,e,\mu,\iota)$, a \emph{$\agp G$-set}%
 \glossary(GSet){\protect{$\absGSet$}}{type of $\agp G$-sets}
 \index{GSet@$\agp G$-set (of abstract group)}
-is a set $S$ together with a homomorphism
-$\agp G\to\abstr(\Sigma_S)$
-from $\agp G$ to the abstract permutation group of $S$.
-Then the type of $\agp G$-sets is defined as 
-$$\absGSet\defequi \sum_{S:\Set}\absHom({\agp G},\abstr(\Sigma_{S})).$$
-
-The \emph{principal ${\agp G}$-torsor} $\absprtor$ is the 
-${\agp G}$-set consisting of the underlying set $S$ together with 
-the homomorphism ${\agp G}\to\abstr(\Sigma_{S})$ with underlying 
+is a set $T$ together with a homomorphism
+$\agp G\to\abstr(\Sigma_T)$
+from $\agp G$ to the abstract permutation group of $T$.
+Then the type of $\agp G$-sets is defined as
+\[
+  \absGSet\defequi \sum_{T:\Set}\absHom({\agp G},\abstr(\SG_T)).
+\]
+
+The \emph{principal ${\agp G}$-torsor} $\absprtor$ is the
+${\agp G}$-set consisting of the underlying set $S$ together with
+the homomorphism ${\agp G}\to\abstr(\Sigma_{S})$ with underlying
 function $S\to (S\eqto S)$ given by sending $g:S$ to $(s\mapsto \mu(g,s))$.
 
 The type of \emph{${\agp G}$-torsors} is
 \[
-\absGTor\defequi\sum_{\absGSetvar:\absGSet}
+  \absGTor\defequi\sum_{\absGSetvar:\absGSet}
   \Trunc{\absprtor \eqto \absGSetvar}.\qedhere
 \]
 \end{definition}
@@ -636,13 +638,13 @@ \section{Groups: from abstract to concrete and back}
 \]
 Setting $t\defequi e$ in the last equation, we see that $\pi(s)=\mu(s,\pi(e))$,
 that is, $\pi$ is simply multiplication with an element $\pi(e):S$.
-In other words,\footnote{Indeed, conversely, $\mu(u,\blank)$
+In other words,\footnote{Indeed, conversely, $\mu(\blank,\inv u)$
 satisfies the condition for $\pi$. Prove this!}
 the function
 \[
 r_{\agp G}:S\to  \sum_{\pi:S\equivto S}\prod_{s,t:S}
 \bigl(\pi(\mu(s,t))=\mu(s,\pi(t)\bigr),
-\qquad r_{\agp G}(u)\defequi(\mu(u,\blank),!)
+\qquad r_{\agp G}(u)\defequi(\mu(\blank,\inv u),!)
 \]
 is an equivalence of sets.
 
@@ -658,8 +660,10 @@ \section{Groups: from abstract to concrete and back}
 In view of \cref{def:abstrisfunctor}, for $r_{\agp G}$ to be an isomorphism,
 it suffices that $r_{\agp G}$ preserves multiplication:
 $r_{\agp G}(\mu(u,v))=r_{\agp G}(u)\circ r_{\agp G}(v)$.
-This follows directly from function extensionality and 
-the associativity of $\mu$. Hence the equivalence $r_{\agp G}$ is 
+This follows directly from function extensionality,
+associativity of $\mu$,
+and the equation $\inv{\mu(u,v)} = \mu(\inv v,\inv u)$.
+Hence the equivalence $r_{\agp G}$ is
 indeed an isomorphism of abstract groups.\footnote{%
  \label{ft:abstract-Cayley}
  This amounts to Cayley's Theorem for abstract groups,