@@ -652,18 +652,26 @@ \section{Subgroups}
652652\subsection {Subgroups through $ G$ -sets }
653653
654654The idea is that a $ G$ -set $ X$ picks out those symmetries in $ G$
655- that keep the point of $ X(\sh _G)$ in place. For this to work well
655+ that keep a chosen point of $ X(\sh _G)$ in place. For this to work well
656656we need to point $ X(\sh _G)$ and $ X$ must be transitive.
657657% so that the set of symmetries that are picked out is closed under composition and reverse.
658658
659659\begin {definition }\label {def:set-of-subgroups }
660- For any group $ G$ , define the type of \emph {subgroups of $ G$ } as
661- \index {type!of subgroups of a group}
662- % \glossary(SubG){$\protect{\Sub_G}$}{type of subgroups of $G$} ERROR???
663- $$ \typesubgroup _G\defequi\sum _{X:\BG\to\Set }{\, }X(\sh _G)
664- \times \istrans (X).$$
665- The \emph {underlying group } of the subgroup $ (X,x,!) : \Sub _G$ is
666- $$ \mkgroup \bigl (\sum _{z:BG}X(z),(\sh _G,x)\bigr ).\qedhere $$
660+ For any group $ G$ , define the type of \emph {subgroups of $ G$ } as%
661+ \index {type!of subgroups of a group}%
662+ \glossary (SubG){$ \protect\Sub (G)$ }{type of subgroups of $ G$ }
663+ \[
664+ \Sub (G)\defequi\sum _{X:\BG\to\Set }{\, }X(\sh _G)
665+ \times\istrans (X).
666+ \]
667+ The \emph {underlying group } of the subgroup $ (X,x) : \Sub (G)$ is\footnote {%
668+ To lighten the notation, we leave out the proof that $ X$ is transitive.
669+ (Otherwise, we would write $ (X,x,!):\Sub (G)$ .)
670+ In~\cref {rem:notationsubgroup } below we'll set out further notational conveniences
671+ regarding subgroups.}
672+ \[
673+ \mkgroup \biggl (\sum _{z:BG}X(z),(\sh _G,x)\biggr ).\qedhere
674+ \]
667675\end {definition }
668676
669677\begin {xca }\label {xca:group-Xx! }
@@ -687,18 +695,18 @@ \subsection{Subgroups through $G$-sets}
687695$ R(\Sloop ) \defis \etop\zs $ , see \cref {def:RtoS1 }.
688696Again we point by $ 0 : R(\base )$ and transitivity of $ R$ is obvious.
689697The only symmetry that keeps $ 0 $ in place is $ \refl {\base }$ ,
690- since $ R(\Sloop ) = \zs $ if and only if $ k=0 $ .
698+ since $ R(\Sloop ^k)( 0 ) = \zs ^k( 0 ) = k = 0 $ if and only if $ k=0 $ .
691699Again, no surprise in view of the results in \cref {sec:symcirc }
692700identifying $ R$ as the universal \covering over $ \Sc $ .
693701
694- The following result is analogous to the fact that $ \Sub _T $ is
702+ The following result is analogous to the fact that $ \Sub (T) $ is
695703a set for any type $ T$ , see \cref {xca:subtypes-set }. It captures
696704that the essence of picking out symmetries (or picking out elements
697705of a type), is a predicate, like $ R_m(p)(0 )=0 $ above.
698706
699707\begin {lemma }
700708 \label {lem:SubGisset }%
701- The type $ \typesubgroup _G $ is a set, for any group $ G$ .
709+ The type $ \Sub (G) $ is a set, for any group $ G$ .
702710\end {lemma }
703711\begin {proof }
704712Let $ G$ be a group, and let $ X$ and $ X'$ be transitive $ G$ -sets with
0 commit comments