subgroups.tex

\chapter{Subgroups}
\label{ch:subgroups}

\section{Subgroups}
\label{sec:subgroups}
In our discussion of the group $\ZZ=\aut_{S^1}(\base)$ of integers in we discovered that the ``subsymmetries'' formed a very organized structure.
For each natural number $n$ we obtained a set of subsymmetry the entire identity type $\base=\base$, namely the set of all the iterates $(\Sloop^{n})^m$ where $m$ varies over the integers.
When $n$ was positive this was realized as the $n$-fold \covering of $S^1$, when $n=0$ this was given by the universal \covering.

For other groups the ``subsymmetries'' form more involved structures.
One thing is that our concept of a subtype of $B$ is merely the first projection $\sum_{b:B}P(b)\to B$, where the $P$ is a family of propositions.
Another thing is that for group the ``sub'' refers to the associated abstract groups, so that ``$BH$ is a subgroup of $BG$'' should \emph{not} mean that ``$BH$ is a subtype of $BG$'', but that we have a group homomorphism $f:\Hom(H,G)$ so that the induced function $(\pt_H=\pt_H)\to(\pt_G=\pt_G)$ is an ``inclusion of a subset''.
In other words, we must have that $f$ is a ``monomorphism'' (see \cref{lem:injofsetsaremono}).


The other extreme of the idea of ``subsymmetries'' was exposed in \cref{sec:groupssubperm} in the form of the slogan ``any symmetry is a symmetry of $\Set$''.
By this we meant that, if $G=\aut_A(a)$ is a group, we produced a monomorphism $\rho_G:\Hom(\aut_a(A),\aut_{a=a}(\Set))$, \ie any symmetry of $a$ is uniquely given by a symmetry (``permutation'') of the set $a=a$.


Now, as we saw in \cref{lem:injofsetsaremono}, that   $f:\Hom(H,G)$ is a monomorphism is equivalent to saying that $f:(\pt_H=\pt_H)\to(\pt_G=\pt_G)$ is an injection (preimages are propositions) which again is equivalent to the preimages of $Bf:BH\to BG$ being sets.
We must choose one of these equivalent formulations for our concept of ``subgroup'', but will move freely between them as may be convenient in a particular case.
%Hence we get the following neat formulation.
    \begin{definition}
      \label{def:subgroup}
      Let $G$ be a group.  
      The \emph{type of subgroups of $G$}\index{type!subgroup} is the type
      $$\typesubgroup_G\defequi\sum_{H:\typegroup}\sum_{f:\Hom(H,G)}\isset(Bf^{-1}(\pt_G)).$$
       A subgroup $(H,f,!)$ is
      \begin{enumerate}
      \item \emph{trivial}\index{trivial subgroup} if $BH$ is contractible
      \item \emph{proper}\index{proper subgroup} if $Bf$ is not an equivalence.
      \end{enumerate}
    \end{definition}
    \begin{remark}
      \label{rem:notationsubgroup}
      A note on notation is in order.  
If $(H,i,!)$ is a subgroup of a group $G$, tradition often permits us to relax the burden of notation; we may write ``a subgroup $i:H\subseteq G$'', or, if we don't need the name of $i:\Hom(H,G)$ in what follows, simply ``a subgroup $H\subseteq G$'' or ``a subgroup $H$ of $G$''.
    \end{remark}

\begin{lemma}
  \label{lem:setofsubgroups}
  If $G$ is a group, then the type $\typesubgroup_G$ of subgroups is a set.
