@@ -769,7 +769,7 @@ \section{Homomorphisms, from abstract to concrete and back}
769769 \]
770770 to be the set quotient of $ (\sh _H\eqto y)\times X(\sh _G)$ modulo
771771 the equivalence relation $ (p,x)\sim (p\, \phi (\inv g),g\cdot _X x)$ for all
772- $ g:\sh _G\eqto\sh _G$ .\footnote {\MB {Induction? $ \exists y $ ?}}
772+ $ g:\sh _G\eqto\sh _G$ .\footnote {\MB {Should be map to $ \Prop $ . Induction? $ \exists g $ ?}}
773773\end {definition }
774774
775775\begin {lemma }\label {lem:abshom_* }
@@ -798,26 +798,30 @@ \section{Homomorphisms, from abstract to concrete and back}
798798$$ \pathsp {}:\Hom (G,H)\we
799799\bigl ((\typetorsor _G,\princ G)\ptdto (\typetorsor _H,\princ H)\bigr )
800800$$
801- by mapping $ \Bf $ to $ \princ H\circ \Bf \circ \invprinc G$ .
802- Then $ A\defeq ({\abstr }\circ \pathsp {}^{-1})$ is a map
801+ by mapping, for any $ f:\Hom (G,H)$ , $ \Bf $ to
802+ $ \pathsp {\blank }^H\circ \Bf \circ (\pathsp {\blank }^G)^{-1}$ .
803+ Then $ A\defeq ({\abstr }\circ \pathsp {}^{-1})$ is a map\footnote {%
804+ \MB {To show that
805+ $ \abstr :\Hom (G,H)\to \absHom (\abstr (G),\abstr (H))$ is an equivalence,
806+ we factor it as $ A\circ \pathsp {}$ and prove that both factors are
807+ equivalences.}}
803808\[
804809A:\bigl ((\typetorsor _G,\princ G)\ptdto (\typetorsor _H,\princ H)\bigr )
805810 \to \absHom (\abstr (G),\abstr (H))
806811\]
807- satisfying $ { \loops f} \circ \pathsp { \blank }^G= \pathsp { \blank }^H \circ A(f) $
808- for all $ f $ in the domain of $ A $ :
812+ satisfying, for all $ g $ in the domain of $ A $ ,
813+ $ { \loops g} \circ \pathsp { \blank }^G= \pathsp { \blank }^H \circ A(g) $ :
809814% see \cref{fig:mapA}
810815\[ % begin{marginfigure}
811816 \begin {tikzcd }[ampersand replacement=\& ]
812- \USymG \ar [r,"A(f )"]\ar [d,eql,"{\pathsp {\blank }^G}"'] \&
817+ \USymG \ar [r,"A(g )"]\ar [d,eql,"{\pathsp {\blank }^G}"'] \&
813818 \USymH \ar [d,eqr,"{\pathsp {\blank }^H}"] \\
814- \princ G\eqto\princ G \ar [r,"{\loops f }"'] \& \princ H\eqto\princ H
819+ \princ G\eqto\princ G \ar [r,"{\loops g }"'] \& \princ H\eqto\princ H
815820 \end {tikzcd }
816821 % \caption{\label{fig:mapA}caption}
817822\] % end{marginfigure}
818- (together with the proof that $ A(f )$ is an abstract group homomorphism).
823+ (together with the proof that $ A(g )$ is an abstract group homomorphism).
819824We are done if we show that $ A$ is an equivalence.
820- \marginnote {The reason to complicate $ \abstr $ this way is that it gets easier to write out the inverse function.\MB {MB doesn't understand.}}
821825
822826For any $ \phi :\absHom (\abstr (G),\abstr (H))$ , recall the pointed map
823827\[
0 commit comments