xca:G/X-set-of-orbits and lem:splitting into orbits in 5.4

actions.tex

@@ -1073,7 +1073,8 @@ \section{Fixed points and orbits}
   $X/G \jdeq \setTrunc{X_{hG}}$ is itself the
   set quotient of $X_{hG} \jdeq \sum_{z:\BG}X(z)$ by
   the relation $\sim$ defined by letting $(z,x)\sim(w,y)$
-  if and only if $\exists_{g:z\eqto w}(g\cdot x=y)$.
+  if and only if $\exists_{g:z\eqto w}(g\cdot x=y)$.\footnote{%
+  \MB{Also iff $\Trunc{(z,x)\eqto(w,y)}$.}}
   Thus,~\cref{thm:quotient-property} gives the
   desired conclusion.
 \end{proof}
@@ -1111,6 +1112,46 @@ \section{Fixed points and orbits}
 \MB{Steer away from $\inv E$?? $G$-\emph{sub}set in ftn 17??}
 \end{xca}
 
+The following exercise explains why we call $X/G$ the set of orbits.
+\begin{xca}\label{xca:G/X-set-of-orbits}\MB{New}
+Let $G$ be a group and $X$ a $G$-set. 
+Let $\inv{[\blank]} : X/G \to \Sub_{X(\sh_G)}$
+map any $z$ to its preimage $\setof{x : X(\shape_G)}{z =_{X/G} [x]}$.
+Show:
+\begin{enumerate}
+\item For all $z: X/G$ the set $\inv{[z]}$ is non-empty;
+\item The map $\inv{[\blank]}$ is an injection;
+\item The image of $\inv{[\blank]}$ consists precisely of all orbits.\footnote{%
+\MB{An \emph{orbit} is a orbit of $x$ for some $x:X(\sh_G)$.}}
+\end{enumerate}
+\end{xca}
+
+The following lemma states that the orbits of a $G$-set $X$
+sum up to its underlying set, with the sum taken over the set
+of orbits $X/G$.
+
+\begin{lemma}\MB{Replaces \cref{lem:splitting into orbits}.}
+  \label{lem:splitting into orbits}
+  The inclusions of the orbits form an equivalence
+\[
+  (z,x,!)\mapsto x \quad:\quad
+  \bigl(\sum_{z:X/G}\sum_{x:X(\shape_G)} 
+  (\inv{[z]} =_{\Sub_{X(\shape_G)}}(G\cdot x))\bigr)
+  \we X(\shape_G).
+\]
+\end{lemma}
+\begin{proof}
+We show for all $z:X/G$ and $x:X(\shape_G)$ that $z=[x]$
+if and only if $\inv{[z]} =_{\Sub_{X(\shape_G)}}(G\cdot x)$.
+Then the result follows by contracting away $z$.
+
+Clearly, if $z=[x]$, then the predicates $z=[\blank]$ for $\inv{[z]}$
+and $[x]=[\blank]$ for $G\cdot x$ are equal. The converse implication is
+immediate.
+\end{proof}
+
+
+
 Note that the classifying type $\BG_x$ of $G_x$
 is identified with the fiber of $\settrunc{\blank} : X_{hG} \to X/G$,
 and $G\cdot x$ (pointed at $x$)