symmetry.tex

% Commented out BID 211116 \section{Cayley diagram}
% \label{sec:cayley-diagram}

% We have seen in the previous chapter how cyclic groups
% (those generated by a single generator)
% have neatly described torsors.

% In this section we shall generalize this story
% to groups $G$ generated by a
% (finite or just decidable)
% set of generators $S$.

% \tikzset{vertex/.style={circle,fill=black,inner sep=0pt,minimum size=4pt}}
% \tikzset{gena/.style={draw=casblue,-stealth}}
% \tikzset{genb/.style={draw=casred,-stealth}}

% \begin{figure}
%   \begin{sidecaption}%
%     {Cayley diagram for $S_3$ with respect to $S = \{(12),(23)\}$.}[fig:cayley-s3]
%   \centering
%   \begin{tikzpicture}
%     \pgfmathsetmacro{\len}{2}
%     \node[vertex,label=30:$(13)$]   (n13)  at (30:\len)  {};
%     \node[vertex,label=90:$(132)$]  (n132) at (90:\len)  {};
%     \node[vertex,label=150:$(12)$]  (n12)  at (150:\len) {};
%     \node[vertex,label=210:$e$]     (ne)   at (210:\len) {};
%     \node[vertex,label=270:$(23)$]  (n23)  at (270:\len) {};
%     \node[vertex,label=330:$(123)$] (n123) at (330:\len) {};
%     \begin{scope}[every to/.style={bend left=22}]
%       % generator a is (12)
%       \draw[gena] (ne)   to (n12);
%       \draw[gena] (n12)  to (ne);
%       \draw[gena] (n13)  to (n132);
%       \draw[gena] (n132) to (n13);
%       \draw[gena] (n123) to (n23);
%       \draw[gena] (n23)  to (n123);
%       % generator b is (23)
%       \draw[genb] (ne)   to (n23);
%       \draw[genb] (n23)  to (ne);
%       \draw[genb] (n13)  to (n123);
%       \draw[genb] (n123) to (n13);
%       \draw[genb] (n12)  to (n132);
%       \draw[genb] (n132) to (n12);
%     \end{scope}
%   \end{tikzpicture}
%   \end{sidecaption}
% \end{figure}

% $G \equiv \Aut(D_G) \to \Sym(\Card G)$

% \section{Actions}
% MOVED TO G-SETS BID 211116
% \label{sec:actions}

% \begin{definition}\label{action}
%   If $G$ is any (possibly higher) group and $A$ is any type of objects,
%   then we define an \emph{action} by $G$ in the world of elements of $A$ as a function
%   \[
%     X : \BG \to A.\qedhere
%   \]
% \end{definition}

% The particular object of type $A$ being acted on is $X(\pt):A$,
% and the action itself is given by transport.
% This generalizes our earlier definition of $G$-sets, $X : \BG \to \Set$.

% \begin{definition}\label{std-action}
%   The \emph{standard action} of $G$ on its designated shape $\shape_G$ is obtained by
%   taking $A \defeq \B G$ and $X \defeq \id_{\B G}$.
% \end{definition}

% \begin{example}
%   An action of $G$ on its set $\USym G$ of symmetries is provided by taking $X$ to be the principal torsor $\princ G$ as defined in
%   \cref{def:principaltorsor}.
% \end{example}

% Notice that the type $\BG \to A$ is equivalent to the type
% \[
%   \sum_{a:A}\hom(G,\Aut_A(a)),
% \]
% that is, the type of pairs of an element $a : A$,
% and a homomorphism from $G$ to the automorphism group of $A$.
% The equivalence maps $X:\BG\to A$ to the pair consisting of $X(\pt)$
% and the homomorphism represented by the pointed map arising
% from corestricting $X$ to factor through the component of $A$ containing $a$
% together with the trivial proof that this map takes $\pt:\BG$ to $a$.

% Because of this equivalence,
% we define a \emph{$G$-action on $a:A$}
% to be a homomorphism from $G$ to $\Aut_A(a)$.

% Many times we are particularly interested in actions on types,
% i.e., $A$ is a universe (or the universe of types-at-large):
% \[
%   X : \BG \to \UU.
% \]

% In this case, we define \emph{orbit type} of the action as
% \[
%   X_G \defeq \sum_{z:\BG} X(z),
% \]
% and the type of \emph{fixed points} as
% \[
%   X^G \defeq \prod_{z:\BG} X(z).
% \]
% The set of orbits is the set-truncation of the orbit type,
% \[
%   X / G \defeq \Trunc{X_G}_0.
% \]
% We say that the action is \emph{transitive} if $X / G$ is contractible.

% \section{Heaps \texorpdfstring{$(\dagger)$}{(\textdagger)}}
% \label{sec:heaps}