\end{lemma}
\begin{proof}
An identity between two subgroups $i_H:H\subseteq G$ and $i_{H'}:H'\subseteq G$ is an identity $p:H'=_{\typegroup}H$ such that $i_{H'}=i_H\,p$ (a proposition since $\Hom(H',G)$ is a set).
  By univalence and \cref{lem:eqofconntypes}, the identity type $H=H'$ is equivalent to the set 
$$\sum_{f:\Hom(H,H')}\isEq(f^=:(\pt_H=\pt_H)\to(\pt_{H'}=\pt_{H'})).$$  
%If $(H,i_H,!)$ is a subgroup of $G$, then
Consequently, the identity type
$(H,i_H,!)=_{\typesubgroup_G}(H,i_H,!)$ is equivalent to the type of homomorphisms $f:\Hom(H,H)$ which are such that $!:i_H^==i_H^=f^=$ and such that $f^=$ is an equivalence (as we see in a moment this last requirement is redundant).  
Now, since $(H,i_H,!)$ is a subgroup, $i_H^=$ is an injection of sets, which forces $!:f^==\refl{\pt_H=\pt_H}$, which ultimately forces $f$ to be (identical to) the identity homomorphism. 
\end{proof}
Not only is the type of subgroups  of $G$ a set, it is in a natural way (equivalent to the value at $\pt_G$ of) a $G$-set which we denote by the same name
$$%\typesubgroup_G:BG\to\Set,\qquad 
\typesubgroup_G(y)\defequi \sum_{H:\typegroup}\sum_{f:\Hom(H,G)(y)}\isset(Bf^{-1}(\pt_G)),$$
where  as in \cref{ex:HomHGasGset}  
$$\Hom(H,G)(y)\defequi\sum_{F:BH_\div\to BG_\div}(y=F(\pt_H))$$
is the $G$-set of homomorphisms from $H$ to $G$.
% In this interpretation, $(H,F,p,!):\typesubgroup_G(\pt_G)$ represents a subgroup of $G$ (so that $p:\pt_G=F(\pt_H)$).  An identity $g:\pt_G=\pt_G$ acts on $\typesubgroup_G(\pt_G)$ by sending $(H,F,p,!)$ to $(H,F,p\,g^{-1},!)$.

\begin{definition}
  \label{def:conjactonsubgroups}
  If $G$ is a group, then the action of $G$ on the set of subgroups is called \emph{conjugation}. 


  \label{def:conjugate}
  If $(H,F,p,!):\typesubgroup_G(\pt_G)$ is a subgroup of $G$ and $g:\pt_G=\pt_G$, then the subgroups  $(H,F,p,!),(H,F,p\,g^{-1},!):\typesubgroup_G(\pt_G)$ are said to be \emph{conjugate}\index{conjugate}. 
\end{definition}
\begin{remark}
  \label{rem:whyconjugate}
  The term ``conjugation'' may seem confusing as the %(abstract) 
action of $g:\pt_G=\pt_G$ on a subgroup $(H,F,p,!):\typesubgroup_G(\pt_G)$ (where $p:x=F(\pt_H)$) is simply $(H,F,p\,g^{-1},!)$, which does not seem much like conjugation.  
However, as we saw in \cref{ex:abstrandconj}, under the equivalence $\abstr:\Hom(H,G)\we\Hom^\abstr(\abstr(H),\abstr(G))$, the corresponding action on $\Hom^\abstr(\abstr(H),\abstr(G))$ is exactly (postcomposition with) conjugation $c^g:\abstr(G)=\abstr(G)$.  
\footnote{The same phenomenon appeared in \cref{xca:HomZGvsAdG} where we gave an equivalence between the $G$-sets $\Hom(\ZZ,G)$ and $\Ad_G$ (where the action is very visibly by conjugation).}
% \end{remark}

% \begin{remark}
  \label{rem:conjactiononsubgroups}
 %  It is worthwhile to study this action a bit further.  Let $(H,f,!)$ be a subgroup of $G$ and let $g:\pt_G=\pt_G$.  We can trade $f$ for $\abstr(f):\Hom^\abstr(\abstr(G),\abstr(H))$ whose underlying set map is the injection $Bf^=:(\pt_H=\pt_H)\to(\pt_G=\pt_G)$. %We allow ourselves to write ``$f$'' instead of $Bf^=$. 
% As we saw in \cref{ex:abstrandconj}, the action of $g$ postcomposes with conjugation $c^g:(\pt_G=\pt_G)=(\pt_G=\pt_G)$.
% Hence, if we represent a subgroup as 
% $$(H,\phi,!):\sum_{H:\typegroup}\sum_{\phi:\Hom^\abstr(\abstr(H),\abstr(G))}\isprop(\phi^{-1}(e_G)),$$ then
% $g\cdot(H,\phi,!)=(H,c^g\,\phi,!)$.

% Now, if $g$ comes from $H$, say, $\i_H(h)$
\end{remark}
Summing up the remark:
\begin{lemma}
  \label{lem:conjugationabstractly}
  Under the equivalence of \cref{lem:actionsconcreteandabstract} between $G$-sets and $\abstr(G)$-sets, the $G$-set $\typesubgroup_G$ corresponds to the $\abstr(G)$-set
$$\sum_{H:\typegroup}\sum_{\phi:\Hom^\abstr(\abstr(H),\abstr(G))}\isprop(\phi^{-1}(e_G))$$ of abstract subgroups of $\abstr(G)$, with action $g\cdot(H,\phi,!)\defequi(H,c^g\,\phi,!)$ for $g:\abstr(G)$, where  $c^g:\abstr(G)=\abstr(G)$ is conjugation as defined in \cref{ex:conjhomo}.
\end{lemma}


\begin{remark}
  If you're familiar with the set-theoretic flavor of things, you know that it is important to distinguish between subgroups and injective group homomorphisms.  
Our use of ``subgroup'' can be defended as follows.  
It corresponds in set-theoretic language to saying that a subgroup is an injective homomorphism \emph{modulo} the relation forcing that precomposing with an isomorphism yields identical subgroups.  
Set-theory offers the luxury of having a representative in every equivalence class: namely the image of the injection, type theory does not.
\end{remark}

\sususe{The geometry of subgroups: some small examples}
\label{smallsubgpex}

As a teaser, and in order to get a geometric feel for the subgroups and their intricate interplay, it can be useful to have some fairly manageable examples to stare at.  
Some of the main tools for analyzing the geometry of subgroups are collected in \cref{sec:fingp} on finite groups, and we hope the reader will be intrigued by our mysterious claims and go on to study \cref{sec:fingp}.
That said, the examples we'll present are possible to muddle through by hand without any fancy machinery, but brute force is generally not an option and even for the present examples it is not something you want to show publicly.

When presenting the subgroups of a group $G$, three types are especially revealing: the set of subgroups $\typesubgroup_G(\pt_G)$, the \emph{groupoid of subgroups} $\typesubgroup(G)\defequi\sum_{y:BG}\typesubgroup_G(y)$ and what we for now call the ``set of normal subgroups'' $\prod_{y:BG}\typesubgroup_G(y)$.   Our local use of ``normal subgroup'' is equivalent to the official definition to come.  

The first projection $\typesubgroup(G)\to BG$ is referred to as the \emph{\covering of subgroups}.

\footnote{Write out and fix the concrete examples (cyclic groups and $\Sigma_3$) commented out}
% \begin{remark}
% In  \cref{cha:circle} we studied the subgroups of the group of integers $G=\ZZ$ through \coverings over the circle $S^1$ (which we showed was equivalent to $B\ZZ$).
% We discovered a subgroup $n\ZZ$ for each natural number $n:\NN$ and in the groupoid $\typesubgroup({\ZZ})$ these sit as elements in separate components.  Each of these components are contractible (because addition is commutative: $\ZZ$ is an abelian group).

% In general, a component $K$ of the groupoid $\sum_{y:BG}\typesubgroup_G(y)$ of subgroups of a group $G$ may be much more interesting. For one thing the, $K$ can contain many subgroups in the sense that the preimage of the first projection $K\to BG$ is a set that may have many different elements; each representing a subgroup.  However, this set of subgroup will be a \emph{conjugacy class} of subgroups: the different subgroups are related by the conjugation action of $G$.  

% If $G$ is abelian this action is trivial, and $\sum_{y:BG}\typesubgroup_G(y)$ consists of contractible components indexed over the subgroups of $G$.  Otherwise different subgroups may live in the same component of the groupoid of subgroups -- we'll see examples in a moment.

% In addition, the components will not in general be contractible, revealing the symmetries of the subgroups under the conjugation action.
% \end{remark}


% \begin{example}
%   The trivial group only has itself as a subgroup; the groupoid of subgroups and the set of normal subgroups are singletons.
% \end{example}
% \begin{example}
%   The cyclic group $C_p$ of prime order $p$ has only two subgroups, the trivial and the full subgroup itself and both are normal.  In fact, all subgroups of abelian groups are normal.  

% In general, the cyclic group $C_n$ of order $n$ has exactly one subgroup for each divisor $i$ of $n$.
% \end{example}


% \begin{example}
%   The group $C_2\times C_2$ has has no less than five subgroups: the trivial one, three subgroups that as groups (as opposed as \emph{sub}groups) are equivalent to $C_2$ and the full group $C_4$ itself.
% \end{example}
% \begin{remark}
%   The permutation group $\Sigma_3$ has four nontrivial proper subgroups.  Three conjugate subgroups isomorphic as groups to $C_2$ and one normal one which is as a group is isomorphic to $C_3$.  The component containing the copies of $C_2$ is equivalent to a circle.
% \end{remark}
\sususe{Kernels and cokernels}
\label{subsec:ker}

If $\phi:\Hom^\abstr(\mathcal G,\mathcal G')$ is an abstract group homomorphism, the preimage $\phi^{-1}(e_G)$ is a classically called the kernel of $\phi$ and the cokernel is the quotient set of $\mathcal G'$ by the relation that if $g:\mathcal G$ and $g':\mathcal G'$, then $g'\sim g'\cdot\phi(g)$.  
In our setup with a group homomorphism 
$$f:\Hom(G,G')\defequi(BG\to_*BG'),$$ the kernel and cokernel are just two aspects of the preimage 
$$(Bf)^{-1}(\pt_{G'})\defequi\sum_{z:BG}(\pt_{G'}=Bf(z)):$$
 the cokernel is the set of components and the kernel is a preferred component.  This point of view makes it clear that the kernel is a subgroup whereas there is no particular reason for the cokernel to be more than a ($G'$-) set.
\begin{definition}
  \label{def:cokernel}
  Let $f:\Hom(G,G')\defequi(BG\to_*BG')$  be a homomorphism. %  The preimage $$f^{-1}(\pt_{G'})\defequi\sum_{z:BG}(\pt_{G'}=f(z))$$
% is a groupoid containing important information about $f$.
The \emph{cokernel}\index{cokernel} of $f$ is the $G'$-set
\[
  \coker f:BG'\to\Set,\qquad \coker f(z)\defequi  \Trunc{(Bf)^{-1}(z)}_0.\text{\footnotemark}
\]
\footnotetext{set trunctation}
The associated $\abstr(G')$-set $\coker f(\pt_{G'})$ is also referred to as the cokernel of $f$.  If $f:\Hom(G,G')$ is clear from the context and displays $G$ as a subgroup of $G'$, we often write $G'/G$ for the cokernel of $f$.  

\end{definition}
\begin{definition}
  \label{def:kernel}
Let $f:\Hom(G,G')$  be a homomorphism.
Consider the element 
$$\pt_{\ker f}\defequi(\pt_G,p_f):(Bf)^{-1}(\pt_{G'})$$ (where $p_f:\pt_{G'}=Bf(\pt_G)$ is the part of $f$ claiming it is a pointed map). 
Define the \emph{kernel}\index{kernel}  of $f$ to be the group defined by the pointed component  of $\pt_{\ker f}$ in $(Bf)^{-1}(\pt_{G'})$:
$$\ker f\defequi ((Bf)^{-1}(\pt_{G'})_{(\pt_{\ker f})},\pt_{\ker f}).
$$ 
Written out,
$B\ker f_\div\defequi \sum_{z:BG}\sum_{p:\pt_{G'}=f(z)}\Trunc{\pt_{\ker f}=(z,p)}.$  

The first projection $B\ker f\to_* BG$ displays the kernel $\ker f$ as a subgroup of $G$ (\emph{sub}group since the preimages are equivalent to the sets $\sum_{p:\pt_{G'}=Bf(z)}\Trunc{\pt_{\ker f}=(z,p)}$).  

A subgroup is said to be \emph{normal}\index{normal} if it is the kernel of a surjective homomorphism.\footnote{clarify the relation between the surjective homomorphism and the subgroup}
\end{definition}

\begin{definition}
\label{def:image}
The \emph{image}\index{image} of $f$ is the subgroup of $G'$ given by $B\image f\defequi \sum_{z:BG'}\coker f(z)$ pointed at $\pt_{\image f}\defequi (\pt_{G'},|\pt_G,p_f|)$ together with the first projection $B\image f\to BG'$ (plus the fact that $\coker f(z)$ is a set).\label{def:surjective}

The \emph{induced homomorphism} $\tilde f:\Hom(G,\image f)$ is given by sending $x:BG$ to
$$B\tilde f(x)\defequi (Bf(x),|x,\refl{Bf(x)}|).$$ 

We say that the homomorphism $f$ is \emph{surjective}\index{surjective! group homomorphism} if $(Bf)^{-1}(\pt_{G'})$ is connected.
%, or equivalently if $\image f\to G'$ is an equivalence.
\end{definition}
% \begin{remark}
%   \label{rem:cokerasGset}
%   If $f:\Hom(G,G')$ we notice that the abstract group $\abstr(G')$ acts on $\coker(f)\defequi\Trunc{f^{-1}(\pt_{G'})}_0$, making the cokernel an $\abstr(G')$-set.  If we prefer to talk about a $G'$-set, we consider the cokernel as the set-family $$BG'\to\Set,\qquad z\mapsto   \Trunc{f^{-1}(z)}_0.$$  
% We will see this used most frequently when considerint inclusions of subgroups: if $H$ is a subgroup of $G$, then $G/H$ is a $G$-set.
% \end{remark}
In view of \cref{ex:charsurinj} below, the families  
$$\mathrm{issurj},\mathrm{isinj}:\Hom(G,G')\to\Prop
$$
of propositions that a given homomorphism is surjective or injective have several useful interpretations.
\begin{xca}
  \label{ex:charsurinj}
  Let $f:\Hom(G,G')$ Prove that
  \begin{enumerate}
  \item the following are equivalent
    \begin{enumerate}
    \item $f$ is a surjective homomorphism (\cref{def:surjective}),
    \item the cokernel of $f$ is contractible,
    \item the first projection $B\image f\to BG$ is an equivalence
    \item the induced map of sets 
$f^=:(\pt_G=\pt_G)\to(\pt_{G'}=\pt_{G'})$ is a surjection
    \end{enumerate}
  \item the following are equivalent
    \begin{enumerate}
    \item $f$ is an injective homomorphism (\ie the induced map of sets 
$f^=:(\pt_G=\pt_G)\to(\pt_{G'}\to\pt_{G'})$
is an injection)
\item the kernel of $f$ is trivial
\item $Bf:BG\to BG'$ is a \covering.
\item the induced map $B\tilde f:BG\to B\image f$ is an equivalence.
    \end{enumerate}
  \end{enumerate}
\end{xca}



Note that if $f:\Hom(G,G')$, then the composite of the induced homomorphism $\tilde f:\Hom(G,\image f)$ with the subgroup inclusion (first projection) of $\image f$ in $G'$ is $f$ by definition.  We will refer to this as the \emph{factorization of $f$ through its image}.

\begin{lemma}
  \label{lem:kerandcoker}
  \label{lem:countinggps}
  Let $f:\Hom(G,G')$ be a group homomorphism.  The induced homomorphism $\tilde f:\Hom(G,\image f)$ is a surjective homomorphims and $f$ factors as $\tilde f$ followed by the inclusion of the image of $f$ in $G'$.  The induced map $(B\tilde f)^{-1}(\pt_{\image f})\to (Bf)^{-1}(\pt_{G'})$ induces an equivalence $B\ker\tilde f\simeq B\ker f$.
\end{lemma}
\begin{proof}
Only the last part needs further comment, but follows since since for $x:BG$ the first projection from $\pt_{\image f}=(Bf,|x,\refl{Bfx}|)$ to $\pt_{G'}=f(x)$ is an equivalence (the fibers are true propositions).
  \footnote{\color{blue}  
 Also show counting results for the finite group part somewhere.} 
\end{proof}

Finally, the image factorization would have been useless were it not for the fact that it is unique:
\begin{lemma}
  \label{lem:uniquenessofimagefactorizationforgroups}
  Let $G,H,G'$ be groups, let $h:\Hom(G,H)$ and $j:\Hom(H,G')$ be homomorphisms and let $!:f=j\,h$.  If $h$ is surjective there is a unique homomorphism $t:\Hom(H,\image f)$ so that $\tilde f=t\, h$ and $j$ is $t$ composed with the first projection from $\image f$ to $ G'$.
\end{lemma}
\begin{proof}
  We've used that we're operating with groupoids to simplify the statement, but a similar statement follows generally by essentially the proof below if you keep track of the element in $f=j\,h$.  To simplify we drop the ``$B$''s from the notation, writing ``$f$'' instead of ``$Bf$''.  

That $h$ is a surjective homomorphism amounts to saying that for $y:BH$, then the set truncation $\Trunc{h^{-1}(y)}_0$ of the preimage is contractible, and so the first projection $\mathrm{pr_1}:\sum_{y:BH}\Trunc{h^{-1}(y)}_0\to BH$ is an equivalence.

For $y:BH$, consider the map 
$$T_y:h^{-1}(y)\to f^{-1}(j y),\qquad T_y(x,p)\defequi (x,!_xj(p))$$ where $x:BG$, $p:y=h(x)$ and $!_xj(p):j(y)=f(x)$ is the composite of $j(p):j(y)=j\,h(x)$ and $!:j\,h=f$ (as applied to $x$).  Performing set-truncation on $T_y$ and precomposing with the inverse of the first projection, we get a map
$$t:BH%\sum_{y:BH}\Trunc{h^{-1}(y)}_0
\to\sum_{z:BG'}\Trunc{f^{-1}(z)}_0\oldequiv B\image f,\qquad Bt(y)\defequi(jy,|T_y|(q_y))$$
where $q_y:\Trunc{h^{-1}(y)}_0$ is the second projection of the inverse of the first projection.  The agreement of $t$ with $\tilde f$ and $j$ follows by construction.
\end{proof}

\begin{example}
  An example from linear algebra: let $A$ be any $n\times n$-matrix with nonzero determinant and with integer entries, considered as a homomorphism $A:\Hom(\ZZ^n,\ZZ^n)$.  Then the cokernel of $A$ is a finite set with cardinality the absolute value of the determinant of $A$.  You might want to picture this as a $|\det(A)|$-fold \covering of the $n$-fold torus $(S^1)^{\times n}$ by itself.
\end{example}


\sususe{Subgroups through $G$-sets}


Occasionally it is useful to define ``subgroups'' slightly differently.
As we've defined it a subgroup of a group $G$ of the form $(H,f,!)$ where $H$ is a group (pointed connected groupoid  $BH$), $f:BH\to_* BG$ is a pointed map whose fibers are sets (a pointed \covering).  There is really no need to specify that $H$ is a group: if $F:T\to BG$ is a \covering, then $T$ is automatically a groupoid.  

On the other hand,  the type of \coverings over $BG$ is equivalent to the type of $G$-sets: if $X:BG\to\Set$ is a $G$-set, then the \covering is given by the first projection $\tilde X\to BG$ where $\tilde X\defequi\sum_{y:BG}X(y)$ and the inverse is obtained by considering the fibers of a \covering.  Furthermore, we saw in \cref{lem:conistrans} that $\tilde X$ being connected is equivalent to the condition $\istrans(X)$ of \cref{def:transitiveGset} claiming that the $G$-set $X$ is transitive. 

Hence, the type (set, really) $\typesubgroup_G$ of subgroups of $G$ is equivalent to the type of pointed connected \coverings over $BG$, which again is equivalent to the type $\typesubgroup_G'$ of transitive $G$-sets $X:BG\to\Set$ together with a point in $X(\pt_G)$.  

The family of sets $\typesubgroup_G(y)$ where we let the element $y:BG$ vary is by the same reasoning equivalent to the family $\typesubgroup_G'(y)$ which we for reference spell out in symbols.

\begin{definition}
  Let $G$ be a group and $y:BG$, then the $G$-set of \emph{subgroups' of $G$} is
  $$\typesubgroup_G':BG\to\Set,\qquad\typesubgroup_G'(y)\defequi\sum_{X:BG\to\Set}\sum_{\pt_y:X(y)}\mathrm{isTrans}(X)$$
and the type of \emph{normal subgroups'} is the set of fixed points
$$\typenormal_G'\defequi\prod_{y:BG}\typesubgroup_G'(y).$$
%A \emph{normal subgroup'} of $G$ is an element in $\typenormal_G'$.
\end{definition}
Likewise, in symbols, the above described equivalence between the families $\typesubgroup_G$ and $\typesubgroup_G'$ is provided by the map 
$$E(y):\typesubgroup_G(y)\to\typesubgroup_G'(y),\qquad E(H,F,p_F,!)=(F^{-1}, (\pt_H,p_F),!)
$$
(where $H$ is a group, $F:BH_\div\to BG_\div$ is a map and $p_F:y=F(\pt_H)$ an identity in $BG$; and $F^{-1}:BG\to\Set$ is $G$-set given by the preimages of $F$ and $(\pt_H,p_F):F^{-1}(y)\defequi \sum_{x:BH}y=F(x)$ is the base point).  If $y$ is $\pt_G$ we follow our earlier convention of dropping it from the notation.


Since the families are equivalent we may use $\typesubgroup_G$ or $\typesubgroup_G'$ interchangeably.  
There is, however, a little explanation needed in order to see that the type $\typenormal_G$ of normal subgroups is equivalent to $\typenormal'_G$.
We do this by using the intermediate set of surjections from $G$:
\newcommand{\epi}{\mathrm{epi}}
\begin{definition}
  \label{def:typeepi}
  If $G$ is a group, then the \emph{set of surjections from $G$} is the set
$$\epi_G\defequi\sum_{G':\typegroup}\sum_{f:\Hom(G,G')}\mathrm{issurj}(f).$$
\end{definition}
Note that if $f:\Hom(G,G')$ is a surjective homomorphism and $e:G'=G''$ is an identity of groups, then $(G',f,!)$ and $(G'',f',!)$ are identitified via $e$, where $f':\Hom(G,G'')$ is the homomorphism given by the composite of $f$ and the homomorphism corresponding to $e$.

\begin{definition}
  \label{def:ker2}
  If $f:\Hom(G,G')$ is a homomorphism and $x,y:BG$, set $P^f_y(x)\defequi (f(y)=f(x))$.
  Define $$\ker':\epi_G\to\typenormal_G'$$
  by $\ker'(G',f,!)(y)\defequi(P^f_y,\refl{f(y)},!)$.
\end{definition}

\begin{lemma}
  \label{lem:diagfornormal}
  The diagram
  $$\xymatrix{
  &\typenormal_G\ar[r]^{\subseteq}&\typesubgroup_G\ar[dd]_{\simeq}^{E}\\
  \epi_G\ar[ur]^{\ker}\ar[dr]_{ker'}&&\\
  &\typenormal_G'\ar[r]^{\subseteq}&\typesubgroup_G'}
$$
commutes, where the top composite is the image factorization of the kernel and the bottom inclusion is the inclusion of fixed points.
\end{lemma}
\begin{proof}
  Following $(G',f,!):\epi_G$ around the top to $\typesubgroup_G'$ yields the transitive $G$-set sending $y:BG$ to the set $\pt_{G'}=f(y)$ together with the point $p_f:\pt_{G'}=f(\pt_G)$ while around the bottom we get the transitive $G$-set sending $y:BG$ to the set $f(\pt_G)=f(y)$ together with the point $\refl{f(\pt_G)}:f(\pt_G)=f(\pt_G)$.  Hence, precomposition by $p_f$ gives the identity proving that the diagram commutes. 
\end{proof}
We will prove that both $\ker$ and $\ker'$ in the diagram of \cref{lem:diagfornormal} are equivalences, leading to the desired conclusion that the equivalence $E:\typesubgroup_G\we\typesubgroup_G'$ takes the subset $\typenormal_G$ identically to $\typenormal_G'$.  Actually, by the uniqueness of the image factorization shown in \cref{lem:uniquenessofimagefactorizationforgroups}, it is enough to show that $\ker'$ is an equivalence; we'll spell out the details.

We start with a small, but crucial observation.
\begin{lemma}
  \label{lem:evaliseqwhennormal}
  Let $N:\typenormal'_G$ be a normal subgroup' with $N(y)\oldequiv (X_y,\pt_y,!)$ for $y:BG$.  Then for any $y,z:BG$
  \begin{enumerate}
  \item the evaluation map
$$\mathrm{ev}_{yz}:(X_y=X_z)\to X_z(y),\qquad \mathrm{ev}_{yz}(f)=f_y(\pt_y)$$
is an equivalence and
  \item  the map $X:(y=z)\to(X_y=X_z)$ (given by induction via $X_{\refl y}\defequi\refl{X_y}$) is surjective.
  \end{enumerate}
\end{lemma}
\begin{proof}
To establish the first fact we need to do induction independently on $y:BG$ and $z:BG$ in $X_y(z)$ at the same time as we observe that it suffices (since $BG$ is connected) to show that $\mathrm{ev}_{yy}$ is an equivalence.

% Induction on the index gives rise to the map $X:(y=z)\to(X_y=X_z)$ ($X_{\refl y}\defequi\refl{X_y}$) and t
The composite 
$$\mathrm{ev}_{yy}X:(y=y)\to X_yy$$ is determined by $\mathrm{ev}_{yy}X(\refl y)\oldequiv \pt_y$. 
By transitivity of $X_y$ this composite is surjective, hence $\mathrm{ev}_{yy}$ is surjective too.  

On the other hand, in  \cref{lem:evisinjwhentransitive} we used the transitivity of $X_y$ to deduce that $\mathrm{ev}_{yy}$ was injective.  Consequently $\mathrm{ev}_{yy}$ is an equivalence.  But since $\mathrm{ev}_{yy}$ is an equivalence and $\mathrm{ev}_{yy}X$ is surjective we conclude that $X$ is surjective
\end{proof}
\begin{definition}
\label{def:normalquotient}
  Let $N:\typenormal'_G$ be a normal subgroup' with $N(y)\oldequiv (X_y,\pt_y,!)$ for $y:BG$.  The \emph{quotient group}\index{quotient group} $G/N$ is the group defined as the component of the groupoid of $G$-sets containing and pointed at $X_{\pt_G}$.  

The \emph{quotient homomorphism}\index{quotient homomorphism} is the homomorphism $q_N:\Hom(G,G/N)$  defined by $Bq_N(z)=X_z$ (strictly pointed).  By \cref{lem:evaliseqwhennormal} $q_N$ is surjective and we have defined a map
$$q:\typenormal_G'\to\epi_G,\qquad q(N)=(G/N,q_N,!).$$
\end{definition}

\begin{remark}
It is instructive to see how the quotient homomorphism $Bq_N:BG\to BG/N$ is defined in the torsor interpretation of $BG$.  If $Y\colon BG\to\UU$ is a $G$-type we can define the quotient as
$$
Y/N:BG\to\UU,\qquad Y/N(y)\defequi\sum_{z:BG}Y(z)\times X_z(y).
$$
We note that in the case $\princ G(y)\defequi (\pt_G=y)$ we get
that 
$
\princ G /N(y)\defequi\sum_{z:BG}(\pt_G=z)\times X_z(y)
$
is equivalent to $X_{\pt_G}$.  Consequently, if $Y$ is a $G$-torsor, then $Y/N$ is in the component of $X_{\pt_G}$ and we have
$$-/N:\typetorsor_G\defequi (G\text{-set})_{(\princ G)}\to (G\text{-set})_{(X_{\pt_G})}.
$$ Our quotient homomorphism $q_N:\Hom(G,G/N)$ is the composite of the equivalence $\pathsp{}^G:BG\we\typetorsor_G$ of \cref{lem:BGbytorsor} and the quotient map $-/N$.
\end{remark}
\begin{lemma}
  \label{lem:qeq}
  The map $\ker':\epi_G\to\typenormal_G'$ is an equivalence with inverse $q:\typenormal_G'\to\epi_G$.
\end{lemma}
\begin{proof}
  Assume $N:\typenormal_G'$ with $N(y)\defequi(X_y,\pt_y,!)$ for $y:BG$.  Then $\ker' q(N):BG\to\Set$ takes $y:BG$ to $(\ker' q(N))(y)\oldequiv(Y_y,\refl{X_y},!)$, where $Y_y(z)\defequi (X_y=X_z)$.  Noting that the equivalence $\mathrm{ev}_{yz}:(X_y=X_z)\we X_z(y)$ of \cref{lem:evaliseqwhennormal} has $\mathrm{ev}_{yy}(\refl{X_y})\defequi \pt_y$ we see that univalence gives us the desired identity $\ker' q(N)=N$.\footnote{fix so that it adhers to dogmatic language and naturality in $N$ is clear}

Conversely, consider a surjective homomorphism $f:\Hom(G,G')$.  
For $x:BG$ and $z:BG'$ let $Q^f_z(x)\defequi (z=f(x))$.  
Then the quotient group $G/\ker'(f)$ is the component  of the groupoid of $G$-sets containing and pointed at $Q^f_{f(pt_G)}$ and the quotient homomorphism $q_{\ker' f}:BG\to_* BG/\ker' f$ is given by  $q_{\ker' f}(y)\defequi Q^f_{f(y)}$ (strictly pointed -- \ie by $\refl{Q^f_{f(\pt_G)}}$). 
Observe that by using the identification of the basepoint $Q^f_{f(\pt_G)}$ of $BG/\ker'f$ with $Q^f_{\pt_{G'}}$ given by $p_f:\pt_{G'}=f(\pt_G)$ we have defined a homomorphism $Q^f:\Hom(G',G/\ker'f$) such that 
 $$\xymatrix{&BG\ar[dl]_f\ar[dr]^{q_{\ker'f}}&\\
 BG'\ar[rr]_{Q^f}&&BG/\ker'f
}$$
commutes.
We are done if we can show that $Q^f$ is an equivalence.
The preimage of the base point $Q^f_{f(\pt_G)}$ is
$$\sum_{z:BG'}\prod_{y:BG}(z=f(y))=(f(\pt_G)=f(y))$$ 
which by 
\cref{lem:epifullyfaithful} is equivalent to
$$\sum_{z:BG'}\prod_{v:BG'}(z=v)=(f(\pt_G)=v)$$
which by \cref{lem:pathsptransportiseq} is equivalent to the contractible type $\sum_{z:BG'}z=f(\pt_G)$.
\end{proof}

\begin{corollary}
  \label{cor:normalisnormal}
  The kernel $\ker:\epi_G\to \typenormal_G$ is an equivalence of sets.
\end{corollary}
\begin{proof}
  Since $\ker':\epi_G\to\typenormal_G'$ and $E:\typesubgroup_G\to\typesubgroup_G'$ are equivalences and the diagram in \cref{lem:diagfornormal} commutes, the kernel from $\epi_G$ to $\typesubgroup_G$ is an injection.  Hence, given a normal subgroup, the type of epimorphisms of which it is the kernel is contractible.
\end{proof}

With this much effort in proving that our two perspectives on the concept of normal subgroups are the same, it can be worthwhile to make the composite equivalence
$$\ker\,q:\typenormal_G'\we\typenormal_G$$
explicit.   Let $N:\typenormal'_G$ be a normal subgroup' with $N(y)\oldequiv (X_y,\pt_y,!)$ for $y:BG$ with $X_y:BG\to\Set$, $\pt_y:X_y(y)$ and $!:\mathrm{isTrans}(X_y)$. 
Then 
$$(B\ker q_N)_\div\defequi\sum_{z:BG}(X_z=X_{\pt_G})$$
pointed at $(\pt_G,\refl{X_{\pt_G}})$ and with $i_{\ker f}:B\ker q_N\to_*BG$ given by the first projection.  This can be simplified somewhat:

\begin{definition}
  \label{def:associatednormal}
  Let $N:\typenormal'_G$ be a normal subgroup' with $N(y)\oldequiv (X_y,\pt_y,!)$ for $y:BG$ with $X_y:BG\to\Set$, $\pt_y:X_y(y)$ and $!:\mathrm{isTrans}(X_y)$.  Define a subgroup $(\mathrm{ass}(N),i_N,!)$ of $G$, called the \emph{associated normal subgroup}, as follows:
  \begin{enumerate}
  \item the connected groupoid $B\mathrm{ass}(N)_\div\defequi\sum_{z:BG}X_{\pt_G}(z)$,
  \item together with the point $\pt_N\defequi(\pt_G,\pt_{\pt_G})$,
  \item the first projection $Bi:B\mathrm{ass}(N)\to_*BG$
  \item together with the assertion that the preimages of $Bi$ (which are equivalent to $X_{\pt_G}(z)$ for varying $z:BG$) are sets. 
  \end{enumerate}
\end{definition}


We obviously need to show that the ``normal'' in the name is warranted.
\begin{lemma}
  \label{lem:normalsarekernels}
The map
$$\mathrm{ev}:B\ker q_N\to B\mathrm{ass}(N),\qquad \mathrm{ev}(z,f)\defequi(z,f(\pt_z))$$ is an equivalence and furthermore commutes with the first projections to $BG$.  The pointed map $\mathrm{ev}_*\defequi(\mathrm{ev},\refl{(\pt_G,\pt_{\pt_G})}):B\ker q_N\to_* B\mathrm{ass}(N)$
(well defined since $\mathrm{ev}(\pt_G,\refl{X_{\pt_G}})\defequi (\pt_G,\pt_{\pt_G})$) induces an identification of the subgroups $\ker\,q(N)$ and $\mathrm{ass}(N)$.  

Provided with this information, the associated normal subgroup $\mathrm{ass}(N)$ \emph{is} a normal subgroup and we get a commuting diagram
$$\xymatrix{&\typenormal_G\\
\epi_G\ar[ur]^{\ker}_{\simeq}\ar[dr]^{\ker'}_\simeq&\\
&\,\typenormal_G'.\ar[uu]^{\mathrm{ass}}_\simeq}$$
  
  % The associated normal subgroup of $N:\typenormal_G'$ is a normal subgroup; more precisely $N(\pt_G)$ is the kernel of the quotient homomorphism $q_N:\Hom(G,G/N)$.
  % Let $N:\typenormal'_G$ be a normal subgroup' with $N(y)\defequi (X_y,\pt_y,!)$ for $y:BG$ with $X_y:BG\to\Set$, $\pt_y:X_y(y)$ and $!:\mathrm{isTrans}(X_y)$.  Define a subgroup $(\mathrm{ass}(N),i_N,!)$ of $G$ as follows:
  % \begin{enumerate}
  % \item the connected groupoid $B\mathrm{ass}(N)_\div\defequi\sum_{z:BG}X_{\pt_G}(z)$,
  % \item together with the point $\pt_N\defequi(\pt_G,\pt_{\pt_G})$,
  % \item the first projection $Bi:B\mathrm{ass}(N)\to_*BG$
  % \item together with the assertion that the preimages of $Bi$ (which are equivalent to $X_{\pt_G}(z)$ for varying $z:BG$) are sets. 
  % \end{enumerate}
  % Then $(\mathrm{ass}(N),i_N,!)$ is a normal subgroup of $G$ in the sense that it is the kernel of a homomorphism.
\end{lemma}
\begin{proof}
  % Let $N(y)\oldequiv (X_y,\pt_y,!)$ for $y:BG$.  Let $G/N$ be the group defined as the component of the groupoid of $G$-sets containing and pointed in $X_{\pt_G}$.  Let $f:\Hom(G,G/N)$ be the homomorphism defined by $Bf(z)=X_z$.
 %  Consider the kernel of the quotient homomorphism $q_N:\Hom(G,G/N)$ of \cref{def:normalquotient},
% $$(B\ker q_N)_\div\defequi\sum_{z:BG}(X_z=X_{\pt_G})$$
% pointed in $(\pt_G,\refl{X_{\pt_G}})$ and with $i_{\ker f}:B\ker q_N\to_*BG$ given by the first projection.  Consider t

% We claim that $\mathrm{ev}$ is an equivalence.
Compared with the proof of $\ker'$ being an equivalence (\cref{lem:qeq}) there are no new ingredients.
Since $B\mathrm{ass}(N)$ is connected it is enough to show that the preimage of $\mathrm{ev}^{-1}(\pt_G,\pt_{\pt_G})$ is contractible.  
Since $\mathrm{ev}$ agrees with the projections to $BG$, the preimage is equivalent to $\sum_{f:X_{\pt_G}=X_{\pt_G}}f(\pt_{\pt_G})=\pt_{\pt_G}$.  We recognize this as the preimage $\mathrm{ev}_{{\pt_G}{\pt_G}}^{-1}(\pt_{\pt_G})$
of the evaluation map 
$\mathrm{ev}_{{\pt_G}{\pt_G}}:(X_{\pt_G}=X_{\pt_G})\to X_{\pt_G}(\pt_G)$ which is an equivalence by \cref{lem:evaliseqwhennormal}.  
% the preimage $\mathrm{ev}_{X_{\pt_G}}^{-1}(\pt_{\pt_G})$
% of the evaluation map 
% $\mathrm{ev}_{X_{\pt_G}}:(X_{\pt_G}=X_{\pt_G})\to X_{\pt_G}(\pt_G)$.  
% In \cref{lem:evisinjwhentransitive} %{lem:conistrans} 
% we proved that (since $X_{\pt_G}$ is transitive) $\mathrm{ev}_{X_{\pt_G}}$ is an injection.  Hence the preimage is a proposition, but since it contains $(\refl{X_{\pt_G}},\refl{\pt_{\pt_G}})$ it is contractible. 

Evoking univalence we get an identification of subgroups between the kernel of $f$ and $(\mathrm{ass}(N),i_N,!)$.
\end{proof}


\begin{remark}
  Where did we use that $N$ was a fixed point of the $G$-set $\typesubgroup_G'$?  If $Y:BG\to\Set$ is a transitive $G$-set and $\pt_H:Y(\pt_G)$, then surely we could consider the group $W$ defined as the component of the groupoid of $G$-sets containing and pointed at $Y$.  The first problem is that we wouldn't know how to construct a homomorphism from $G$ to $W$ which we then could consider the kernel of.  The second problem is that we'd be stuck at the very end where we 
used \cref{lem:evaliseqwhennormal} to show that the evaluation map is an equivalencs; if we only had transitivity we could use \cref{lem:evisinjwhentransitive} to pin down injectivity, but surjectivity needed the extra induction freedom. 
\end{remark}

Summing up, using the various interpretations of subgroups, we get the following list of equivalent sets all interpreting what a normal subgroup is.  
%The explicit equivalences are left out of the statements.
\begin{lemma}
  \label{lem:characterizations of normal}
  Let $G$ be a group, then the following sets are equivalent
\begin{enumerate}
\item The set $\epi_G$ of surjective homomorphisms from $G$,
\item the set $\typenormal_G$ of kernels of surjections from $G$,
\item the set $\typenormal_G'$ of fixed points of the $G$-set $\typesubgroup_G'$,
\item the set of fixed points of the $G$-set $\typesubgroup_G$
\item the set of fixed points of the $G$-set of abstract subgroups of $\abstr(G)$ of \cref{lem:conjugationabstractly}.
\end{enumerate}
\end{lemma}


% The associated normal subgroup defines an equivalence from $\typenormal_G'$ to the type $\typenormal_G$ of kernels of surjective homomorphism. To see this we construct an inverse.

% \begin{definition}
%   \label{def:kerneltofixedpoint}
%   Let $f:\Hom(G,G')$ be a surjective homomorphism.  For $y,z:BG$ consider the set $X_y^f(z)\defequi (f(z)=f(y))$ and the element $\pt^f_y\defequi\refl{f(y)}:X_y(y)$.  The $G$-set $X_y:BG\to\Set$ is transitive since $f$ is surjective and so we have a map 
% $$\mathrm{ssa}:\typenormal_G\to\typenormal_G',\qquad \mathrm{ssa}(f)(y)\defequi(X_y^f,\pt_y^f,!).$$
% \end{definition}

% \begin{lemma}
%   \label{lem:characterizations of normal}
%   Let $G$ be a group, then the associated normal subgroup is an equivalence
%   $$\mathrm{ass}:\typenormal_G'\to\typenormal_G$$
% with inverse $\mathrm{ssa}$.  Summing up the following sets are equivalent
% \begin{enumerate}
% \item The set $\typenormal_G$ of kernels of surjections from $G$,
% \item the set $\typenormal_G'$ of fixed points of the $G$-set $\typesubgroup_G'$,
% \item the set of fixed points of the $G$-set $\typesubgroup_G$
% \item the set of fixed points of the $G$-set of abstract subgroups of $\abstr(G)$.
% \end{enumerate}
% \end{lemma}
% \begin{proof}
%   The last three entries are equivalent since they are the fixed points of equivalent $G$-sets, so we only need to comment on the first assertion.

% Let $f:\Hom(G,G')$ be a surjective homomorphism.  
% The kernel $N\oldequiv \ker f$ is then given by the first projection 
% $$\text{pr}:\sum_{z:BG}\pt_{G'}=Bf(z)\to_*BG.$$
% Then $\mathrm{ass\,ssa}(\ker f)$ defined to be
% $$
% (\sum_{z:BG}\prod_{y:BG}
% (\pathsp{f(\pt_G)}^{G'}{f(y)}=\pathsp{f(z)}^{G'}{f(y)},
% \text{pr}, (\pt_G,\refl{\pathsp{f(\pt_G)}^{G'}{f(\pt_G)}},!),$$
% where $\pathsp{a}^{G'}{b}\defequi (a=b)$ for $a,b:BG'$.
% The desired identification between $\ker f$ and $\mathrm{ass\,ssa}(\ker f)$ is then given by composing the identifications
% $\preinv(p_f):(\pt_{G'}=f(z))=(f(\pt_G)=f(z))$ and 
% $$\preinv:(f(\pt_G)=f(z))=
% \prod_{y:BG}(\pathsp{f(\pt_G)}^{G'}{f(y)}=\pathsp{f(z)}^{G'}{f(y)})$$
% \footnote{((find ref where this was demonstrated: slight modification since we only claim naturality in $G$)).}
% \end{proof}



% There are many valuable constructions to be extracted from the proof of \cref{lem:normalsarekernels}.
% \begin{definition}
%   \label{def:associatedquotient}
% \end{definition}
% \footnote{COMEBACK 190509 Do the converse and elevate constructions to definitions}



\sususe{The pullback}
\label{sec:pullback}

\begin{definition}
  \label{def:pullback}
  Let $B, C, D$ be types and let $f:B\to D$ and $g:C\to D$ be two maps.  
The \emph{pullback}\index{pullback} of $f$ and $g$ is the type 
$$\prod(f,g)\defequi\sum_{(b,c):B\times C}(f(b)=_Dg(c))$$
together with the two projections $\prod(f,g)\to B$ and $\prod(f,g)\to C$ sending $(b,c,p):\prod(f,g)$ to $b:B$ or $c:C$.  If $f$ and $g$ are clear from the context, we may write $B\times_DC$ instead of $\prod(f,g)$ and summarize the situation by the diagram
$$\xymatrix{B\times_DC\ar[r]\ar[d]&C\ar[d]^g\\B\ar[r]^f&\,D.}$$
\end{definition}
\begin{xca}
  \label{xca:univpropofpullback}
  Let $f:B\to D$ and $g:C\to D$ be two maps with common target.  If $A$ is a type show that 
  \begin{align*}
    (A\to B)\times_{(A\to D)}(A\to C)\to &(A\to B\times_DC)\\ 
(\beta,\gamma,p:f\beta=g\gamma)\,\mapsto\,&(a\mapsto (f(a),g(a),p(a):f\beta(a)=g\gamma(a)))
  \end{align*}
 is an equivalence.
\end{xca}

\begin{example}
  If $g:\bn 1\to D$ has value $d:D$ and $f:B\to D$ is any map, then $\prod(f,g)\oldequiv B\times_D\bn 1$ is equivalent to the preimage $f^{-1}(d)\defequi\sum_{b:B}d=f(b)$.
\end{example}
\begin{example}
  \label{ex:pullbackandgcd}
  Much group theory is hidden in the pullback.  For instance, the greatest common divisor $\gcd(a,b)$ of $a,b:\NN$ is another name for the number of components you get if you pull back the $a$-fold and the $b$-fold cover of the circle: as we will see in \cref{lem:iso2} we have a pullback
$$\xymatrix{S^1\times C_{\gcd(a,b)}\ar[d]\ar[r]& S^1\ar[d]^{(-)^b}\\
S^1\ar[r]^{(-)^a}&\,S^1}
$$ 
(where $C_n$ was the cyclic group of order $n$).
To get a geometric idea, think of the circle as the unit circle in the complex numbers so that the $a$-fold cover is simply taking the $a$-fold power.  With this setup, the pullback should consist of pairs $(z_1,z_2)$ of unit length complex numbers with the property that $z_1^a=z_2^b$.  Let $a=a'G$ and $b=b'G$ where $G=\gcd(a,b)$. Taking an arbitrary unit length complex number $z$, then the pair $(z^{b'},z^{a'})$ is in the pull back (since $a'b=ab'$).  But so is $(\zeta z^{b'},z^{a'})$, where $\zeta$ is any $G$-th root of unity.  Each of the $G$-choices of $\zeta$ contributes in this way to a component of the pullback.  In more detail: identifying the cyclic group $C_G$ of order $G$ with the group of $g$-th roots of unity, the top horizontal map $S^1\times C_G\to S^1$ sends $(z,\zeta)$ to $z^{a'}$ and the left vertical map sends $(z,\zeta)$ to the product $\zeta z^{b'}$.  

Also the least common multiple is hidden in the pullback; in the present example it is demonstrated that the map(s) accross the diagram makes each component of the pullback a copy of the subgroup $a'b\ZZ$ of $\ZZ$.
\end{example}


\begin{definition}
  \label{def:intersectionand unionofsets}
  Let $S$ be a set and consider two subsets $A$ and $B$ of $S$ given by two families of propositions (for $s:S$) $P(s)$ and $Q(s)$.  The \emph{intersection}\index{intersection! of sets} $A\cap B$ of the two subsets is given by the family of propositions $P(s)\times Q(s)$.  The \emph{union}\index{union of sets} $A\cup B$ is given by the set family of propositions $A(s)+B(s)$.  
\end{definition}
\begin{xca}
  \label{xca:intersectionpullbackofsets}
  Given two subsets $A$, $B$ of a set $S$, prove that
  \begin{enumerate}
  \item The pullback $A\times_SB$ maps by an equivalence to the intersection $A\cap B$,
  \item\label{xca:cardinalityintersectionunion} 
    If $S$ is finite, then the sum of the cardinalities of $A$ and $B$ is equal to the sum of the cardinalities of $A\cup B$ and $A\cap B$.
  \end{enumerate}
\end{xca}

\begin{definition}
  \label{def:intersectionofgroups}
  Let $f:\Hom(H,G)$ and $f':\Hom(H',G)$ be two homomorphisms with common target.  The \emph{pullback}\index{pullback!of groups} $H\times_GH'$ is the group obtained as the (pointed) component of 
$$\pt_{H\times_GH'}\defequi(\pt_H,\pt_{H'},p_{f'}p_f^{-1})$$ of the pullback $BH\times_{BG}BH'$ (where $p_f:\pt_G=f(\pt_H)$ is the name we chose for the data displaying $f$ as a pointed map, so that $p_{f'}p_f^{-1}:f(\pt_H)=f'(\pt_{H'})$).

If $(H,f,!)$ and $(H',f',!)$ are subgroups of $G$, then the pullback is called the \emph{intersection}\index{intersection! of subgroups} and if the context is clear denoted simply $H\cap H'$.
\end{definition}
\begin{example}
  If $a,b:\NN$ are natural number with least common multiple $L$, then $L\ZZ$ is the intesection $a\ZZ\cap b\ZZ$ of the subgroups $a\ZZ$ and $b\ZZ$ of $\ZZ$. 
\end{example}

\begin{xca}
  Prove that if $f:\Hom(H,G)$ and $f':\Hom(H',G)$ are homomorphisms, then the pointed version of \cref{xca:univpropofpullback} induces an equivalence
$$(\pt_{H}=\pt_{H})\times_{(\pt_{G}=\pt_{G})}(\pt_{H'}=\pt_{H'})
\simeq (\pt_{H\times_GH'}=\pt_{H\times_GH'})
$$
(hint: set $A\defequi S^1$, $B\defequi BH$, $C\defequi BH'$ and $D\defequi BG$).  Elevate this equivalence to a statement about abstract groups.
\end{xca}

\begin{xca}
  If $\mathcal G$ is an abstract group and $\mathcal H$ and $\mathcal K$ are abstract subgroups.  Give a definition of the intersection $\mathcal H\cap\mathcal K$ is the abstract subgroup of $\mathcal G$ agreeing with our definition for groups.
\end{xca}
\begin{lemma}
  \label{lem:whatSylow2needs}
  Let $f:\Hom(G,G')$ be a surjective homomorphism with kernel $N$ and let $H$ be a subgroup of $G$.  Then
  %\begin{enumerate}
  %\item 
$N\cap H$ is a normal subgroup of $H$
%  \item The 
and the induced homomorphism $H/N\cap H\to G'$ is injective.
  % \item If $H$ and $G'$ are finite with coprime cardinalities, then $H$ is a subgroup of $N$.
%  \end{enumerate}
  \begin{proof}
Let $i:\Hom(H,G)$ be the inclusion.  We will show that $N\cap H$ is the kernel of the composite $fi:\Hom(H,G')$.  

Now, $N$ is the kernel of the surjective homomorphism $f$, giving an equivalence between $BN_\div$ and the preimage 
$$(Bf)^{-1}(\pt_{G'})\defequi\sum_{y:BG}\pt_{G'}=Bfy.$$  
Writing out the definition of the pullback (and using that for each $x:BH$ the type $\sum_{y:BG}y=Bix$ is contractible), we get an equivalence between $BN\times_{BG}BH$ and 
$$B(fi)^{-1}(\pt_{G'})\defequi\sum_{x:BH}\pt_{G'}=B(fi)x,$$  
the preimage of $\pt_{G'}$ of the composite $B(fi):BH\to BG'$.
 By definition, the intersection $B(N\cap H)$ is a the pointed component of the pullback containing $(\pt_N,\pt_H)$.  Under the equivalence with $B(fi)^{-1}(\pt_{G'})$ the intersection corresponds to the component of $(\pt_H,Bf(p_i)\,p_f)% :\sum_{x:BH}\pt_{G'}=B(fi)x
 $.  
Since (by definition of the composite of pointed maps) $p_{fi}\defequi Bf(p_i)\,p_f$ we get that the intersection $N\cap H$ is identified with the kernel of the composite $fi:\Hom(H,G')$.
%    \item 

Finally, since $N\cap H$ is the kernel of the composite $fi:\Hom(H,G')$, under the equivalence of \cref{lem:countinggps}, $N\cap H$ is equivalent to the kernel of the induced surjective homomorphism $\widetilde {fi}:\Hom(H,\image (fi))$.  Otherwise said, the quotient group $H/(N\cap H)$ is another name for $\image (fi)$ which indeed injects into $G'$.
%    \end{enumerate}
  \end{proof}
\end{lemma}


Recall that if $X:BG\to\Set$ is a $G$-set, then the set of fixed points is the set $\prod_{v:BG}X(v)$, which is a subset of $X(\pt_G)$ via the evaluation map.  If a homomorphism from a group $H$ to $G$ is given by $F:BH_\div\to BG_\div$ and $p_F:\pt_G=F(\pt_H)$, then precomposition (``restriction of scalars'') by $F$ gives an $H$-set 
$$F^*X\defequi X\,F:BH\to\Set.$$  
In the case of inclusions of subgroups (or other situations where the homomorphism is clear from the context) it is not uncommon to talk about ``the $H$-set $X$'' rather than ``$F^*X$''.  
This can be somewhat confusing when it comes to fixed points: the fixed points of $F^*X$ are given by $\prod_{v:BH}XF(v)$ which evaluates nicely to $XF(\pt_H)$, but in order to considered  these as elements in $X(\pt_G)$ we need to apply $X(p_F^{-1}):X(F(\pt_H))=X(\pt_G)$.  

Consequently, we'll say that $x:X(\pt_G)$ is an \emph{$H$-fixed point} if there is an $f:\prod_{v:BH}XF(v)$ such that $x=X(p_F^{-1})f(\pt_H)$.



\begin{lemma}
  \label{lem:thereisaconjugate}
  Let $G$ be a group, $X:BG\to Set$ a $G$-set, $x:X(\pt_G)$, $g:\pt_G=\pt_G$ and $H=(H,F,p,!):\typesubgroup_G$ a subgroup of $G$ ($F:BH_\div\to BG_\div$ and $p:\pt_G=F(\pt_H)$).  

Then $g\,x$ is a fixed point for the $H$-action on $X$ if and only if $x$ is a fixed point for the action  of the conjugate subgroup $g\,H\defequi(H,F,g^{-1}p_F,!)$ on $X$.
\end{lemma}
\begin{proof}
  Consider an $f:\prod_{v:BH}XF(v)$.  Then $g\cdot x=X(p_F^{-1})(f(\pt_H))$ if and only if $x=g^{-1}\cdot X(p_F^{-1})(f(\pt_H))\oldequiv X((g^{-1}p_F)^{-1}(f(\pt_H))$.
\end{proof}



% {\color{blue}Remove when lemma above gets stable \begin{lemma}
%   \label{lem:thereisaconjugate}
%   Let $G$ be a group, $X$ a $G$-set, $x:X$ and $H=(H,i,!)$ a subgroup of $G$.  If $y$ is an element in the orbit of $x$ s.t. $H\subseteq Stab_y$  (\ie $y$ is an $H$-fixed point), then there is a conjugate $H'=(H',i',!)$ of $H$ with $H'\subseteq Stab_x$.
% \end{lemma}
% \begin{proof}
%   CLASSICAL: There is a $g:G$ s.t. $y=g\cdot x$ and for all $h:H$ we have $h\cdot y=y$.  Define $H'=g^{-1}Hg$.  If $h':H'$, then $h'=g^{-1}hg$ for a unique $h:H$ and
% $$h'\cdot x=(g^{-1}hg)\cdot x = g^{-1}\cdot(h\cdot (g\cdot x))=g^{-1}\cdot(h\cdot y)=g^{-1}\cdot y = x.$$
% \end{proof}
% }

\sususe{The Weyl group}
\label{sec:Weyl}

In \cref{def:normalquotient} defined the quotient group of a normal subgroup.  The definition itself never used that the subgroup was normal (but the quotient homomorphism did) and is important in this more general context.

Recall the equivalence between the set $\typesubgroup_G$ of subgroups and the set $\typesubgroup_G'$ of pointed transitive $G$-sets: The pair $(X,\pt_X)$ where $X:BG\to\Set$ is a transitive $G$-set and $\pt_X:X(\pt_G)$ corresponds to the subgroup $(H,i_H,!)$ defined by  $BH_\div\defequi\sum_{y:BG}X(y)$ pointed at $\pt_H\defequi (\pt_G,\pt_X)$ together with the first projection $Bi_H:BH\to_*BG$.  Conversely, if $(H,i_H,!):\typesubgroup_G$, then the corresponding transitive $G$-set is $G/H\defequi\coker i_H$ pointed at $|\pt_H,p_{i_H}|:\coker i_H(\pt_G)\defequi\Trunc{\sum_{x:BH}\pt_G=BiH(x)}_0$.  

For the remainder of the section we'll consider a fixed group $G$ with subgroup given by $i_H:\Hom(H,G)$ and $(X,\pt_X,!)$ will be the associated pointed transitive $G$-set.

\begin{definition}
  % Let $G$ be a group and consider the subgroup represented by the transitive $G$-set $X:BG\to\Set$ together with the point $\pt_X:X(\pt_G)$ % (so that $BH_\div\defequi\sum_{y:BG}X(y)$ pointed at $\pt_H\defequi (\pt_G,\pt_X)$ together with the first projection $Bi_H:BH\to_*BG$ defines an element in $(H,i_H,!):\typesubgroup_G$)
  % .
  
The \emph{Weyl group} \label{def:Weyl}\index{Weyl group}
$$W_GH\defequi\Aut_{G\text{-set}}(X)$$ is defined by the component $BW_GH$ of the groupoid of $G$-sets pointed at $X$.

The \emph{normalizer subgroup} \label{def:normalizer}\index{normalizer}
$$N_GH\defequi\Aut_{\sum_{y:BG}\typesubgroup_G'(y)}(\pt_G,X,\pt_X)$$ is defined by the component $BN_GH$ of the groupoid $\sum_{y:BG}\typesubgroup_G'(y)$ pointed at $(\pt_G,X,\pt_X)$.
\end{definition}

Unpacking, we find that
$$BN_GH_\div\oldequiv \sum_{y:BG}\sum_{Y:BG\to\Set}\sum_{\pt^y_Y:Y(y)} \Trunc{(\pt_G,X,\pt_X)=(y,Y,\pt^y_Y)}.$$
While the projection $((\pt_G,X,\pt_X)=(y,Y,\pt^y_Y))\to (X=Y)$ may not be an equivalence, the transitivity of $X$ tells us that for any $\beta:X=Y$ there is a $g:\pt_G=y$ such that $X(g)\,p^y_Y=\beta^{-1}_y\pt_X$, and so the propositional truncation $\Trunc{(\pt_G,X,\pt_X)=(y,Y,\pt^y_Y)} \to \Trunc{X=Y}$ is an equivalence.
Consequently, the projection
$$BN_GH_\div\to \sum_{y:BG}\sum_{Y:BG\to\Set}Y(y)\times\Trunc{X=Y}$$
is an equivalence.  With an innocent rewriting, we see that we have provided an equivalence 
$$e:BN_GH_\div\we\sum_{(y\times Y):BG\times BW_GH}Y(y)\qquad e(y,Y,\pt^y_Y,!)\defequi (y,Y,\pt^y_Y,!).$$
This formulation has the benefit of simplifying the analysis of the ``inclusion'' 
$$i_{N_GH}:\Hom(N_GH,G)$$
given by $Bi_{N_GH}(y,Y,\pt^y_Y,!)\defequi y$, the ``projection''
 $$p_G^H:\Hom(N_GH,W_GH)$$
$Bp_G^H(y,Y,\pt^y_Y,!)\defequi (Y,!)$ and the ``inclusion''
$$j_H:\Hom(H,N_GH)$$
given by $Bj_H(y,v)\defequi(y,X,v,!))$.


% \begin{definition}
% The projections from $N_GH$ to $BG$ and $BW_GH$ are referred to as the inclusion $i_G^H:\Hom(N_GH,G)$ and the projection $p_G^H:\Hom(N_GH,W_GH)$.
% Define $j_H:\Hom(H,N_GH)$ by the pointed map 
% $$Bj_H:\sum_{y:BG}X(y)\to_*\sum_{(y,Y):BG\times BW_GH}Y(y),\qquad Bi_H(y,v)\defequi ((y,X),v).$$
% \end{definition}

% The \emph{normalizer subgroup} $N_GH$ is alternatively defined as
% $$N_GH\defequi(\sum_{(y,Y):BG\times BW_GH}Y(y),((\pt_G,X),\pt_X)).$$

\begin{lemma}
  The inclusion $i_G^H:\Hom(N_GH,G)$ displays the normalizer as a subgroup of $G$ and the projection $p_G^H:\Hom(N_GH,W_GH)$ is a surjective group homomorphism.  

The homomorphism $j_H:\Hom(H,N_GH)$ defines $H$ as a normal subgroup of the normalizer,
$$\ker p_G^H=_{\typesubgroup_{N_GH}for}(H,i_H,!)$$
and $i_H=_{\Hom(H,G)}i_G^H\,j_H$.
\end{lemma}
\begin{proof}
  Immediate from (our rewriting of) the definitions.
\end{proof}

The Weyl group $W_GH$ has an important interpretation.  It is defined as symmetries of the transitive $G$-set $X$, and so $\pt_{W_GH}=\pt_{W_GH}$ is nothing but $(X=_{G\text{-set}}X)=\prod_{y:BG}(X(y)=X(y))$.  On the other hand, $BH_\div$ is equivalent to $\sum_{y:BG}X(y)$ and 
$$\prod_{y:BG}(X(y)=X(y))\simeq \prod_{\sum_{y:BG}X(y)}X(y),$$ so $\pt_{W_GH}=\pt_{W_GH}$ is equivalent to the set $% (i_H^*X)^H\defequi
\prod_{x:BH}X\, Bi_Hx$ of fixed points of $X=G/H$ (regarded as an $H$-set through $i_H$).

Summing up
\begin{lemma}
  \label{lem:WGHisHfixofG/H}
  The map  $e:(X=X)\to \prod_{x:BH}X\, Bi_Hx$ with $e(f)(y,v)=f(y)$ defines an equivalence
$$e:(\pt_{W_GH}=\pt_{W_GH})\we (G/H)^H.$$ 
\end{lemma}

{\color{blue}THE REST OF THE CHAPTER CONTAINS KNOWN NONSENSE \tiny Don't actually seem to need at present; hence put on hold
\begin{lemma}
  \label{lem:iso2}
  Let $G$ be a group with subgroups $(H,i_H,!)$ and $(N,i_N,!)$ where $N$ is normal. Let $i_{HN}:Hom(H \vee N,G)$ be the homomorphism from the sum $H\vee N$ of \cref{def:sumofgroup} to $G$ induced by $i_H$ and $i_N$.  Then 
the pullback $BN\times_{BG}BH$
is equivalent to $G/{HN}\times B(H\cap N)$.\footnote{display the equivalence}
\end{lemma}
\begin{proof}
  ((WRITE)) Can alternatively be phrased as the fiber of $B(H\ltimes N)\to BG$ once semi-direct product has been discussed.
\end{proof}

The below should be deleted


Recall that we defined a normal subgroup as a kernel of a homomorphism (which we may assume is surjective by replacing the target with the image without changing the kernel); we can now give a second characterization:
\begin{lemma}
  \label{lem:normalisfixed}
  Let $G$ be a group.  A subgroup of $G$ is normal if and only if it is a fixed points under the conjugation action.
\end{lemma}
\begin{proof}
  Consider a surjective homomorphism $f:\Hom(G,G')$ and let $BN\defequi\sum_{z:BG}(\pt_{G'}=Bf(z))$ (pointed at $(\pt_G,p_f)$) represent its kernel, with the first projection to $BG$ representing the injection $i_N:\Hom(N,G)$ (with $\refl{\pt_G}$ the witness that $\pt_G$ is identical to the first projection of $(\pt_G,p_f)$).   Now, by the very representation of $N$, for every $g:\pt_G=\pt_G$ we get an equivalence $C^g:BN\we BN$ by setting $C^g(z,p)\defequi(z,p\,f(g)^{-1})$ with basepoint identity (from $\pt_N\defequi(\pt_G,p_f)$ to $C^g\pt_G\defequi (\pt_G,p_ff(g)^{-1})$) given by $g^{-1}:\pt_G=\pt_G$ and the fact 
$$\xymatrix{\pt_Q\ar@{=}[rr]^{p_f}_\to\ar@{=}[d]_{\refl{\pt_Q}}&&f(\pt_G)\\
\pt_Q\ar@{=}[r]^-{p_f}_-\to&f(\pt_G)&\,f(\pt_G).\ar@{=}[l]^\gets_{f(g)}\ar@{=}[u]^\uparrow_{f(g)}}
$$
Since $C^g$ followed by the first projection is exactly the first projection and also the base points match up (\ie $\refl{pt_G}\circ\mathrm{pr}_1(g^{-1},!)=_{\pt_G=\mathrm{pr}_1(\pt,p_f)}g^{-1}$) we get an identity $(N,Bi_N,\refl{\pt_G},!)=_{\typesubgroup_G}(N,Bi_N,g^{-1},!)$, showing that the normal subgroup is a fixed point. 

Conversely, let $(H,i,!)$ be any subgroup of $G$ and consider the pointed component $BW$ of the type of $G$-sets containing the cokernel $G/H$.  If $X$ is a $G$-torsor, then the orbit $X/H$ is a $G$-set in $BW$, \footnote{((explain how you transport the $G\times G$-action from $G$ or deloop))}
providing us with a pointed map $f:BG\to BW$.
By \cref{lem:aut-orbit} \footnote{((which has yet to be provided with a proof))} the identity type $G/H=G/H$ is 


% Let $(H,F,p,!):\typesubgroup_G$ be a fixed point, \ie for all $g:\pt_G=\pt_G$ there is an identity $C^g:H=H$ so that 
% $$\xymatrix{}
% $$
\end{proof}}


% \begin{definition}
%   \label{def:normalizer}
% \footnote{TO BE MOVED TO or AFTER the chapter on symmetry (need Burnside -  a $G$-set splits into orbits - etc) has been covered.}
% An element of the $G$-orbit of a subgroup $(H,i_H,!)$ are called a \emph{conjugate} of $(H,i_H,!)$.   The stabilizer group of a subgroup $(H,i_H,!)$ is called the \emph{normalizer $N_G(H)$ of $H$ in $G$}.\index{normalizer}

% If $(K,i_K,!)$ is another subgroup containing a conjugate of $(H,i_H,!)$, we say that $(H,i_H,!)$ is \emph{subconjugate} to $(K,i_K,!)$.
% \end{definition}

% \begin{lemma}
%   Let $(H,i_H,!):\typesubgroup_G$ and let $N_G(H)$ be the normalizer subgroup of $H$ of \cref{ex:abstrandconj} (considered as a subgroup $(N_G(H),i_{N_G(H)},!)$ of $G$).  Then $H$ is a normal subgroup of $N_G(H)$.  ((come back and prove normal))
% \end{lemma}
% \begin{proof}
%   Remember that $N_G(H)$ is the stabilizer subgroup of $(H,i_H,!)$ under the conjugation action, so to prove that $H$ is a subgroup of $N_GH$ we need to show that if $h:\pt_H=\pt_H$, then there is an identity between $(H,i_H,!)$ and $c^{i_H(h)}(H,i_H,!)$.   
% Let $g\defequi i_H(h)$.  If $s:\pt_H=\pt_H$, then $c^gi_H(s)=g\,i_H(s)\,g^{-1}=i_H(h)\,i_H(s)\,i_H(h)^{-1}=i_H(h\,s\,h^{-1})=i_H(c^hs)$ (since $i_H$ is a homomorphism).  
% Using the identity $c^h:H=H$ we have obtained an identity $(H,i_H,!)=(H,c^{i_H(h)}i_H,!)$.
% \end{proof}

\section{Historical remarks}
\label{sec:grouphistory}

% Move in place

% \begin{remark}
%   Notice that the last statement  (``More precisely\dots'')  not only asserts that there \emph{exist} inverses, but that there actually is a (preferred and consistent) way to produce them.

% Classically this was in many instances unnecessay to say because there was a unique inverse, and the distinction is not mentioned in introductory texts.  However, then this very point had to be revisited later on.  In our proof relevant setting it is obvious that the ultimate statement will have to go beyond an assertion that inverses exist.
% \end{remark}

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


%the below is the illustration used for the n-fold \covering in the deck trafo section.
% Move in place
% \begin{figure}
%   \centering
%   \begin{tikzpicture}
%     \node (A) at (2,2) {$\sqrt[n]X$};
%     \node (B) at (2,-2) {$\bn{n}$};
%     \draw[->] (A) -- node[auto] {$p$} (B);
%     \foreach \y in {-2,0,1,2}
%     { \begin{scope}[shift={(0,\y)}]
%         \foreach \x in {0,...,4}
%         { \node[fill,circle,inner sep=1pt] at (180+72*\x:1 and .3) {}; }
%         \foreach \x in {0,...,3}
%         { \draw[-stealth] (180+72*\x:1 and .3) arc(180+72*\x:252+72*\x:1 and .3); }
%       \end{scope} }
%     \begin{scope}[shift={(0,-2)}]
%       \draw[-stealth] (108:1 and .3) arc(108:180:1 and .3);
%     \end{scope}
%     \foreach \y in {1,2}
%     { \begin{scope}[shift={(0,\y)}]
%         \draw[-stealth] (108:1 and .3)
%         .. controls ++( 5:-.3) and ++(80:.2) .. (-.7,-.4)
%         .. controls ++(80:-.2) and ++(90:.2) .. (-1,-1);
%       \end{scope} }
%     \draw[-stealth] (108:1 and .3)
%     .. controls ++( 5:-.3) and ++(80:.2) .. (-.7,-.4);
%     \node (dz) at (-.7,-.7) {\footnotesize $\vdots$};
%     \begin{scope}[shift={(0,3)}]
%       \draw[-stealth] (-.7,-.4)
%       .. controls ++(80:-.2) and ++(90:.2) .. (-1,-1);
%     \node (da) at (-.7,0) {\footnotesize $\vdots$};
%     \end{scope}
%   \end{tikzpicture}
%   \caption{The $n$'th root of an endomorphism, with projection}
%   \label{fig:rootproj}
% \end{figure}