finite group + minor in 5.8

actions.tex

@@ -1278,8 +1278,8 @@ \section{Invariant maps and orbits}
 \end{proof}
 
 \begin{corollary}\label{cor:orbit-equiv}\MB{New:}
-Being surjective, the map $[\blank] : X(\sh_G) \to X/G$ induces\footnote{%
-\MB{To do in Chapter 2, then refer to it.}}
+Being surjective, the map $[\blank] : X(\sh_G) \to X/G$ induces
+by \cref{xca:map-induces-quotient}\ref{it:surj-ind-quot=codomain}
 an equivalence between the induced quotient of $X(\sh_G)$ and $X/G$.
 \end{corollary}
 
@@ -2102,31 +2102,36 @@ \section{The lemma that is not Burnside's}
 \label{sec:burnsides-lemma}
 \label{lem:burnsides-lemma}
 
+\begin{definition}\label{def:finite-group}\MB{Where?}
+A group $G$ is a \emph{finite group} if $\isfinset(\USymG)$.
+\index{finite group}\index{group!finite}
+\end{definition}
+
 \begin{lemma}
   \label{lem:burnside}
   Let $G$ be a finite group acting on a finite set $X$.
   Then the set of orbits is finite with cardinality
   \[
-    \Card(X/G) = \frac1{\Card(G)}\sum_{g:\El G}\Card(X^g),
+    \Card(X/G) = \frac1{\Card(G)}\sum_{g:\USymG}\Card(X^g),
   \]
-  where $X^g = \setof{x:X}{gx=x}$ is the set of elements
+  where $X^g = \setof{x:X}{g\cdot x = x}$ is the set of elements
   that are fixed by $g$.
 \end{lemma}
 \begin{proof}
   Since $X$ and $G$ is finite, we can decide equality of their elements.
   Hence each $X^g$ is a finite set, and since $G$ is finite,
   we can decide whether $x,y$ are in the same orbit by searching
-  for a $g : \El G$ with $gx = y$.
+  for a $g : \USymG$ with $g\cdot x = y$.
   Hence the set of orbits is a finite set as well.
 
-  Consider now the set $R \defeq \sum_{g:\El G} X^g$,
+  Consider now the set $R \defeq \sum_{g:\USymG} X^g$,
   and the function $q : R \to X$
   defined by $q(g,x) \defeq x$.
   The map $q^{-1}(x) \to G_x$ that sends $(g,x)$ to $g$ is a bijection.
   Thus, we get the equivalences
   \[
-    R \jdeq \sum_{g:\El G} X^g \equiv \sum_{x:X} G_x
-    \equiv \sum_{z:X/G} \sum_{x : \mathcal O_z} G_x,
+    R \jdeq \sum_{g:\USymG} X^g \equivto \sum_{x:X} G_x
+    \equivto \sum_{z:X/G} \sum_{x : \mathcal O_z} G_x,
   \]
   where the last step writes $X$ as a union of orbits.
   Within each orbit $\mathcal O_z$,

intro-uf.tex

@@ -3901,9 +3901,9 @@ \subsection{Set quotients}
 \glossary[A/f]{$A/f$}{quotient induced by $f:A\to B$}
 Now:
 \begin{enumerate}
-\item\label{it:inj-ind-settrunc-domain}
+\item\label{it:inj-ind-settrunc=domain}
 If $f$ is injective, give an equivalence from $A/f$ to $\setTrunc{A}$;
-\item\label{it:surj-ind-equiv-codomain}
+\item\label{it:surj-ind-quot=codomain}
 If $B$ is a set and $f$ surjective, give an equivalence from $A/f$ to $B$.\qedhere
 \end{enumerate}
 \end{xca}