% Recall that we in \cref{rem:heap-preview} wondered about
% the status of general identity types $a=_A a'$,
% for $a$ and $a'$ elements of a groupoid $A$,
% as opposed to the more special loop types $a=_Aa$.\marginnote{%
%   This section has no implications for the rest of the book,
%   and can thus safely be skipped on a first reading.
%   (TODO: Move in place in \cref{ch:groups}?)}
% Here we describe the resulting algebraic structure
% and how it relates to groups.

% We proceed in a fashion entirely analogous to that of \cref{sec:typegroup},
% but instead of looking a pointed types, we look at \emph{bipointed types}.

% \begin{definition}\label{def:bipt-conn-groupoid}
%   The type of \emph{bipointed, connected groupoids} is the type
%   \[
%     \UUppone \defeq \sum_{A:\UU^{=1}}(A \times A).\qedhere
%   \]
% \end{definition}
% Recall that $\UU^{=1}$ is the type of connected groupoids $A$,
% and that we also write $A:\UU$ for the underlying type.
% We write $(A,a,a'):\UUppone$ to indicate the two endpoints.

% Analogous to the loop type of a pointed type,
% we have a designated identity type of a bipointed type,
% where we use the two points as the endpoints of the identifications:
% We set $\ISym(A,a,a') \defeq (a =_A a')$.

% \needspace{6\baselineskip}
% \begin{definition}\label{def:heap}
%   The type of \emph{heaps}\footnote{%
%     The concept of heap (in the abelian case)
%     was first introduced by Prüfer\footnotemark{}
%     under the German name \emph{Schar} (swarm/flock).
%     In Anton Sushkevich's book
%     \casrus{Теория Обобщенных Групп}
%     (\emph{Theory of Generalized Groups}, 1937),
%     the Russian term \casrus{груда} (heap)
%     is used in contrast to \casrus{группа} (group).
%     For this reason, a heap is sometimes
%     known as a ``groud'' in English.}%
%   \footcitetext{Pruefer-AG}
%   is a wrapped copy (\cf \cref{sec:unary-sum-types})
%   of the type of bipointed, connected groupoids $\UUppone$,
%   \[
%     \Heap \defeq \Copy_{\mkheap}(\UUppone),
%   \]
%   with constructor $\mkheap : \UUppone \to \Heap$.
% \end{definition}
% We call the destructor $\B : \Heap \to \UUppone$,
% and call $\BH$ the \emph{classifying type} of the heap $H \jdeq\mkheap\BH$,
% just as for groups,
% and we call the first point in $BH$ is \emph{start shape} of $H$,
% and the second point the \emph{end shape} of $H$.

% The identity type construction $\ISym : \UUppone \to \Set$
% induces a map $\USym : \Heap \to \Set$,
% mapping $\mkheap X$ to $\ISym X$.
% These are the \emph{underlying identifications} of the heaps.

% These is an obvious map (indeed a functor) from groups to heaps,
% given by doubling the point.
% That is, we keep the classifying type and use the designated shape
% as both start and end shape of the heap.
% In fact, this map lifts to the type of heaps with a chosen identification.
% \begin{exercise}\label{xca:group+torsor-heap}
%   Define natural equivalences $\Heap \weq \sum_{G:\Group}\BG$,
%   and $\Group \weq \sum_{H:\Heap}(\USym H)$.
% \end{exercise}
% Recalling the equivalence between $\BG$ and the type of $G$-torsors
% from~\cref{lem:BGbytorsor},
% we can also say that a heap is the same
% as a group $G$ together with a $G$-torsor.\footnote{%
%   But be aware that are \emph{two} such descriptions,
%   according to which endpoint is the designated shape,
%   and which is the ``twisted'' torsor.}
% It also follows that the type of heaps is a (large) groupoid.

% In the other direction,
% there are \emph{two} obvious maps (functors) from heaps to groups,
% taking either the start or the end shape to be the designated shape.

% Here's an \emph{a priori} different map from heaps to groups:
% For a heap $H$, consider all the
% symmetries of the underlying set of identifications $\USym H$
% that arise as $r \mapsto p\inv q r$ for $p,q\in \USym H$.

% Note that $(p,q)$ and $(p',q')$ determine the same symmetry
% if and only if $p\inv q = p'\inv{q'}$, and if and only if
% $\inv{p'}p = \inv{q'}q$.

% For the composition, we have $(p,q)(p',q') = (p\inv{q}p',q') = (p,q'\inv{p'}q)$.

% \begin{exercise}
%   Complete the argument that this defines a map
%   from heaps to groups. Can you identify the resulting group
%   with the symmetry group of the start or end shape?
%   How would you change the construction to get the other endpoint?
% \end{exercise}

