Polished Def. 6.5.3

Author: Marc Bezem

absgroup.tex

@@ -769,7 +769,7 @@ \section{Homomorphisms, from abstract to concrete and back}
 by $\Trunc{(\sh_G,p,x)\eqto(\sh_G,q,y)}$, which is equivalent to
 $\exists_{g:\USymG}((p=q\ap{f}(g))\times(g\cdot_X x = y))$.
 
-\begin{definition}\label{def:abshom_*} %\MB{From old 5.5.}
+\begin{definition}\label{def:abshom_*}
   Given groups $G$, $H$ and an abstract homomorphism
   $\phi:\absHom(\abstr(G),\abstr(H))$, we define the map $\phi_*$
   from $G$-sets to $H$-sets as follows. 
@@ -779,24 +779,28 @@ \section{Homomorphisms, from abstract to concrete and back}
   \]
   to be the set quotient of $(\sh_H\eqto w)\times X(\sh_G)$ modulo
   the equivalence relation $(p,x)\sim(q,y)$ if there exists a $g:\USymG$
-  such that $p=q\phi(g)$ and $g\cdot_X x)$.
+  such that $p=q\phi(g)$ and $g\cdot_X x = y$.
 \end{definition}
 
 \begin{lemma}\label{lem:abshom_*}
   With $\phi_*$ as in \cref{def:abshom_*}, the map 
-  $\eta_\phi:\phi_*\princ G \equivto \princ H$ sending, for all $y:\BH$,
-  $[(p,g)]: (\sh_H \eqto y) \times_G \USymG$ to $p\phi(g):(\sh_H\eqto y)$,
+  $\eta_\phi:\phi_*\princ G \equivto \princ H$ sending, for all $w:\BH$,
+  $[(p,x)]: (\sh_H \eqto w) \times_G \USymG$ to $p\phi(x):(\sh_H\eqto w)$,
   is a well defined (fiberwise) equivalence. Consequently,
   $(\phi_*,\inv{\eta_\phi})$ is a pointed map from
   $(\typetorsor_G,\princ G)$  to $(\typetorsor_H,\princ H)$.
 \end{lemma}
 \begin{proof}
-First, $\eta_\phi$ respects $\sim$ since
-$p\phi(\inv g)\phi(gq) = p\phi(q)$, so it is indeed well defined.
+First we show that $\eta_\phi$ respects the equivalence relation.
+Let $(p,x)\sim(q,y)$ with $p,q:(\sh_H \eqto w)$ and $x,y:\USymG$.
+Then there exists a $g:\USymG$ such that $p=q\phi(g)$ and $g\cdot_X x = y$.
+Now, $p\phi(x)=q\phi(gx) = q\phi(y)$, so $\eta_\phi$
+is indeed well defined.
 It is also clearly a surjection. So it remains to prove that $\eta_\phi$
-is injective. Assume $(p,g)$ and $(p',g')$ are such that
-$p\phi(g) = p'\phi(g')$. Then $p'= p\phi(g\inv{g'})$, and
-hence $(p,g)\sim(p',g')$, so their classes are equal.
+is injective. Assume $(p,x)$ and $(q,y)$ are such that
+$p\phi(x) = q\phi(y)$. Then $p= q\phi(y\inv{x})$ and 
+$y\inv{x}\cdot_X x = y$. 
+Hence $(p,x)\sim(q,y)$, so their classes are equal.
 This shows that $\eta_\phi$ is injective, and completes the proof.
 \end{proof}