Lagrange + extra in 5.4

actions.tex

@@ -1063,7 +1063,7 @@ \section{Invariant maps and orbits}
 the action type in blue (\ie corresponding to an element of the set of orbits),
 and we see that it contains a subset of the underlying set,
 the three red elements $\set{0,1,2}$.
-Such a set is what is traditionally called an orbit \MB{(contested!)}
+Such a set is what is traditionally called an orbit \MB{(contested)}
 This connection is emphasized in the following result.
 
 \begin{lemma}\label{lem:orbit-equiv}
@@ -1104,7 +1104,7 @@ \section{Invariant maps and orbits}
   \begin{enumerate}
   \item Define the group $G_x \defeq \Aut_{X_{hG}}(\sh_G,x)$.
   Clearly, $\fst:\BG_x \to \BG$ is a set bundle:
-  each fiber at $z:\BG$ is a subset\footnote{%
+  each fiber at $z:\BG$ is a subset\footnote{\label{ft:fib-fst}%
   $\sum_{y:X(z)}\Trunc{(\sh_G,x)\eqto(z,y)}$} of $X(z)$.
   Hence $(G_x,\fst,!):\typemono_G$ is monomorphism into $G$.
   We call the subgroup $G_x$ of $G$ the 
@@ -1113,15 +1113,15 @@ \section{Invariant maps and orbits}
     $\BG$ classifies a monomorphism denoted by $i_x : \Hom(G_x,G)$.
   \item Define $G\cdot x \defeq \setof{y : X(\sh_G)}{[x] =_{X/G} [y]}$
     to be the \emph{orbit}\index{orbit!of $x$} of $x$.
-    An \emph{orbit} is the orbit of $x$ for some $x:X(\sh_G)$\MB{(contested!)}.\footnote{%
+    An \emph{orbit} is the orbit of $x$ for some $x:X(\sh_G)$\MB{(contested)}.\footnote{%
     In \cref{lem:G/X-set-of-orbits} we explain how orbits correspond
     to elements of the set of orbits $X/G$. We freely use the term
     `orbit' for both.}\qedhere
   \end{enumerate}
 \end{definition}
 \begin{xca}\label{xca:Gx-in-Sub_G}
 Find $(X_x,x,!):\Sub_G$ corresponding to $(G_x,\fst,!):\typemono_G$.
-\MB{Steer away from $\inv E$?? $G$-\emph{sub}set in ftn 18??}
+\MB{Steer away from $\inv E$?? $G$-\emph{sub}set in \cref{ft:fib-fst}??}
 \end{xca}
 
 The following lemma explains why we call $X/G$ the set of orbits.
@@ -1157,7 +1157,7 @@ \section{Invariant maps and orbits}
 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}.}
+\begin{lemma}\footnote{\MB{Replaces \cref{old:splitting into orbits}.}}
   \label{lem:splitting into orbits}
   The inclusions of the orbits form an equivalence
 \[
@@ -1173,40 +1173,11 @@ \section{Invariant maps and orbits}
 the equivalence classes sum up to $A$.}
 \end{proof}
 
-The first projection of a symmetry of the shape of the
-stabilizer group $G_x$ is a symmetry of the shape of $G$,
-and the second projection is just a true proposition.
-This suggest a simple way for $G_x$ to act on the latter
-symmetries, by just ignoring the second projection. 
-Then one gets a $G_x$-set whose action type can, as expected,
-easily be identified with the orbit of $x$. This is spelled
-out in the following construction.
-
-\begin{construction}[Orbit-stabilizer theorem]
-\MB{Replaces \cref{thm:orbitstab}.}
-  \label{thm:orbitstab}
-  Fix a $G$-type $X$ and a point $x : X(\sh_G)$. Define the $G_x$-type
-  $\tilde X_x : \BG_x \to \UU$ by $\tilde X_x(z,\blank,!)\defeq(\sh_G\eqto z)$,
-  acting on $\tilde X_x(\sh_{G_x})\defeq (\sh_G\eqto\sh_G)$.
-  Then we have an equivalence from the action type $(\tilde X_x)_{hG_x}$
-  to the orbit $G\cdot_X x$ of $x$.
-\end{construction}
-\begin{implementation}{thm:orbitstab}
-  The desired equivalence is the composition of elementary equivalences
-  for sums and products, followed by contracting away the $z$:
-  \begin{align*}
-    (\tilde X_x)_{hG_x}
-    &\defeq \sum_{u : \BG_x}\tilde X_x(u) \\
-    &\equivto \sum_{z:\BG}\sum_{y:X(z)}
-    (\settrunc{(\sh_G,x)} =_{X/G} \settrunc{(z,y)})\times (\sh_G \eqto z) \\
-    &\equivto \sum_{y:X(\sh_G)}[x] =_{X/G} [y]\quad\defeq\quad(G\cdot_X x).\qedhere
-  \end{align*}
-\end{implementation}
 
 
 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$ \MB{MB???)})
+and $G\cdot x$ (pointed at $x$)
 is identified with the fiber of $[\blank] : X(\sh_G) \to X/G$,
 both taken at $[x]$, the orbit containing $x$.
 
@@ -1223,7 +1194,7 @@ \section{Invariant maps and orbits}
       \& X/G, \&
     \end{tikzcd}
   \]
-  Note that $\inv{[[x]]}\jdeq(G\cdot x)$
+  Indeed, $\inv{[[x]]}\jdeq(G\cdot x)$
   and $\inv{\settrunc{[x]}}\equivto \BG_x$ via identity on $X_{hG}$.}
 
 
@@ -1253,21 +1224,6 @@ \section{Invariant maps and orbits}
   being an isomorphism.
 \end{proof}
 
-\begin{lemma}\label{lem:free-pt-char}
-  Given a $G$-set $X$, an element $x:X(\sh_G)$ is\marginnote{%
-    Doesn't fit well here; move to where?}
-  free if and only if the (surjective) map
-  $\blank \cdot x : \USymG \to G\cdot x$ is injective
-  (and hence a bijection).
-\end{lemma}
-\begin{proof}
-  Consider two elements of the orbit, say $g\cdot x,g'\cdot x$ for $g,g':\USymG$.
-  We have $g\cdot x=g' \cdot x$ if and only if $x = \inv{g} g'\cdot x$
-  if and only if $\inv{g} g'$ lies in $\USymG_x$.
-  \MB{Now apply \cref{xca:connected-trivia} yielding that that 
-  $G_x$ is trivial iff $\USymG_x$ is contractible.}
-\end{proof}
-
 When $X : \BG \to \Set$ is a $G$-set for an ordinary group $G$, the subset
 \[
   \setof{x : X(\sh_G)}{\text{$x$ is fixed}}
@@ -1329,6 +1285,115 @@ \section{Invariant maps and orbits}
 the $\SG_2$-sets $X(\blank,\bn2)$ and $X(\bn2,\blank)$.
 \end{xca}
 
+\subsection{The Orbit-stabilizer theorem and Lagrange's theorem}
+
+Recall \cref{def:orbit-stabilizer}.
+The classifying type of the stabilizer group $G_x$
+is the component of $X_{hG}$ containing the shape $(\sh_G,x)$.
+The first projection of a symmetry of $(\sh_G,x)$ is a symmetry of 
+$\sh_G$, and the second projection is just a true proposition.
+This suggest a simple way for $G_x$ to act on the
+symmetries of $\sh_G$, by just ignoring the second projection. 
+Then one gets a $G_x$-set whose action type can, as expected,
+easily be identified with the orbit of $x$. This is spelled
+out in the following construction.
+
+\begin{construction}[Orbit-stabilizer theorem]
+\footnote{\MB{Replaces \cref{old:orbitstab}.}}
+  \label{thm:orbitstab} Let $G$ be a group.\footnote{%
+  \MB{This construction works for $\infty$-groups as well.}}
+  Fix a $G$-type $X$ and a point $x : X(\sh_G)$. Define the $G_x$-type
+  $\tilde G_x : \BG_x \to \UU$ by $\tilde G_x(z,\blank,!)\defeq(\sh_G\eqto z)$,
+  acting on $\tilde G_x(\sh_{G_x})\defeq (\sh_G\eqto\sh_G)$.
+  Then we have an equivalence from the action type $(\tilde G_x)_{hG_x}$
+  to the orbit $(G\cdot_X x)$ of $x$.
+\end{construction}
+\begin{implementation}{thm:orbitstab}
+  The desired equivalence is the composition of elementary equivalences
+  for sums and products, followed by contracting away the variable $z$:
+  \begin{align*}
+    (\tilde G_x)_{hG_x}
+    &\defeq \sum_{u : \BG_x}\tilde G_x(u) \\
+    &\equivto \sum_{z:\BG}\sum_{y:X(z)}
+    (\settrunc{(\sh_G,x)} =_{X/G} \settrunc{(z,y)})\times (\sh_G \eqto z) \\
+    &\equivto \sum_{y:X(\sh_G)}[x] =_{X/G} [y]\quad\defeq\quad(G\cdot_X x).\qedhere
+  \end{align*}
+\end{implementation}
+
+The above theorem holds for $\infty$-groups $G$ and $G$-types $X$,
+but if $\BG$ is a groupoid and $X$ is a $G$-set,
+then we can draw some interesting additional conclusions. 
+In that case also $\BG_x$ is a groupoid and $(G\cdot_X x)$ is a set.
+\cref{thm:orbitstab} then tells us that $(\tilde G_x)_{hG_x}$ is a set.
+By the following exercise we get that all stabilizer subgroups $(G_x)_g$
+of the $G_x$-set $\tilde G_x$ are trivial,
+\ie the action $\tilde G_x$ is free.
+\cref{lem:free-pt-char} below will allow us to conclude that
+all orbits $(G_x \cdot_{\tilde G_x} g)$ are equivalent.
+
+\begin{xca}\label{xca:set-symms-contractible}\MB{New:}
+Let $G$ be a \aninftygp and $X$ a $G$-type. Then the
+action type $X_{hG}$ is a set if and only if each
+stabilizer group $G_x$ is trivial.
+\end{xca}
+%solution\begin{proof}
+%Any type $T$ is a set iff all identity types $t\eqto_T t$ are contractible.
+%Since $\BG$ is connected we get that $X_{hG}$ is a set iff each
+%identity type $(\sh_G,x)\eqto (\sh_G,x)$ is contractible, \ie
+%each stabilizer group $G_x$ is trivial.\end{proof}
+
+\begin{lemma}\label{lem:free-pt-char}
+  Let $G$ be a group.
+  Given a $G$-set $X$, an element $x:X(\sh_G)$ is
+  free if and only if the (surjective) map
+  $(\blank \cdot x) : \USymG \to (G\cdot x)$ is injective
+  (and hence a bijection).
+\end{lemma}
+\begin{proof}
+  Consider two elements of the orbit, say $g\cdot x,g'\cdot x$ for $g,g':\USymG$.
+  We have $g\cdot x=g' \cdot x$ if and only if $x = \inv{g} g'\cdot x$
+  if and only if $\inv{g} g'$ lies in $\USymG_x$.
+  \MB{Now apply \cref{xca:connected-trivia} yielding that that 
+  $G_x$ is trivial iff $\USymG_x$ is contractible.}
+\end{proof}
+
+The above results culminate in the following theorem.
+
+\begin{theorem}[Lagrange's Theorem]\label{thm:lagrange}
+\footnote{\MB{Replaces \cref{old:lagrange}.}}
+  %\cref{def:set-of-subgroups}
+  For all subgroups $(X,x,!):\Sub_G$, the $G_x$-set $\tilde G_x$ acts 
+  freely on the set $\USymG$, so all orbits under this action are
+  equivalent to $\USymG_x$ via 
+  $(\blank \cdot_{\tilde G_x} g): \USymG_x \equivto (G_x\cdot_{\tilde G_x} g)$
+  by \cref{lem:free-pt-char}.
+\end{theorem}
+
+\MB{Extra (exercise?).}
+The subgroup is given by $(X,x,!):\Sub_G$ with $X$ transitive,
+so the one and only orbit is $X(\sh_G)$. Using 
+\cref{lem:splitting into orbits} (equivalence $\settrunc{\blank}$),
+\cref{thm:orbitstab} (equivalence $(y,p)\mapsto(\sh_G,y,p,\refl{\sh_G})$),
+we get the following chain of equivalences:
+\[
+\USymG \equivto \bigl(\sum_{o:{\tilde G_x}/G_x} \inv{[o]} \bigr)
+\equivto \bigl(\sum_{p:(\tilde G_x)_{hG_x}} \inv{[\settrunc{p}]} \bigr)
+\equivto \bigl(\sum_{y:X(\sh_G)} \inv{[\settrunc{(\sh_G,y,!,\refl{\sh_G})}]} \bigr).
+\]
+Here $!$ is the proof of the proposition $[x] =_{X/G} [y]$,
+which exists since $X$ has only one orbit.
+Furthermore, $[\blank]: \USymG \to {\tilde G_x}/G_x$ is defined by
+$[g]\defeq \settrunc{(\sh_G,x,\trunc{\refl{(\sh_G,x)}},g)}$.
+Now, $\inv{[\settrunc{(\sh_G,y,!,\refl{\sh_G})}]}$ is easily
+identified with $\sum_{g:\USymG}((\sh_G,x)\eqto(\sh_G,y))$, so
+with $\USymG_x$ for all $y$ \MB{(only merely?)}. 
+Thus we get in total an equivalence
+from $\USymG$ to $X(\sh_G)\times\USymG_x$ \MB{(only merely?)}.
+
+
+
+
+
 
 \section{The classifying type is the type of torsors}
 \label{sec:torsors}
@@ -1735,7 +1800,7 @@ \section{The orbit-stabilizer theorem}
 In this way, the (abstract) $G$-type $X(\sh_G)$ splits as a disjoint union (i.e., a $\Sigma$-type over a set) of orbits,
 parametrized by the set of orbits:
 \begin{lemma}
-  \label{lem:splitting into orbits}
+  \label{old:splitting into orbits}
   The inclusions of the orbits induce an equivalence 
 \[
   \sum_{z : X / G} \mathcal O_z  \we X(\sh_G).
@@ -1774,7 +1839,7 @@ \section{The orbit-stabilizer theorem}
 We say that the action is \emph{free}\index{free $G$-type} if all stabilizer groups are trivial.
 
 \begin{theorem}[Orbit-stabilizer theorem]
-  \label{thm:orbitstab}
+  \label{old:orbitstab}
   Fix a $G$-type $X$ and a point $x : X(\sh_G)$.
   There is a canonical action $\tilde G : \BG_x \to \UU$,
   acting on $\tilde G(\sh_G)\equiv G$
@@ -1806,7 +1871,7 @@ \section{The orbit-stabilizer theorem}
 tells us that
 
 \begin{theorem}[Lagrange's Theorem]\footnote{insert that the action is free (referred to)}
-\label{thm:lagrange}
+\label{old:lagrange}
   If $H \to G$ is a subgroup, then $H$ has a natural action on $G$,
   and all the orbits under this action are equivalent.
 \end{theorem}