% \begin{exercise}
%   Show that the symmetry groups of the two endpoints of a heap
%   are \emph{merely} isomorphic.

%   Define the notion of an \emph{abelian heap},
%   and show that for abelian heaps,
%   the symmetry groups of the endpoints are (\emph{purely}) isomorphic.
% \end{exercise}

% Now we come to the question of describing the algebraic structure
% of a heap.
% Whereas for groups we can define the abstract structure
% in terms of the reflexivity path and the binary operation of path composition,
% for heaps, we can define the abstract structure
% in terms of a \emph{ternary operation},
% as envisioned by the following exercise.

% \begin{exercise}\label{xca:heap-variety}
%   Fix a set $S$.
%   Show that the fiber $\inv{\USym}(S)\jdeq\sum_{H:\Heap}(S=\USym H)$ is a set.

%   Now fix in addition a ternary operation $t:S\times S\times S\to S$ on $S$.
%   Show that the fiber of the map $\Heap \to \sum_{S:\Set}(S\times S\times S \to S)$,
%   mapping $H$ to $(\USym H,(p,q,r)\mapsto p \inv{q} r)$,
%   at $(S,t)$ is a proposition,
%   and describe this proposition in terms of equations.
% \end{exercise}

% \section{Semidirect products}
% \label{sec:Semidirect-products}

% In this section we describe a generalization of the product of two group, called the {\em semidirect} product, which can be constructed from an
% action of a group on a group.  Like the product, it consists of pairs, both at the level of concrete groups and of abstract groups, as we shall
% see.

% We start with some preliminaries on paths between pairs.
% Lemma \cref{lem:isEq-pair=} above takes a simpler form when $y$ and $y'$ are values of a family $x \mapsto f(x)$
% of elements of the family $x \mapsto Y(x)$, as the following lemma shows.

% \begin{lemma}\label{lem:pathpairsection}
%   Suppose we are given a type $X$ and a family of types $Y(x)$ parametrized by the elements $x$ of $X$.
%   Suppose we are also given a function $f : \prod_{x:X} Y(x)$.
%   For any elements $x$ and $x'$ of $X$,
%   there is an equivalence of type
%   $$\left ( (x,f(x)) = (x',f(x')) \right ) \weq (x=x') \times (f(x) = f(x)),$$
%   where the identity type on the left side is between elements of $\sum_{x:X} Y(x)$.
% \end{lemma}

% \begin{proof}
%   By \cref{lem:isEq-pair=} and by composition of equivalences, it suffices to establish an equivalence of type
%   $$\left( \sum_{p:x=x'} \pathover {f(x)} Y p {f(x')} \right) \weq (x=x') \times (f(x) = f(x)).$$
%   Rewriting the right hand side as a sum over a constant family, it suffices to find an equivalence of type
%   $$\left( \sum_{p:x=x'} \pathover {f(x)} Y p {f(x')} \right) \weq \sum_{p:x=x'} (f(x) = f(x)).$$
%   By \cref{lem:fiberwise} it suffices to establish an equivalence of type
%   $$ \left( \pathover {f(x)} Y p {f(x')} \right) \weq (f(x) = f(x))$$
%   for each $p:x=x'$.  By induction on $x'$ and $p$ we reduce to the case where $x'$ is $x$ and $p$ is $\refl x$, and it suffices to establish an
%   equivalence of type
%   $$ \left( \pathover {f(x)} Y {\refl x} {f(x)} \right) \weq (f(x) = f(x)).$$
%   Now the two sides are equal by definition, so the identity equivalence provides what we need.
% \end{proof}

% The lemma above shows how to rewrite certain paths between pairs as pairs of paths.  Now we wish to establish the formula for composition of
% paths, rewritten in terms of pairs of paths, but first we introduce a convenient definition for the transport of loops in $Y(x)$ along paths in
% $X$.

% \begin{definition}\label{def:pathsectionaction}
%   Suppose we are given a type $X$ and a family of types $Y(x)$ parametrized by the elements $x$ of $X$.
%   Suppose we are also given a function $f : \prod_{x:X} Y(x)$.
%   For any elements $x$ and $x'$ of $X$ and for any identity $p : x = x'$, define a function $(f(x') = f(x')) \to (f(x) = f(x))$, to be denoted
%   by $q' \mapsto {q'} ^ p$, by induction on $p$ and $x'$, reducing to the case where $x'$ is $x$ and $p$ is $\refl x$, allowing us to
%   set ${q'} ^{ \refl x } \defeq q'$.
% \end{definition}

% We turn now to associativity for the operation just defined.

% \begin{lemma}\label{def:pathsectionactionassoc}
%   Suppose we are given a type $X$ and a family of types $Y(x)$ parametrized by the elements $x$ of $X$.
%   Suppose we are also given a function $f : \prod_{x:X} Y(x)$.
%   For any elements $x$, $x'$, and $x''$ of $X$, for any identities $p : x = x'$ and $p' : x' = x''$,
%   and for any $q : f x'' = f x''$,
%   there is an identification of type $ ( q ^{ p' }) ^ p = q ^{( p' \cdot p )}$.
% \end{lemma}

% \begin{proof}
%   By induction on $p$ and $p'$, it suffices to show that $ ( q ^{ \refl y }) ^ { \refl y } = q ^{( \refl y \cdot \refl y )}$, in which both sides are
%   equal to $q$ by definition.
% \end{proof}

% Observe that the operation depends on $f$, but $f$ is not included as part of the notation.

% The next lemma contains the formula we are seeking.

% \begin{lemma}\label{lem:pathpairsectionmult}
%   Suppose we are given a type $X$ and a family of types $Y(x)$ parametrized by the elements $x$ of $X$.
%   Suppose we are also given a function $f : \prod_{x:X} Y(x)$.
%   For any elements $x$, $x'$, and $x''$ of $X$, and for any two identities $e : (x,f(x)) = (x',f(x'))$ and $e' : (x',f(x')) = (x'',f(x''))$,
%   if $e$ corresponds to the pair $(p,q)$ with $p : x = x'$ and $q : f x = f x$ under the equivalence of \cref{lem:pathpairsection},
%   and $e'$ corresponds to the pair $(p',q')$ with $p' : x' = x''$ and $q' : f x' = f x'$,
%   then $e' \cdot e$ corresponds to the pair $(p' \cdot p , ({q'} ^ p) \cdot q)$.
% \end{lemma}

% \begin{proof}
%   By induction on $p$ and $p'$ we reduce to the case where $x'$ and $x''$ are $x$ and $p$ and $p'$ are $\refl x$.
%   It now suffices to show that $e' \cdot e$ corresponds to the pair $(\refl x , q' \cdot q)$.
%   Applying the definition of the map $\Phi$ in the proof of \cref{lem:isEq-pair=} to our three pairs, we see that it suffices to show that
%   $\left( \apap g {\refl x} {q'} \right) \cdot \left( \apap g {\refl x} {q} \right) = \apap g {\refl x} {q' \cdot q}$, with $g$, as there, being the function $ g(x)(y) \defeq (x,y)$.
%   By \cref{def:applfun2comp} it suffices to show that $\left( \ap {g(x)} {q'} \right) \cdot \left( \ap {g(x)} {q} \right) = \ap {g(x)} {(q' \cdot q)}$, which follows from
%   compatibility of $\ap {g(x)}$ with composition, as in \cref{lem:apcomp}.
% \end{proof}

% The lemma above will be applied mostly in the case where $x'$ and $x''$ are $x$, but if it had been stated only for that case, we would not have
% been able to argue by induction on $p$ and $p'$.

% \begin{definition}\label{def:semidirect-product}
%   Given a group $G$ and an action $\tilde H : \BG \to \typegroup$ on a group $H \defeq \tilde H(\shape_G)$, we define a group called the {\em
%     semidirect product} as follows.
%   $$G \ltimes \tilde H \defeq \mkgroup { \sum_{t:\BG} \B \tilde H(t) }$$
%   Here the basepoint of the sum is taken to be the point $(\shape_G,\shape_H)$.
%   (We deduce from \cref{lem:level-n-utils}, \cref{level-n-utils-sum}, that $\sum_{t:\BG} \B \tilde H(t)$ is a groupoid.
%   See \cref{lem:UNKNOWN} for a proof that $\sum_{t:\BG} \B \tilde H(t)$ is connected.)
% \end{definition}

% Observe that if the action of $G$ on $H$ is trivial, then $\tilde H(t) \jdeq H$ for all $t$ and $G \ltimes \tilde H \jdeq G \times H$.

% Projection onto the first factor gives a homomorphism $p \defeq \mkgroup \fst : G \ltimes \tilde H \to G$.
% Moreover, there is a homomorphism $s : G \to G \ltimes \tilde H$ defined by
% $ s \defeq \mkgroup {\left( t \mapsto (t,\shape_{\tilde H(t)}) \right) }$, for $t : \B G$.
% The two maps are homomorphisms because they are made from basepoint-preserving maps.
% The map $s$ is a \emph{section} of $p$ in the sense the $p \circ s = \id_G$.
% There is also a homomorphism $j : H \to G \ltimes \tilde H$ defined by $j \defeq \mkgroup { \left( u \mapsto (\shape_G,u) \right) }$, for $u : \B H$.

% \begin{lemma}
%   The homomorphism $j$ above is a monomorphism, and it gives the same (normal) subgroup of $G \ltimes \tilde H$ as the kernel $\ker p$ of $p$.
% \end{lemma}

% \begin{proof}
%   See \ref{def:kernel} for the definition of kernel.  According to \cref{lem:fst-fiber(a)=B(a)}, the map $\B H \to (\B p)^{-1}(\shape_G)$ defined by
%   $ u \mapsto ((\shape_G,u), \refl{\shape_G}) $ is an equivalence.  This establishes that the fiber $(\B p)^{-1}(\shape_G)$ is connected and thus serves as
%   the classifying type of $\ker p$.  Pointing out that the composite map $H \xrightarrow{\isom} \ker p \to G \ltimes \tilde H$ is $j$ and using
%   univalence to promote the equivalence to an identity gives the result.
% \end{proof}

% Our next goal is to present the explicit formula for the multiplication operation in $\USym { G \ltimes \tilde H }$.
% First we apply \cref{lem:pathpairsection} to get a bijection $\USym { G \ltimes \tilde H } \weq \USym G \times \USym H$.
% Now use that to transport the multiplication operation of the group $\USym { G \ltimes \tilde H }$ to the set $\USym G \times \USym H$.
% Now \cref{lem:pathpairsectionmult} tells us the formula for that transported operation is given as follows.
% $$ (p',q') \cdot (p,q) = (p' \cdot p , ({q'} ^ p) \cdot q) $$
% In a traditional algebra course dealing with abstract groups, this formula is used as the definition of the multiplication operation
% on the set $\USym G \times \USym H$, but then one must prove that the operation satisfies the properties of \cref{def:abstractgroup}.
% The advantage of our approach is that the formula emerges from the underlying logic that governs how composition of paths works.

\section{The orbit-stabilizer theorem}
\label{sec:orbit-stabilizer-theorem}


Let $G$ be a group (or $\infty$-group) and  $X : \BG \to \UU$  a $G$-type.
Recall the orbit type of \cref{def:orbittype} $X_{hG}\defequi
\sum_{z:\BG}X(z)$ and its truncation, the set of orbits $X / G \defeq \Trunc{X_{hG}}_0$ and the map $X(\shape_G)\to X_{hG}$ sending $x:X(\shape_G)$ to $[x]\defequi (\shape_G,x)$.


For an element $x:X/G$ consider the associated subtype of $X(\shape_G)$ consisting of
 all $y : X(\shape_G)$ so that $|[y]|$ is equal to $x$ in the set of orbits:
\[
  \mathcal O_{x} \defeq \sum_{y : X(\shape_G)} x =_{X/G} |[y]|.
\]
 For a point $x : X(\shape_G)$, we call $G\cdot x \defeq \mathcal O_{|[x]|}$ 
 the \emph{orbit through $x$}\index{orbit through $x$}.
 % as the subtype of $X(\shape_G)$ consisting of
%  all $y : X(\shape_G)$ so that $[y]$ is equal to $[x]$ in the set of orbits:
% \[
%   G\cdot x \defeq \mathcal O_{[x]} \defeq \sum_{y : X(\shape_G)} [x] =_{X/G} [y].
% \]
Note the (perhaps) unfortunate terminology: an ``orbit'' is not an element in the
orbit type, but rather consists of all the elements in $X(\shape_G)$ sent to a given element in the orbit set.
% Also note that the orbit $G\cdot x\defeq \mathcal O_x$ only depends on the image of $x$ in the set $X/G$ of orbits,
% thus justifying the names.

In this way, the (abstract) $G$-type $X(\shape_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}
  The inclusions of the orbits induce an equivalence 
\[
  \sum_{z : X / G} \mathcal O_z  \we X(\shape_G).
\]
\end{lemma}

The \emph{stabilizer group}\index{stabilizer group}
(also known as the \emph{isotropy group}\index{isotropy group}) of
$x : X(\shape_G)$ is the automorphism group of $[x]$ in the orbit type
$$G_x\defequi\Aut_{X_{hG}}([x]),$$
so that
$X_{hG}$ is equivalent to the disjoint union $\sum_{z:X/G}(\BG_x)_\div$.

%The \emph{stabilizer group}\index{stabilizer group}
%(also konwn as the \emph{isotropy group}\index{isotropy group}) of
%$x : X(\shape_G)$ is the automorphism group of $[x]$ in the orbit type
%$$G_x\defequi\Aut_{X_{hG}}([x]).$$

  For $x:X(\shape_G)$ the restriction of the first projection $\fst:X_{hG}\to\BG$ to the component of $[x]$ gives a homomorphism $i_x:\Hom(G_x,G)$ if we point it by $\refl{\shape_G}:\shape_G=\fst([x])$.

  Recall that if $H$ and $G$ are groups, the set of homomorphisms $\hom(H,G)$ is a $G$-set.  In particular, if $g:\shape_G=\shape_G$ and $f:\hom(H,G)$, then we can denote the result of letting $g$ act on $f$ by $f^g:\hom(H,G)$ which has $\B(f^g)_\div\defequi\Bf$, but is pointed by $p_fg^{-1}:\shape_G=\Bf_\div(\shape_H)$ (i.e., precomposing the witness $p_f:\shape_G=f(\shape_H)$ with the inverse of $g$).  In the case where $f$ was a monomorphism so that it defines a subgroup, we called $f^g$ the conjugate of the original subgroup.
  
 If $g:\shape_G=\shape_G$ the identity map of $X_{hG}$ can be pointed by the identity between $(\shape_G,x) $ and $(\shape_G,gx)$ given by $g:\shape_G=\shape_G$ and $\refl{gx}$ to give an isomorphism from $G_x$ to $G_{gx}$ identifying (by univalence) the homomorphism $i_{gx}:\hom(G_{gx},G)$ with $i^{g^{-1}}_x:\hom(G_x,G)$.


In the case where $X$ is a $G$-\emph{set}, the homomorphism $i_x:\hom(G_x,G)$ is a monomorphism, and with this extra information we consider $G_x$ as a subgroup of $G$.
Thus, different points in the same orbit of $X(\shape_G)$ have conjugate stabilizer subgroups.

Another way of formulating these ideas is to consider the $G$-type
$$\mathcal O_x\colon\BG\to\UU,\qquad\mathcal O_x(z)\defequi\sum_{y:X(z)}|[x]|=_{X/G}|(z,y)|,
$$
and obtain the alternative definition of $\BG_x$ as $\sum_{z:\BG}\mathcal O_x(z)$, which we see is a subgroup exactly when $\mathcal O_x$ is a $G$-set.

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}
  Fix a $G$-type $X$ and a point $x : X(\shape_G)$.
  There is a canonical action $\tilde G : \BG_x \to \UU$,
  acting on $\tilde G(\shape_G)\equiv G$
  with orbit type $\tilde G_{hG_x} \equiv \mathcal O_x$.
\end{theorem}
\begin{proof}
  Define $\tilde G(x,y,!) \defeq (\shape_G = x)$.
\end{proof}

Now suppose that $G$ is a $1$-group acting on a set.
We see that the orbit type is a set
(and is thus equivalent to the set of orbits)
if and only if
all stabilizer groups are trivial,
\ie if and only if the action is free.

If $G$ is a $1$-group,
then so is each stabilizer-group,
and in this case (of a set-action),
the orbit-stabilizer theorem
tells us that

\begin{theorem}[Lagrange's Theorem]\footnote{insert that the action is free (referred to)}
\label{thm: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}

% Interaction with cardinality: if G acts freely on S, then card(S/G) = card(S)/card(G)

\section{The isomorphism theorems}
\label{sec:noether-theorems}

Cf.~\cref{sec:stuff-struct-prop}

Group homomorphisms provide examples of forgetting stuff and structure.
For example, the map from cyclically ordered sets with cardinality $n$
to the type of sets with cardinality $n$ forgets structure,
and represents an injective group homomorphism from the cyclic
group of order $n$ to the symmetric group $\Sigma_n$.

And the map from pairs of $n$-element sets to $n$-element sets
that projects onto the first factor clearly forgets stuff,
namely, the other component.
It represents a surjective group homomorphism.

More formally, fix two groups $G$ and $H$,
and consider a homomorphism $\varphi$ from $G$ to $H$,
considered as a pointed map $\B\varphi : \BG \to_\pt \BH$.
Then $\B\varphi$ factors as
\begin{align*}
  \BG
  = &\sum_{w:\BH}\sum_{z:\BG}(\B\varphi(z)=w)\\
  \to_\pt &\sum_{w:\BH}\;\Trunc[\Big]{\sum_{z:\BG}(\B\varphi(z)=w)}_0\\
  \to_\pt &\sum_{w:\BH}\;\Trunc[\Big]{\sum_{z:\BG}(\B\varphi(z)=w)}_{-1} = \BH.
\end{align*}
The pointed, connected type in the middle represents a group
that is called the \emph{image} of $\varphi$, $\Img(\varphi)$.


(FIXME: Quotient groups as automorphism groups, normal subgroups/normalizer, subgroup lattice)

\begin{lemma}
  \label{lem:aut-orbit}
  The automorphism group of the $G$-set $G/H$ is isomorphic to $\N_G(H)/H$.
\end{lemma}

\begin{theorem}[Fundamental Theorem of Homomorphisms]
  \label{thm:fund-thm-homs}
  For any homomorphism $f : \Hom(G,G')$
  the map {\color{blue} TODO} defines an isomorphism
  $G/\ker f \simeq \im f$.\footnote{TODO: Fix and move to Ch. 5}
\end{theorem}

\section{(the lemma that is not) Burnside's lemma}
\label{sec:burnsides-lemma}
\label{lem:burnsides-lemma}

\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),
  \]
  where $X^g = \setof{x:X}{gx=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$.
  Hence the set of orbits is a finite set as well.

  Consider now the set $R \defeq \sum_{g:\El G} 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,
  \]
  where the last step writes $X$ as a union of orbits.
  Within each orbit $\mathcal O_z$,
  the stabilizer groups are conjugate,
  and thus have the same finite cardinality,
  which from the orbit-stabilizer theorem (\cref{thm:orbitstab}),
  is the cardinality of $G$ divided by the cardinality of $\mathcal O_z$.
  We conclude that $\Card(R) = \Card(X/G)\Card(G)$, as desired.
\end{proof}

% Where does this go?!
\section{More about automorphisms}
\label{sec:automorphisms}

% Written to record somewhere the results of a discussion with Bjorn
For every group $G$ (which for the purposes of the discussion
in this section we allow to be a higher group)
we have the automorphism group $\Aut(G)$.
This is of course the group of self-identifications $G = G$ in the type of groups, $\Group$.
If we represent $G$ by the pointed connected classifying type $\BG$,
then $\Aut(G)$ is the type of pointed self-equivalences of $\BG$.

We have a natural forgetful map from groups to the type of connected groupoids.
Define the type $\Bunch$ to be the type of all connected groupoid.
If $X:\Bunch$, then all the elements of $X$ are merely isomorphic,
that is, they all look alike,
so it makes sense to say that $X$ consists of a \emph{bunch} of alike objects.

For every group $G$ we have a corresponding bunch, $\BG_\div$,
\ie{} the collection of $G$-torsors,
and if we remember the basepoint $\shape_G : \BG_\div$,
then we recover the group $G$.
Thus, the type of groups equivalent to the type
$\sum_{X : \Bunch} X$
of pairs of a bunch together with a chosen element.
(This is essentially our definition of the type $\Group$.)

Sometimes we want to emphasize that we $\BG_\div$ is a bunch,
so we define $\bunch(G) \defeq \BG_\div : \Bunch$.

\begin{definition}[The center as an abelian group]
  \label{def:center}
  Let
  $$Z(G) \defeq \prod_{z : \BG}(z = z)$$ denote the type of fixed points of the adjoint action of $G$ on itself.
  This type is equivalent to the automorphism group of the identity on $\bunch(G)$,
  and hence the loop type of
  \[
    \B Z(G) \defeq \sum_{f : \BG \to \BG} \merely{f \sim \id}.
  \]
  This type is itself the loop type of the pointed, connected type
  \[
    \B^2Z(G) \defeq \sum_{X : \Bunch}\Trunc{\bunch(G) = X}_0,
  \]
  and we use this to give $Z(G)$ the structure of an \emph{abelian} group,
  called the \emph{center} of $G$.
\end{definition}
There is a canonical homomorphism from $Z(G)$ to $G$ given by the pointed map
from $\B Z(G)$ to $\BG$ that evaluates at the point $\shape_G$.
The fiber of the evaluation map $e : \B Z(G) \to_\pt \BG$ is
\begin{align*}
  \fiber_e(\shape_G)
  &\jdeq \sum_{f : \BG \to \BG} \merely{f \sim \id} \times (\mathop f \shape_G = \shape_G) \\
  &\equiv \sum_{f : \BG \to_\pt \BG} \merely{f \sim \id},
\end{align*}
and this type is the loop type of the pointed, connected type
\[
  \B\Inn(G) \defeq \sum_{H : \Group} \Trunc{\bunch(G) = \bunch(H)}_0,
\]
thus giving the homomorphism $Z(G)$ to $G$ a normal structure with
quotient group $\Inn(G)$, called the \emph{inner automorphism group}.

Note that there is a canonical homomorphism from $\Inn(G)$ to $\Aut(G)$
given by the pointed map $i : \B\Inn(G) \to \B\Aut(G)$ that forgets the component.
On loops, $i$ gives the inclusion into $\Aut(G)$ of the subtype of automorphisms of $G$
that become merely equal to the identity automorphism of $\bunch(G)$.
The fiber of $i$ is
\begin{align*}
  \fiber_i(\shape_G)
  &\jdeq \sum_{H : \Group} \Trunc{\bunch(G) = \bunch(H)}_0 \times (H = G) \\
  &\equiv \Trunc{\bunch(G) = \bunch(G)}_0.
\end{align*}
This is evidently the type of loops in the pointed, connected groupoid
\[
  \B\Out(G) \defeq \Trunc*{\sum_{X : \Bunch}\merely{\bunch(G) = X}}_1,
\]
thus giving the homomorphism $\Inn(G)$ to $\Aut(G)$ a normal structure with
quotient group $\Out(G)$, called the \emph{outer automorphism group}.
Note that $\Out(G)$ is always a $1$-group,
and that it is the decategorification of $\Aut(\bunch(G))$.

\begin{theorem}
  Let two groups $G$ and $H$ be given.
  There is a canonical action of $\Inn(H)$
  on the set of homomorphisms from $G$ to $H$, $\Trunc{\BG \to_\pt \BH}_0$.
  This gives rise to an equivalence
  \[
    \Trunc{\BG_\div \to \BH_\div}_0 \equiv \Trunc*{\left(\Trunc{\BG \to_\pt \BH}_0\right) _{h\Inn(H)}}_0
  \]
  between the set of maps from $\bunch(G)$ to $\bunch(H)$ and the set of
  components of the orbit type of this action.
\end{theorem}
\begin{proof}
  We give the action by defining a type family $X : \B\Inn(H) \to \UU$ as follows
  \[
    X\, \angled{K,\phi} \defeq \Trunc{\Hom(G,K)}_0 \jdeq \Trunc{\BG \to_\pt \BK}_0,
  \]
  for $\angled{K,\phi} : \B\Inn(H) \jdeq \sum_{K : \Group} \Trunc{\bunch(H) = \bunch(K)}_0$.
  Now we can calculate
  \begin{align*}
    \Trunc{X_{\Inn(H)}}_0
    &\jdeq \Trunc*{\sum_{K:\Group}\Trunc{\bunch(H)=\bunch(K)}_0\times\Trunc{\Hom(G,K)}}_0 \\
    &\equiv \Trunc*{\sum_{K:\Group}(\bunch(H)=\bunch(K))\times\Hom(G,K)}_0 \\
    &\equiv \Trunc*{\sum_{K:\Bunch}\sum_{k:K}(\bunch(H)=K)\times\sum_{f:\bunch(G)\to K)}\mathop f \pt = k}_0 \\
    &\equiv \Trunc*{\sum_{K:\Bunch} (\bunch(H)=K) \times(\bunch(G) \to K)}_0 \\
    &\equiv \Trunc*{\bunch(G)\to\bunch(H)}_0 \jdeq \Trunc*{\BG_\div \to \BH_\div}_0.\qedhere
  \end{align*}
\end{proof}

% \section{Orbit type as a groupoid completion(*)}
%deleted BID 211116
% \emph{This is a somewhat advanced topic that should occur much later, if at all.}

% \bigskip

% Suppose $G$ is a group acting on a groupoid $X$,
% given by a map $X : \BG \to_\pt \B\!\Aut(X_0)$,
% with $e_X : X(\pt) = X_0$.
% By induction on $e_X$ we may assume that $X_0\jdeq X(\pt)$
% and $e_X\jdeq\refl{}$.

% We have the orbit type $X_{hG} \jdeq \sum_{T:\BG}X(T)$.
% We think of this as identifying elements of $X_0$
% that are in the same orbit,
% in the sense that there are new identifications of $x$ and $y$
% for group elements $g$ with $g\cdot x = y$.

% In this section we study one way of making this intuition precise.

% Consider the pregroupoid $C_G(X)$ with object type $X_0$ and morphism sets
% \[
%   \hom(x,y) \defeq \sum_{g:G}(g\cdot x = y),
% \]
% where $g\cdot x \defeq g_*(x)$. The identity at $x$ is
% $(1,\id)$, while the composite of $(g,p):\hom(x,y)$ with
% $(h,q):\hom(y,z)$ is $(hg,r)$, where $r$ is built from $p$ and $q$ as
% follows:
% \[
%   hg \cdot x = h\cdot(g\cdot x) = h\cdot y = z.
% \]

% We have a functor of pregroupoids $F: C_G(X) \to X_{hG}$
% defined on objects by
% $F(x) := (\pt,x)$ and on morphisms $(g,p):\hom(x,y)$ by $F(g,p) :=
% (g,p)^=$.

% This functor is essentially surjective on objects (by connectivity of
% $\BG$) and fully faithful by the characterization of paths in
% $\sum$-types. Hence it induces an equivalence from the completion of
% $C_G(X)$ to $X_{hG}$.

% As a corollary, the orbit set $X/G \jdeq \Trunc{X_{hG}}_0$,
% is the set quotient of $X_0$ modulo the equivalence relation
% $x \sim y \defeq \exists g:G, g\cdot x = y$.

%%% Local Variables:
%%% mode: latex
%%% fill-column: 144
%%% TeX-master: "book"
%%% End: