From 1c1727299e6597866228eaf13f5e6413c28297b0 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Fri, 30 Aug 2024 08:41:32 +0100 Subject: [PATCH] BIG REFACTORING: ONLY THE MOVES, NO EDITS --- book.tex | 6 +- group.tex | 2699 ------------------------------------------------- subgroups.tex | 197 ++++ symmetry.tex | 146 --- 4 files changed, 202 insertions(+), 2846 deletions(-) diff --git a/book.tex b/book.tex index b0fb50b..96c502c 100644 --- a/book.tex +++ b/book.tex @@ -46,9 +46,13 @@ \include{intro-uf} \include{circle} \include{group} +\include{actions} +\include{absgroup} +\include{congp} \include{subgroups} -\include{fggroups} \include{fingp} +\include{fggroups} +\include{abelian} \include{fields} \include{geometry} \include{galois} diff --git a/group.tex b/group.tex index 62c55e1..e55b139 100644 --- a/group.tex +++ b/group.tex @@ -2071,2705 +2071,6 @@ \section{Infinity groups (\texorpdfstring{\inftygps}{∞-groups})} $\Bf : \BG\ptdto\BH$ the \emph{classifying map} of $f$. \end{definition} -\section{Group actions ($G$-sets)} -\label{sec:gsets} - -One of the goals of \cref{sec:Gsetforabstract} below -is to prove that the types of groups and abstract groups are equivalent. -In doing that, we are invited to explore how abstract groups should be thought of as symmetries and introduce the notion of a $G$-set. -However, this takes a pleasant detour where we have to explore the most important feature of groups: they \emph{act} on things (giving rise to manifestations of symmetries)! - -Before we handle the more complex case of abstract groups, -let us see what this looks like for groups. - -\begin{definition} - For $G$ a group, a \emph{$G$-set} is a function - \[ - X : \BG\to\Set, - \] - and $X(\shape_G)$ is referred to as the \emph{underlying set}. - If $p:x\eqto y$ in $\BG$, - then the transport function $X(x)\to X(y)$ induced - by $X(p)\defeq\trp{X}(p) : X(x)\eqto X(y)$ is also denoted by $X(p)$. - We denote $X(p)(a)$ by $p\cdot_X a$. - The operation $\cdot_X$ is called the \emph{group action} of $X$. - When $X$ is clear from the context we may leave out the - subscript $X$.\footnote{% - Note that in this case $\cdot: (x\eqto y) \to X(x) \to X(y)$. - See \cref{def:principaltorsor} for a special case - where $\cdot_X$ is indeed path composition.} - In particular, if $g:\USymG$, - then $X(g)$ is a permutation of the underlying set of $X$. - - The type of $G$-sets is - \[ - \GSet\defequi(\BG\to\Set).\qedhere - \] -\end{definition} -\marginnote{ - Much of what follows will work equally well for $\infty$-groups; - if $G$ is (a group or) an infinity group, - a \emph{$G$-type} is a function $X : \BG\to\UU.$ - More generally, an action of $G$ on en element of type $A$ - is a function $X : \BG\to A$, see~\cref{sec:actions} below.} -If $x:\BG$, then $X(x)$ is a ``twisted'' version of the underlying set. -\begin{remark} - The reader will notice that the type of $G$-sets is equivalent to the -type of \coverings over $\BG$. -The reason we have allowed ourselves two names is that our focus is different: for a $G$-set $X:\BG\to\Set$ we focus on the sets $X(z)$, whereas when talking about \coverings the first projection $\sum_{z:\BG}X(z)\to \BG$ takes center stage. Each focus has its advantages. -\end{remark} - -\begin{example}\label{def:principaltorsor} - If $G$ is a group, then - \[ - \princ G:\BG\to\Set, - \qquad\princ G(z)\defequi\pathsp{\shape_G}(z)\defequi(\shape_G \eqto z) - \] - is a $G$-set called the \emph{principal $G$-torsor}.\footnote{% - The term ``$G$-torsor'' will reappear several times and will mean nothing but a $G$-set in the component of $\princ G$ -- a ``twisted'' version of $\princ G$.} - We've seen this family before in the guise of the (preimages of the) ``universal \covering'' of \cref{def:universalcover}! - - There is nothing sacred about starting the identification - $\shape_G \eqto z$ at $\shape_G$. - Define more generally - \begin{equation}\label{eq:pathsp} - \pathsp{\blank}:\BG\to\GSet, - \qquad - \pathsp{y} \defeq(y\eqto\blank), - \end{equation} - Applying $\pathsp{\blank}$ to a path $q:y\eqto y'$ - induces an equivalence from $\pathsp y$ to $\pathsp {y'}$ that sends $p:y \eqto z$ - to $pq^{-1}:y'\eqto z$. - As a matter of fact, \cref{lem:BGbytorsor} will identify $\BG$ with the type of - $G$-torsors via the map $\pathsp{\blank}$, simply denoted as $\pathsp{}$, - using the full transport structure of the identity type $\pathsp y(z)\jdeq(y \eqto z)$. -\end{example} - -Note that the underlying set of $\princ G$ is -\[ - \princ G(\shape_G) \jdeq - \pathsp{\shape_G}(\shape_G) \jdeq - (\shape_G \eqto \shape_G) \jdeq \USymG, -\] -the underlying symmetries of $G$. -If we vary both ends of the identifications simultaneously, -we get another $G$-set: -\begin{example}\label{def:adjointrep} - If $G$ is a group (or \inftygp), then - \[ - \Ad_G:\BG\to\UU,\qquad\Ad_G(z)\defequi(z\eqto z) - \] - is a $G$-set (or $G$-type) called - the \emph{adjoint $G$-set (or $G$-type)}.\footnote{% - The name ``adjoint'' comes from how transport works in this case; if $p:y \eqto z$, - then $\Ad_G(p):(y\eqto y) \equivto (z\eqto z)$ is given by conjugation: - \[ - \Ad_G(p)(q)\eqto pqp^{-1} : z \eqto z. - \] - The picture - \[ - \begin{tikzcd}[ampersand replacement=\&] - y \ar[r,eqr,"p"]\ar[d,eql,"q"'] \& z \ar[d,eqr,"\Ad_G(p)(q)"] \\ - y \ar[r,eql,"p"'] \& z - \end{tikzcd} - \] - is a mnemonic device illustrating that it couldn't have been different, - and should be contrasted with the picture for - $\princ G (p):(\shape_G\eqto y)\equivto (\shape_G\eqto z)$: - \[ - \begin{tikzcd}[ampersand replacement=\&] - \shape_G \ar[r,eqr,"{\refl{\shape_G}}"]\ar[d,eql,"q"'] - \& \shape_G \ar[d,eqr,"\princ G(p)(q)"] \\ - y \ar[r,eql,"p"'] \& z. - \end{tikzcd} - \] - }\label{ft:adjoint-transport} -Notice that by the induction principle for the circle, -\[ - \sum_{z:\BG}\Ad_G(z) \jdeq \sum_{z:\BG}(z \eqto z) -\] -is equivalent to the type of (unpointed!) maps $\Sc\to\BG$, -known in other contexts as the \emph{free loop space} of $\BG$, -an apt name given that it is the type of ``all symmetries in $\BG$.'' -The first projection $\sum_{z:\BG}\Ad_G(z)\to \BG$ correspond to the function $(\Sc\to\BG)\to\BG$ given by evaluating at $\base$. -\end{example} -\begin{example} - \label{ex:HomHGasGset} - Recall that a homomorphism $f:\Hom(H,G)$ consists of an unpointed map - $F:\BH_\div\to \BG_\div$ together with a $p_f:\shape_G \eqto F(\shape_H)$, - so if, for $x:\BH$ and $y:\BG$, we define - \[ - \Hom(H,G)(x,y)\defequi\sum_{F:\BH_\div\to \BG_\div}(y\eqto F(x)) - \] - we see that $\Hom(H,G)$ may be considered to be a $H\times G$-set - \[ - \Hom(H,G) : \BH\times \BG\to\Set. - \] - We shall be particularly interested in the restriction to $G$, - giving a $G$-set for which we recycle the notation: - \[ - \Hom(H,G)(y)\defequi\Hom(H,G)(\shape_H,y)\jdeq - \sum_{F:\BH_\div\to \BG_\div}(y \eqto F(\shape_H)).\qedhere - \] -\end{example} -\begin{xca} - \label{xca:HomZGvsAdG} - Provide an identification between the $G$-sets - $\Ad_G$ and $\Hom(\ZZ,G)$ - of \cref{def:adjointrep,ex:HomHGasGset}.\footnote{% - Hint: This is similar to \cref{ex:Zinitial}: - identify $\Hom(\ZZ,G)(y)$ with $\sum_{z:\BG}\sum_{p:z\eqto z}(y \eqto z)$ - and use~\cref{lem:contract-away}.} -\end{xca} - -\begin{example}\label{def:trivGset} - If $G$ is a group and $X$ is a set, then - \[\triv_G X(z)\defequi X\] - is a $G$-set. - Examples of this sort (regardless of $X$) are called \emph{trivial $G$-sets}. -\end{example} - -\begin{remark} - \label{remark:GsetsareGsets} - A $G$-set $X$ is often presented by focusing on the underlying set $X(\shape_G)$ - and providing it with a structure relating it to $G$ determining - the entire function $X : \BG\to\Set$. - - More precisely, since $\BG$ is connected, a $G$-set $X : \BG\to\Set$ factors - through the component - $\conncomp \Set {X(\shape_G)} \jdeq \sum_{Y:\Set}\Trunc{X(\shape_G) \eqto Y}$ - that contains the point $X(\shape_G)$. - Since $\BSG_{X(\shape_G)}\jdeq(\conncomp \Set {X(\shape_G)},X(\shape_G))$, - the $G$-set $X$ can, - without loss of information, be considered as a homomorphism from $G$ to - the permutation group $\SG_{X(\shape_G)}$ of $X(\shape_G)$, - classified by a pointed map - \[ - \BG\ptdto\BSG_{X(\shape_G)}. - \] - - The constructions in the previous two paragraphs yields the following equivalences: - \[ - \GSet \equivto \sum_{X:\Set} (\BG \ptdto \BSG_X) - \equivto \sum_{X:\Set}\Hom(G,\SG_X).\qedhere - \] -\end{remark} - -\begin{xca} -Show that if $X$ is a type family with parameter type $\BG$ and $X(\shape_G)$ is a set, -then $X$ is a $G$-set. -\end{xca} - -\begin{xca}\label{xca:Ad-triv-abelian} - Prove that a group $G$ is abelian if and only if the $G$-sets $\Ad_G$ and - $\triv_G(\USymG)$ are identical. -\end{xca} - -\begin{xca}\label{xca:Ad-princ-trivial} - Prove that a group $G$ is the trivial group if and only if the $G$-sets $\Ad_G$ and - $\princ G$ are identical. -\end{xca} - -\subsection{Transitive $G$-sets} -\label{sec:transitiveGsets} -We saw in~\cref{cha:circle} that connected \coverings play a special role: -In the case of the circle, classifying the group of integers $\ZZ$, -they correspond to cycles (\cref{thm:cycset-connS1cover}). - -We hinted there that they are connected to subgroups, so -we now study them over a general group $G$. -As $G$-sets they are called transitive $G$-sets. -Classically, a $\abstr(G)$-set (a notion \emph{we} have yet not defined) $\mathcal X$ is said to be \emph{transitive} if there exists some $x:\mathcal X$ such that for all $y:\mathcal X$ there exists a $g:\mathcal X$ with $x=g\cdot y$. In our world this translates to: -\begin{definition}\label{def:transitiveGset} - A $G$-set $X:\BG\to\Set$ is \emph{transitive}\index{transitive $G$-set} if the proposition - \[ - \istrans(X) \defequi - \exists_{x:X(\shape_G)} \prod_{y:X(\shape_G)} \exists_{g:\USymG} x=g\cdot y - \] - holds. -\end{definition} -\begin{remark} - In other words, $X$ is transitive if and only if there exists - some $x:X(\shape_G)$ such that the map $\blank\cdot x:\USymG\to X(\shape_G)$ is - surjective. - - Note also that by connectedness (cf.~\cref{xca:component-connected}) - it is equivalent to demand this over all $z:\BG$: - \begin{equation}\label{eq:Gset-trans-gen} - \prod_{z:\BG}\exists_{x:X(\shape_G)} - \prod_{y:X(\shape_G)}\exists_{g:z\eqto z}a=g\cdot b. - \end{equation} - - Yet another equivalent way of expressing that $X$ is transitive is to say - that $X(\shape_G)$ is nonempty and for any $x,y:X(\shape_G)$ there - exists some $g:\USymG$ with $x = g\cdot y$. -\end{remark} - -\begin{lemma} - \label{lem:conistrans} - A $G$-set is transitive if and only if the associated \covering is connected. -\end{lemma} -\begin{proof} - Consider a $G$-set $X:\BG\to\Set$ and the associated \covering - $f:\tilde X\to\BG$ where $\tilde X\defequi\sum_{y:\BG}X(y)$ and $f$ - is the first projection. Now, $\tilde X$ is connected if and only - if there exists a $z:\BG$ and a $x:X(z)$ such that for - all $w:\BG$ and $y:X(w)$ there exists some $g:z\eqto w$ such that $y=g\cdot x$. - Since $\BG$ is connected, this is equivalent to asserting that there - exists some $x:X(\shape_G)$ such that for all $y:X(\shape_G)$ there exists - some $g:\USymG$ such that $x=g\cdot y$. -\end{proof} - -The next lemma is an analog of~\cref{cor:ConnCycles}, -but for a general group and transitive \covering -we only get injectivity, not an equivalence. -We'll study exactly when we get surjectivity in~\cref{sec:normal} -on ``normal'' subgroups. -\Cref{fig:not-normal} illustrates what can go wrong. -\begin{marginfigure} - \noindent\begin{tikzpicture}[scale=.1] - \node[dot,label=above:$x$] (two) at (0,10) {}; - \node[dot] (one) at (0, 6) {}; - \node[dot] (zero) at (0, 2) {}; - \node[dot] (base) at (0,-5) {}; - - \pgfmathsetmacro\cc{.55228475}% = 4/3*tan(pi/8) - \pgfmathsetmacro\cy{2*\cc}% - \pgfmathsetmacro\cx{10*\cc}% - \pgfmathsetmacro\intx{3.5}% - \pgfmathsetmacro\inty{1.5}% - \pgfmathsetmacro\ay{.35165954}% - - % right 3-cycle - \draw (zero.center) .. controls ++(0,-\cy+\ay) and ++(-\cx,-\ay) - .. (10,1) .. controls ++(\cx,+\ay) and ++(0,-\cy-\ay) - .. (20,4) - \foreach \y in {4,8} { - .. controls ++(0,\cy + \ay) and ++(\cx,-\ay) - .. (10,3 + \y) .. controls ++(-\cx,\ay) and ++(0,\cy-\ay) - .. (0,2 + \y) .. controls ++(0,-\cy+\ay) and ++(-\cx,-\ay) - .. (10,1 + \y) .. controls ++(\cx,\ay) and ++(0,-\cy-\ay) - .. (20,4 + \y) } - .. controls ++(0,+\cc) and ++(\cx,\ay) - .. (10+\intx,12 + \inty) .. controls ++(-\cx,-\ay) and ++(\cx,\ay) - .. (10-\intx,2 + \inty) .. controls ++(-\cx,-\ay) and ++(0,\cc) - .. (zero.center); - - % left 2-cycle - \draw (one.center) .. controls ++(0,-\cy+\ay) and ++(\cx,-\ay) - .. (-10,5) .. controls ++(-\cx,+\ay) and ++(0,-\cy-\ay) - .. (-20,8) .. controls ++(0,\cy + \ay) and ++(-\cx,-\ay) - .. (-10,11) .. controls ++(+\cx,\ay) and ++(0,\cy-\ay) - .. (two.center) .. controls ++(0,-\cy+\ay) and ++(\cx,-\ay) - .. (-10,9) .. controls ++(-\cx,\ay) and ++(0,-\cy-\ay) - .. (-20,12) .. controls ++(0,+\cc) and ++(-\cx,\ay) - .. (-10-\intx,12 + \inty) .. controls ++(\cx,-\ay) and ++(-\cx,\ay) - .. (-10+\intx,6 + \inty) .. controls ++(\cx,-\ay) and ++(0,\cc) - .. (one.center); - - % left 1-cycle - \draw (zero.center) .. controls ++(0,\cy) and ++(\cx,0) - .. (-10,4) .. controls ++(-\cx,0) and ++(0,\cy) - .. (-20,2) .. controls ++(0,-\cy) and ++(-\cx,0) - .. (-10,0) .. controls ++(\cx,0) and ++(0,-\cy) - .. (zero.center); - - % base right - \draw (base.center) .. controls (0,-5+\cy) and ++(-\cx,0) - .. (10,-3) .. controls ++(\cx,0) and ++(0,\cy) - .. (20,-5) .. controls ++(0,-\cy) and ++(\cx,0) - .. (10,-7) .. controls ++(-\cx,0) and ++(0,-\cy) .. (base.center); - % base left - \draw (base.center) .. controls (0,-5 + \cy) and (-10+\cx,-3) - .. (-10,-3) .. controls (-10-\cx,-3) and (-20,-5 + \cy) - .. (-20,-5) .. controls (-20,-5 - \cy) and (-10-\cx,-7) - .. (-10,-7) .. controls (-10+\cx,-7) and (0,-5 - \cy) - .. (base.center); - \end{tikzpicture} - \caption{A $\mkgroup(\Sc\vee\Sc)$-set for which $\protect\ev_x$ is not surjective.} - \label{fig:not-normal} -\end{marginfigure} - -\begin{lemma} - \label{lem:evisinjwhentransitive} - Let $X,X':\BG\to\Set$ be $G$-sets. Let $z:\BG$ and $x:X(z)$. Suppose that $X$ - is transitive. Then the evaluation map - \[ - \ev_x:(X \eqto X')\to X'(z),\qquad \ev_x(f)\defequi f_z(x) - \] - is injective.\footnote{% - Recall that for type families $X,X':T\to\UU$, and - $f:\prod_{y:T}X(y)\to X'(y)$, we may write $f_y:X(y)\to X'(y)$ (instead of - the more correct $f(y)$) for its evaluation at $y:T$.} -\end{lemma} -\begin{proof} - In view of function extensionality, our claim is that the evaluation - map $\ev:\prod_{x:\BG}(X(x)=X(x))\to X(y)$ given by the same formula - is injective; that is all $f$s with the same value $f_y(b)$ are - identical. - - For $a:X'(y)$, consider an $f:X=X'$ with $f_y(b)=a$. Let $z:\BG$ and - $c:X(z)$. For any $g:y=z$ such that $g\cdot b=c$ we have - $f_z(c)=f_z(g\cdot b)=g \cdot f_y(b)=g \cdot a$: the value does not - depend on $f$. Since we try to prove a proposition we are done. -\end{proof} - -\subsection{Actions in a type} -\label{sec:actions} -Oftentimes it is interesting not to have an action on a set, but on an element in any given type (not necessarily the type of sets). For instance, a group can act on another, giving rise to the notion of the semidirect product in \cref{sec:Semidirect-products}. We will return these more general types of actions many times. - -\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(\shape_G):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 \BG$ and $X \defeq \id_{\BG}$. -\end{definition} - -\begin{example} - By composing constructions we can build new actions - starting from simple building blocks. - For example, the standard action of symmetric group $\SG_n$ - is to permute the elements of the standard $n$-element set $\bn n$. - Composing with the projection $\BSG_n \to \Set$, - we get the corresponding standard $\SG_n$-set.\footnote{% - Check that this action is transitive for $n>0$.} - Composing further with the operation $\blank \to \bool : \Set \to \Set$, - we get the action of $\SG_n$ on the set of decidable subsets of $\bn n$. -\end{example} - -Generalizing~\cref{remark:GsetsareGsets}, -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$. -This equivalence maps an action $X:\BG\to A$ -to the pair consisting of $a \defeq X(\shape_G)$ -and the homomorphism represented by the pointed map -from $\BG$ to the pointed component $\conncomp A a$ given by $X$. - -Because of this equivalence, -we define a \emph{$G$-action on $a:A$} -to be a homomorphism from $G$ to $\Aut_A(a)$. - -\subsection{Fixed points and orbits} -\label{sec:fixpts-orbits} -We now return to some important constructions involving $G$-sets for a group $G$. -However, since they make equally good sense for \emph{$G$-types} for \aninftygp -$G$, we'll mostly work in that generality. -\begin{definition} - \label{def:orbittype} - If $X : G\to\UU$, then the \emph{orbit type}\index{orbit type} - of the action is\footnote{% - The superscripts and subscripts are decorated with ``$hG$'', - following a convention in homotopy theory. - This helps to distinguish them from other uses, such as powers. - The orbit type is sometimes denoted $X \dblslash G$.} -\[ - X_{hG} \defeq \sum_{z:\BG} X(z), -\] -and the type of \emph{fixed points}\index{fixed point type} as -\[ - X^{hG} \defeq \prod_{z:\BG} X(z). -\] -The \emph{set of orbits}\index{set!of orbits}\index{orbit set} is the set-truncation of the orbit type, -\[ - X / G \defeq \Trunc{X_{hG}}_0. -\] -We say that the action is \emph{transitive}\index{transitive} -if $X / G$ is contractible. -\end{definition} - -\begin{xca} - Show that the above notion of transitive coincides with the one we introduced in \cref{def:transitiveGset} for a $G$-set $X$ for an ordinary group $G$: - that $X/G$ is contractible exactly encodes that there is just one ``orbit'': - there is some $x:X(\shape_G)$ so that for any $y:X(\shape_G)$ - there is a $g:\USymG$ such that $x=g\cdot y$. -\end{xca} - -We have seen many instances of orbit types before: -When $G$-sets are considered as \coverings $f : A \to \BG$, -they are the domains $A$. -Recall for example~\cref{fig:two-comp-S1-cover}, -showing an action of $\ZZ$ on $\set{1,2,3,4,5}$ with no fixed points -and an orbit type equivalent to a sum of two circles. -In~\cref{fig:ZZ-set-orbits}, we show a similar $\ZZ$-set, -with underlying set $\set{0,1,2,3,4,5}$, three orbits, -and $5$ as a single fixed point. - -\begin{marginfigure} - \begin{tikzpicture}[scale=.15] - \node (Sc) at (0,-5) {$\B\ZZ$}; - \node[dot,label=left:$5$] (five) at (-10,30) {}; - \node[dot,label=left:$4$] (four) at (-10,22) {}; - \node[dot,label=left:$3$] (three) at (-10,18) {}; - \node[dot] (base) at (-10,-5) {}; - \node[label=left:$\Sloop$] (Sloop) at (10,-5) {}; - - \pgfmathsetmacro\cc{.55228475}% = 4/3*tan(pi/8) - \pgfmathsetmacro\cy{2*\cc}% - \pgfmathsetmacro\cx{10*\cc}% - \pgfmathsetmacro\intx{3.5}% - \pgfmathsetmacro\inty{1.5}% - \pgfmathsetmacro\ay{.35165954}% - - \draw (-10,18) .. controls (-10,18 - \cy + \ay) and (-\cx,17 - \ay) - .. (0,17) .. controls (\cx,17 + \ay) and (10,20 - \cy - \ay) .. (10,20) - .. controls (10,20 + \cy + \ay) and (\cx,23 - \ay) - .. (0,23) .. controls (-\cx,23 + \ay) and (-10,22 + \cy - \ay) - .. (-10,22) .. controls (-10,22 - \cy + \ay) and (-\cx,21 - \ay) - .. (0,21) .. controls (\cx,21 + \ay) and (10,24 - \cy - \ay) - .. (10,24) - .. controls (10,24 + \cc) and (\intx + \cx, 24 + \inty + \ay) - .. (\intx,24 + \inty) .. controls (\intx - \cx,24 + \inty - \ay) - and (-\intx + \cx,20 + \ay) - .. (-\intx,18 + \inty) .. controls (-\intx - \cx,18 + \inty - \ay) - and (-10,18 + \cc) .. (-10,18); - \draw[casblue] (-10,2) .. controls (-10,2 - \cy + \ay) and (-\cx,1 - \ay) - .. (0,1) .. controls (\cx,1 + \ay) and (10,4 - \cy - \ay) - .. (10,4) - \foreach \y in {4,8} { - .. controls (10,\y + \cy + \ay) and (\cx,3 + \y - \ay) - .. (0,3 + \y) .. controls (-\cx,3 + \y + \ay) and (-10,2 + \y + \cy - \ay) - .. (-10,2 + \y) .. controls (-10,2 + \y - \cy + \ay) and (-\cx,1 + \y - \ay) - .. (0,1 + \y) .. controls (\cx,1 + \y + \ay) and (10,4 + \y - \cy - \ay) - .. (10,4 + \y) } - .. controls (10,12 + \cc) and (\intx + \cx, 12 + \inty + \ay) - .. (\intx,12 + \inty) .. controls (\intx - \cx,12 + \inty - \ay) - and (-\intx + \cx,4 + \ay) - .. (-\intx,2 + \inty) .. controls (-\intx - \cx,2 + \inty - \ay) - and (-10,2 + \cc) .. (-10,2); - \draw (10,-5) .. controls ++(0,\cy) and ++(\cx,0) - .. (0,-3) .. controls ++(-\cx,0) and ++(0,\cy) - .. (-10,-5) .. controls ++(0,-\cy) and ++(-\cx,0) - .. (0,-7) .. controls ++(\cx,0) and ++(0,-\cy) .. (10,-5); - - \draw (10,30) .. controls ++(0,\cy) and ++(\cx,0) - .. (0,32) .. controls ++(-\cx,0) and ++(0,\cy) - .. (-10,30) .. controls ++(0,-\cy) and ++(-\cx,0) - .. (0,28) .. controls ++(\cx,0) and ++(0,-\cy) .. (10,30); - - \node[dot,label=left:$2$,casred] (two) at (-10,10) {}; - \node[dot,label=left:$1$,casred] (one) at (-10, 6) {}; - \node[dot,label=left:$0$,casred] (zero) at (-10, 2) {}; - \end{tikzpicture} - \caption{A $\ZZ$-set with three orbits and one fixed point.} - \label{fig:ZZ-set-orbits} -\end{marginfigure} - -In~\cref{fig:ZZ-set-orbits} we have highlighted a single component of -the orbit 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. -This connection is emphasized in the following result. - -\begin{lemma}\label{lem:orbit-equiv} - The map - \[ - [\blank] : X(\shape_G) \to X/G, \qquad - [x] \defeq \settrunc{(\shape_G,x)} - \] - is surjective, and $[x] = [y]$ is equivalent to - $\exists_{g:\USymG}(g\cdot x = y)$. -\end{lemma} -\begin{proof} - Surjectivity follows from the connectivity of $\BG$. - By~\cref{rem:set-trunc-as-quotient}, - $X/G \jdeq \setTrunc{X_{hG}}$ is itself the - set quotient of $X_{hg} \jdeq \sum_{z:\BG}X(z)$ by - the relation $\sim$ defined by letting $(z,x)\sim(w,y)$ - if and only if $\exists_{g:z\eqto w}(g\cdot x=y)$. - Thus,~\cref{thm:quotient-property} gives the - desired conclusion. -\end{proof} -Thus, both the underlying set $X(\shape_G)$ and the orbit type -$X_{hg}$ have equivalence relations with quotient set $X/G$.\footnote{% - This also justifies the notation $X/G$. - We have a diagram of surjective maps: - \[ - \begin{tikzcd}[ampersand replacement=\&] - X(\shape_G) \ar[rr,"{x\mapsto(\shape_G,x)}"]\ar[dr,"{[\blank]}"'] - \& \& X_{hG}\ar[dl,"{\settrunc\blank}"] \\ - \& X/G \& - \end{tikzcd} - \]} -The equivalence classes of both are important: -\begin{definition}\label{def:orbit-stabilizer} - If $X : \BG \to \Set$ is a $G$-set, and $x : X(\shape_G)$ is an - element of the underlying set, then we let - \begin{enumerate} - \item $G_x \defeq \Aut_{X_{hg}}(\shape_G,x)$ - be the \emph{stabilizer group}\index{stabilizer}% - \index{group!stabilizer} at $x$, and - \item $G\cdot x \defeq \setof{y : X(\shape_G)}{[x] =_{X/G} [y]}$ - be the \emph{orbit}\index{orbit} of $x$.\qedhere - \end{enumerate} -\end{definition} -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$) -is identified with the fiber of $[\blank] : X(\shape_G) \to X/G$, -both taken at $[x]$, the orbit containing $x$. - -Also, the base point of $\BG_x$ depends on the choice of $x$, -but the underlying type $(\BG_x)_\div$ only depends on $[x]:X/G$. -Thus, we can decompose our diagram by writing $X(\shape_G)$ and $X_{hG}$ -as sums of the respective fibers.\footnote{% - Yielding the diagram - \[ - \begin{tikzcd}[ampersand replacement=\&,column sep=tiny] - \displaystyle\sum_{b:X/G}G\cdot b \ar[rr]\ar[dr,"\fst"'] - \& \& \displaystyle\sum_{b:X/G}(\BG_b)_\div\ar[dl,"\fst"] \\ - \& X/G, \& - \end{tikzcd} - \] - where we use $b$ to denote a \emph{bane}/orbit. (Too cute?)} - -The stabilizer group $G_x$ comes equipped with a homomorphism -$i_x : \Hom(G_x,G)$, classified by -the projection $\fst:X_{hG} \to \BG$.\footnote{% - Since the projection is still a \covering, $\iota_x$ is a monomorphism - (\cref{lem:eq-mono-cover}), so $G_x$ together with $i_x$ - becomes a \emph{subgroup} of $G$. {\color{red}REORDER?}} -There are two possible extreme cases that are important: -\begin{definition}\label{def:invariant-free} - Let $X$ be a $G$-set and $x:X(\shape_G)$ an element of the underlying set. - We say that - \begin{enumerate} - \item $x$ is \emph{invariant}\index{invariant} - if $i_x$ is an isomorphism (so $G_x$ is all of $G$), - \item and $x$ is \emph{free}\index{free}\index{action!free} - is $G_x$ is trivial. - \end{enumerate} - We say that $X$ itself is \emph{free} if each $x:X(\shape_G)$ is free. -\end{definition} - -\begin{lemma}\label{lem:invariant-char} - Given a $G$-set $X$, an element $x:(\shape_G)$ is - invariant if and only if the orbit $G\cdot x$ is contractible, - \ie $x = g\cdot x$ for all $g:\USymG$. -\end{lemma} -\begin{proof} - The orbit $G\cdot x$ is the fiber of $\Bi_x : \BG_x \ptdto \BG$ - at $\shape_G$. Since $\BG$ is connected, - this is contractible if and only if all fiber of $\Bi$ are contractible, - \ie $\Bi_x$ is an equivalence, which in turn is equivalent to $i_x$ - being an isomorphism. -\end{proof} - -\begin{lemma}\label{lem:free-pt-char} - Given a $G$-set $X$, an element $x:(\shape_G)$ is\marginnote{% - Doesn't fit well here; move to where?} - free if and only if the (surjective) map - $\blank \cdot x : G \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$. -\end{proof} - -When $X : \BG \to \Set$ is a $G$-set for an ordinary group $G$, -there is another reasonable definition of the fixed points, -namely the subset -\[ - \setof{x : X(\shape_G)}{\text{$x$ is invariant}} -\] -consisting of the invariant elements. -If we evaluate a fixed point $f : \prod_{z:\BG}X(z)$ at $\shape_G$ -we do indeed land in this subset: -Letting $x\defeq f(\shape_G)$, -and taking the dependent action on paths, -$\apd{f}(g) : \pathover x X g x$, -we can use~\cref{def:pathover-trp} to conclude -$\trp[X] g(x)\jdeq g\cdot x = x$, for all $g:\USymG$. - -\begin{lemma}\label{lem:fixpts-are-fixed} - For any $G$-set $X$, evaluation at $\shape_G$ gives an equivalence - \[ - X^{hG} \jdeq \prod_{z:\BG}X(z) \equivto - \setof{x : X(\shape_G)}{\text{$x$ is invariant}}. - \] -\end{lemma} -\begin{proof} - Fix an invariant $x : X(\shape_G)$, - so $g\cdot x = x$ for all $g: \USymG$. - We need to show that the type - \[ - \sum_{f : \prod_{z:\BG}X(z)}f(\shape_G)=x - \] - is contractible. - This is equivalent to the type of pointed sections - of the projection $\fst : (X_{hG},x) \ptdto \BG$. - Since $\BG$ is connected, this is in turn equivalent - to the type of pointed sections of $\Bi_x : \BG_x \ptdto \BG$, - \ie the type of sections of the inclusion homomorphism $i_x:\Hom(G_x,G)$. - This is a proposition, and it's true if and only if $i_x$ is an isomorphism. -\end{proof} - -\section{The classifying type is the type of torsors} -\label{sec:torsors} -This section can be seen as a motivation for the use of torsors. -In \cref{sec:Gsetforabstract} we'll use this concept to prove that the type of groups and the type of abstract groups are equivalent by classifying abstract groups via their pointed connected groupoid of torsors. To see how this might work it is good to start with the case of a (concrete) group $G$. -In the end we want the torsors of $\abstr(G)$ to be equivalent to $\BG$, so to get the right definition we should first explore what the torsors of $G$ look like and prove~\cref{lem:BGbytorsor}, showing that $\BG$ is equivalent to the type of $G$-torsors. -\begin{definition} - Given a group $G$, the type of \emph{$G$-torsors}% - \index{torsor@torsor}% - \glossary(TorsorG){$\protect\typetorsor_G$}{the type of $G$-torsors}% - \footnote{This works equally well with $\infty$-groups: $G$-torsors are in that case $G$-types in the component of the principal torsor $\princ G:\BG\to\UU$. There is no conflict with the case when the $\infty$-group $G$ is actually a group since then any $G$-type in the component of the principal $G$-torsor will be a $G$-set.} - is - \[ - \typetorsor_G\defequi\sum_{X:\GSet}\Trunc{\princ G \eqto X}, - \] - where $\princ G$ is the principal $G$-torsor of \cref{def:principaltorsor}. -\end{definition} - -\begin{xca}\label{xca:torsor=free+transitive} - Show that a $G$-set is a $G$-torsor if and only if it is free and transitive. -\end{xca} - -\begin{remark} - For $G$ a group, the type of $G$-torsors is just another name for the component of the type of \coverings of $\BG$ containing the universal \covering. - - Observe that for a group $G$, $\typetorsor_G$ is a connected groupoid\footnote{Admittedly in a higher universe, but we can use the - Replacement~\cref{pri:replacement} to see that $\typetorsor_G$ is equivalent - to a type in the same universe as $G$ -- even before we - have~\cref{lem:BGbytorsor} showing we can take $\BG$.} - and so -- by specifying the base point $\princ G$ -- it represents a group! - Guess which one! -\end{remark} - -For $y:\BG$, recall from~\cref{def:principaltorsor}\eqref{eq:pathsp} -the definition of $\pathsp y:\BG\to\Set$ as the -$G$-set with $\pathsp y(z)\jdeq(y\eqto z)$ -(so that in particular $\princ G\jdeq\pathsp{\shape_G}$). -Note that $\pathsp y$ is a $G$-torsor, so we can wrap these up as follows: - -\begin{definition} - \label{def:BG2TorsG} - Let - \[ - \pathsp{}:\BG\ptdto(\typetorsor_G,\princ G) - \] - be the pointed map given by sending $z:\BG$ to $\pathsp z$ - and by the identification - $\refl{\pathsp{\shape_G}}:\princ G\eqto\pathsp{\shape_G}$.\footnote{% - That is, we have classified a homomorphism from $G$ - to $\Aut_{\GSet}(\princ G)$. We don't bother giving it a name, - however, since it'll turn out to an isomorphism.} -\end{definition} -If $G$ is not clear from the context, we may choose to write $\pathsp{}^G$ instead of $\pathsp{}$. - -\begin{example}\label{ex:pathsptransport} - For $y,z:\BG$ we make the induced map - \[ - \pathsp{}:(y\eqto z)\to (\pathsp y\eqto \pathsp z), - \] - or rather its composite with the identification with - $\prod_{x:\BG}\pathsp y(x)\eqto \pathsp z(x)$, - explicit. - For $q:y\eqto z$, the transport - $\pathsp q:\prod_{x:\BG}\pathsp y(x)\eqto \pathsp z(x)$ - is obtained - by sending $p:\pathsp y(x)\jdeq (y\eqto x)$ to\footnote{In a picture, - \[ - \begin{tikzcd}[ampersand replacement=\&] - y \ar[r,eqr,"q"]\ar[d,eql,"p"'] \& z \ar[d,eqr,"{\pathsp q(p)}"] \\ - x \ar[r,eql,"{\refl x}"'] \& x. - \end{tikzcd} - \]} - \[ - \pathsp q(p)\eqto pq^{-1}:\pathsp z(x)\jdeq(z\eqto x).\qedhere - \] -\end{example} - -\begin{lemma}\label{lem:pathsptransportiseq} - For $y,z:\BG$ the induced map (\ie transport) of identity types - \[ - \pathsp{}:(y\eqto z)\to (\pathsp y\eqto \pathsp z) - \] - is an equivalence.\footnote{% - For connoisseurs of category theory, - this is also a corollary of a \emph{type-theoretic Yoneda lemma}, - stating that transport gives an equivalence - \[ - X(a) \equivto \prod_{b:A}\bigl((a \eqto b) \to X(b)\bigr) - \] - for any pointed type $(A,a)$ and type family $X: A \to \UU$. - Try to prove this yourself!} -\end{lemma} -\begin{proof} - We craft an inverse $Q:(\pathsp y\eqto \pathsp z) \to (y\eqto z)$ for - $\pathsp{}$. Given an identity $f:\pathsp y \eqto \pathsp z$, the map - $f_y: (y\eqto y) \to (z\eqto y)$ maps the reflexivity path $\refl y$ to a path - $f_y(\refl y):z\eqto y$, and we define - \[ - Q(f) \defequi \inv{f_y(\refl y)}. - \] - First, $Q$ is an inverse on the right for $\pathsp{}$ as - $\pathsp {Q(f)}$ is the map $p \mapsto p f_y(\refl y)$, and - by induction on $p:y\eqto x$, we have $p f_y(\refl y) \eqto f_x(p)$ - (this indeed holds when $p\jdeq \refl y$). - This means that we have $\pathsp {Q(f)} \eqto f$. - Next, we show that $Q$ is an inverse on the left for - $\pathsp{}$: indeed for any $q:y \eqto z$ we have - $\inv{\pathsp{q}(\refl y)} \eqto \inv{(\refl y \inv q)} \eqto q$; in other - words $Q(\pathsp q)\eqto q$, as desired. -\end{proof} - -\begin{theorem}\label{lem:BGbytorsor} - If $G$ is a group (or \inftygp), then the function - $\pathsp{}:\BG\to\typetorsor_G$ from~\cref{def:BG2TorsG} - is an equivalence. - Univalence then allows us to derive an identity - \[\bar{\pathsp{}}:G\eqto\Aut_{\GSet} (\princ G)\] - of groups.\footnote{For $\infty$-groups: $G \eqto \Aut_{\BG\to\UU}(\princ G)$.} -\end{theorem} - -\begin{proof} - Since both $\typetorsor_G$ and $\BG$ are connected, it suffices by - \cref{cor:fib-vs-path} to show that each - $\ap {\pathsp{}}:(y\eqto z)\to(\pathsp y\eqto \pathsp z)$ is an - equivalence. We first observe that $\ap {\pathsp{}}$ is indeed - the function - \[ - \pathsp{}:(y\eqto z)\to(\pathsp y\eqto\pathsp z) - \] - made explicit in \cref{ex:pathsptransport}. Indeed, by induction - on $q:y\eqto z$, we have - \[ - \ap {\pathsp{}}(\refl y) \jdeq \refl {\pathsp y} \eqto (p\mapsto p\inv{\refl y}). - \] - Then~\cref{lem:pathsptransportiseq} states exactly that $\ap P$ is - an equivalence. -\end{proof} - -\subsection{Homomorphisms and torsors} -\label{sec:homotor} -In view of the equivalence $\pathsp{}^G$ between $\BG$ and $(\typetorsor_G,\princ G)$ of \cref{lem:BGbytorsor} one might ask what a group homomorphism $f:\Hom(G,H)$ translates to on the level of torsors. Off-hand, the answer is the round-trip $(\pathsp{}^H)\Bf(\pathsp{}^G)^{-1}$, but we can be more concrete than that. -We do know that for $x:\BG$ the $G$-torsor $\pathsp x^G$ should be sent to -$\pathsp {\Bf(x)}^H$, but how do we express this for an arbitrary $G$-torsor? -\begin{definition} - \label{def:restrictandinduce} - Let $f:\Hom(G,H)$ be a group homomorphism. If $Y:\BH\to\Set$ is an $H$-set, - then the \emph{restriction}\index{action!restricted}\index{restriction} - $f^*Y$ of $Y$ to $G$ is the $G$-set given by precomposition - \[ - f^*Y\defequi Y\,\Bf:\BG\to\Set. - \] - - If $X:\BG\to\Set$ is a $G$-set, we define - the \emph{induced $H$-type}\index{action!induced}\index{induced action}\footnote{% - Note that the induced $H$-type may or may not be an $H$-\emph{set}. - As an example, consider the homomorphism $f\defeq(\blank\mod 2) : \Hom(\ZZ,\SG_2)$ - discussed in~\cref{ex:groups-morphisms}, given by sending $\base:\Sc$ - to $\bn 2$ and $\Sloop$ to the twist. (This is classified by the function - $R_2$ from~\cref{def:RmtoS1}.) - - The induced $\SG_2$-set $f_*\bn 1$ of the trivial - $\ZZ$-set on the unit type $\bn 1$ is given by - \[A\mapsto \sum_{z:\Sc}(R_2(z)\eqto A)\times \bn 1,\] - which has underlying type equivalent to $\sum_{z:\Sc}R_2(z)$, which we know - back from~\cref{rem:finitecoveringsofS1} to be a circle. - So the induced $\SG_2$-type in question is \emph{not} a set. - - This situation is common in algebra and is often referred to by saying - that some construction is not ``exact''.} - $f_*X : \BH\to\UU$ by setting, for $y:\BH$, - \[ - f_*X(y)\defequi\sum_{x:\BG}(\Bf(x) \eqto y)\times X(x).\qedhere - \] -\end{definition} -Note that the type $f_*X(y)$ is also the orbit type $(H^y \times X)_{hG}$, -of the $G$-set $H^y\times X$, -where $(H^y\times X)(x) \defeq (\Bf(x) \eqto y)\times X(x)$ for $x:\BG$, -and whose underlying set is equivalent to $(\shape_H\eqto y)\times X(\shape_G)$. - -\begin{remark} - Dually, there is also a \emph{coinduced $H$-set}\index{action!coinduced} - $f_!:\BH\to\Set$ given by - \[ - f_!X(y)\defeq\prod_{x:\BG}\bigl((\Bf(x)\eqto y) \to X(x)\bigr). - \] - Note that this always lands in sets when $X$ does. -\end{remark} - -When $X$ is the $G$-torsor $\pathsp x^G$, for some $x:\BG$, -the contraction (recall \cref{lem:contract-away}) -of $\sum_{z:\BG}(x\eqto z)$ induces an equivalence -\[ - \eta_y:f_*\pathsp x^G(y) \jdeq \sum_{z:\BG}(\Bf(z) \eqto y)\times(x \eqto z) - \equivto (\Bf(x)\eqto y)\jdeq\pathsp{\Bf(x)}^H(y). -\] -The resulting identity $\bar\eta:f_*\pathsp x^G\eqto \pathsp{\Bf(x)}^H$ shows that for every $G$-torsor $X$ the $H$-type $f_*X$ is an $H$-torsor. -Furthermore, when $x\jdeq\shape_G$, so $\pathsp x^G\jdeq\princ G$ -is the principal $G$-torsor, the pointedness path $\Bf_\pt : \shape_H\eqto\Bf(\shape_G)$ -gives an identification $f_*\princ G\eqto \princ H$. - -Summing up, we have proved: -\begin{lemma} - \label{lem:inducedtorsor} - Let $f:\Hom(G,H)$ be a group homomorphism. - If $X$ is a $G$-torsor, then the induced $H$-type $f_*X$ is an $H$-torsor, - and so we get an induced map - \[ - f_*:\typetorsor_G\ptdto\typetorsor_H, - \] - such that the diagram of pointed maps - \[ - \begin{tikzcd} - \BG \ar[r,"\Bf"]\ar[d,"{\pathsp{}^G}"'] & - \BH\ar[d,"{\pathsp{}^H}"] \\ - \typetorsor_G \ar[r,"f_*"'] & \typetorsor_H - \end{tikzcd} - \] - commutes. -\end{lemma} - -\begin{remark} - \label{rem:inducedGsetfromabstracthomomorphisms} - Notice that our construction of the induced $G$-set works equally well for - a homomorphism of abstract groups $\phi:\Hom^\abstr(\abstr(G),\abstr(H))$: - if $X:\BG\to\Set$ is a $G$-set, then we can - define the $H$-set $\phi_*X:\BH\to\Set$ by - \[ - \phi_*X(y)\defequi (\shape_H \eqto y) \times_G X(\shape_G) - \] - to be the set quotient of $(\shape_H\eqto y)\times X(\shape_G)$ by - the relation - $(p,x)\sim(p\, \phi(q)^{-1},q\cdot x)$ for all $q:\shape_G=\shape_G$. - Just as above, for $X$ the principal $G$-torsor we get an identity - $\eta_\phi:\phi_*\princ G=\princ H$ which, when evaluated at $y:\BH$, - corresponds under univalence to the equivalence - \[ - (\shape_H\eqto y)\times_G\USymG\equivto (\shape_H\eqto y) - \] - sending $[(p,q)]$ to $p\,\phi(q):(\shape_H\eqto y)$.\footnote{% - \color{red}I'd like to rephrase this in terms of noticing - when $f_*X$ is a set, or maybe redefining $f_*X$ to always take the - set truncation.} -\end{remark} - - -\section{Groups; concrete vs.~abstract% -- same gem, different wrapping -} -\label{sec:Gsetforabstract} - -We use \cref{lem:BGbytorsor} as our inspiration for trying to construct a group from an abstract group. -That is, in total analogy, we define the torsors for an abstract group, -and it will then be a relative simple matter to show that the processes of -\begin{enumerate} -\item forming the abstract group of a group and -\item taking the group represented by the torsors of an abstract group -\end{enumerate} - are inverse to each other. -\marginnote{% -Note that we have not considered an ``abstract'' counterpart of the concept of $\infty$-group, so all we do in this section is set-based. -} -\begin{definition} -\label{def:abstrGtorsors} -If ${\agp G}=(S,e,\mu,\iota)$ is an abstract group, a \emph{$\agp G$-set}% -\index{Gset@$\agp G$-set (of abstract group)} -is a set $\mathcal X$ together with a homomorphism -$\agp G\to\abstr(\Sigma_{\mathcal X})$ -from $\agp G$ to the (abstract) permutation group of $\mathcal X$: -$$Set_{\agp G}^\abstr\defequi \sum_{\mathcal X:\Set}\Hom_\abstr({\agp G},\abstr(\Sigma_{\mathcal X})).$$ - -The \emph{principal ${\agp G}$-torsor} $\princ {\agp G}^\abstr$ is the ${\agp G}$-set consisting of the underlying set $S$ together with the homomorphism ${\agp G}\to\abstr(\Sigma_{S})$ with underlying function of sets $S\mapsto (S=S)$ given by sending $g:S$ to $\mathrm{ua}(s\mapsto s\cdot g^{-1})$. - -The type of \emph{${\agp G}$-torsors} is -$$\typetorsor_{\agp G}^\abstr\defequi\sum_{S:\Set_{\agp G}^\abstr}\Trunc{\princ {\agp G}^\abstr=S}.$$ -\end{definition} -\begin{example} - If $G$ is a group we can unravel the definition and see that an $\abstr(G)$-set consists of - \begin{enumerate} - \item a set $S$, - \item a function $f:\USymG\to (S=S)$ - \item such that $f(e_G)=\refl{S}$ and for all $p,q:\USymG$ we have that $f(p\, q)=f(p)\,f(q)$. - \end{enumerate} - -\end{example} - - -To help reading the coming proofs we introduce some notation that is redundant, but may aid the memory in cluttered situations: Let $x,y,z$ be elements in some type, then -\marginnote{We recognize $\preinv$ from \cref{lem:pathsptransportiseq} as the induced map of identity types $\pathsp{}\colon (y=z)\to(\pathsp y=\pathsp z)$ evaluated at $x$, while post-composition $\post$ is transport in the family $\pathsp x$.} -\begin{align*} -% \pre:(x=y)\to ((y=z)=(x=z)),\qquad&\pre(q)(p)\defequi pq\\ - \preinv:(y=x)\to ((y=z)=(x=z)),\quad&\preinv(q)(p)\defequi\pathsp qp\defequi pq^{-1}\\ - \post:(y=z)\to ((x=y)=(x=z)),\quad&\post(p)(q)\defequi\post_pq\defequi pq\\ - %\adjoint:(x=y)\to((x=x)=(y=y)),\qquad&\adjoint(q)(p)\defequi\adjoint_qp\defequi qpq^{-1} -\end{align*} - - -\begin{example}\label{ex:qG} - If $G$ is a group, then for any $x:\BG$ the principal $G$-torsor \emph{evaluated at $x$}, \ie the set $\princ Gx\defequi(\shape_G=x)$, has a natural structure of an $\abstr(G)$-set by means of - $$\preinv:\USymG\to ((\shape_G=x)=(\shape_G=x))$$ and the fact that $\preinv(e_G)\defequi\refl{\shape_G=x}$ and that for $p,q:\USymG$ we have that - \marginnote{\ie if $r\colon \shape_G=x$ we have that -$\preinv(p\, q)(r)=r(p\,q)^{-1}=r\,q^{-1}p^{-1}=\preinv(p)\preinv(q)(r)$ -- demonstrating why we chose $\preinv$: without the inverse this would have gone badly wrong.} - $$\preinv(p\,q)=\preinv(p)\preinv(q).$$ - - -That this $\abstr(G)$-set is an $\abstr(G)$-torsor then follows since $\BG$ is connected (any $\shape_G=x$ will serve as a proof of $(\shape_G=x,\preinv,!)=\princ{\abstr(G)}^\abstr$). - -Though it sounded like we made a choice ending up with $\preinv$; we really didn't -- it is precisely what happens when you abstract the homomorphism $G\to\Sigma_{\princ G(x)}$: -you get the function of identity types -$$\USymG\to (\princ G(x)=\princ G(x))$$ -which by the very definition of transport for $\princ G$ is $\preinv$. -\end{example} - -\begin{definition} - If ${\agp G}$ is an abstract group, then the \emph{concrete group $\concr({\agp G})$ associated with ${\agp G}$} is the group given by the pointed connected groupoid $(\typetorsor_{\agp G}^\abstr,\princ {\agp G})$. -\end{definition} -We give the construction of \cref{ex:qG} a short name since it will occur in important places. -\begin{definition} - Let $G$ be a group. - The group homomorphism - $$q_G:\Hom(G,\concr(\abstr(G)))$$ - is defined in terms of the pointed map by the same name -$$q_G:\BG\to_* (\typetorsor^\abstr_{\abstr(G)},\princ {\abstr(G)}),\quad q_G(z)=(\princ G(z),\preinv,!).$$ -\end{definition} - -\begin{lemma} - \label{lem:Groupsareidentitytypes} -For all groups $G$, the pointed function $q_G:G\to_*\concr(\abstr(G))$ -is a equivalence. -\end{lemma} -\begin{proof} - To prove that $q_G$ is an equivalence it is, by \cref{cor:fib-vs-path}\ref{conn-fib-vs-path}, enough to show that if $x,y:\BG$ then the induced map -$$q_G:(x=_{\BG}y)\to (q_G(x)=q_G(y)) -$$ -is an equivalence. - Now, $q_G(x)=q_G(y)$ is equivalent to the set -$$ -((\shape_G=x),\preinv)=_{\abstr(G)\text{-set}}((\shape_G=y),\preinv)$$ -which in turn is equivalent to -$$\sum_{f:(\shape_G=x)=(\shape_G=y)}f\preinv=\preinv f -$$ - ($f\preinv=\preinv f$ is shorthand for $\prod_{q:\shape_G=x}\prod_{p:\shape_G=p}f(pq^{-1})=f(p)q^{-1}$ and the rest of the data is redundant at the level of symmetries) and under these identities $q_G$ is given by -$$(\post,!):(x=y)\to \sum_{f:(\shape_G=x)=(\shape_G=y)}f\preinv=\preinv f.$$ -Given an element -$(f,!):\sum_{f:(\shape_G=x)=(\shape_G=y)}f\preinv=\preinv f$, the preimage -$(\post,!)^{-1}(f,!)$ is equivalent to the set -$\sum_{r:x=y}(f=\post_r)$. But if $(r,!),(s,!): \sum_{r:x=y}(f=\post_r)$, then for all $p:\shape_G=x$ we get that $r\,p=f(p)=s\,p$, that is $r=s$, so that the preimage is in fact a proposition. -To show that the preimage is contractible, it is enough to construct a function $(\shape_G=x)\to \sum_{r:x=y}(f=\post_r)$, and sending $p$ to $f(p)p^{-1}$ will do. -\end{proof} - -\begin{example} - \label{ex:abstrconcrG} - Let ${\agp G}=(S,e,\mu,\iota)$ be an abstract group. -Then the underlying set of $\abstr(\concr({\agp G}))$ is $\princ {\agp G}^\abstr=_{\typetorsor^\abstr_{\agp G}}\princ {\agp G}^\abstr$. -Unraveling the definitions we see that this set is equivalent to -$$\sum_{p:S=S}\prod_{q,s:S}(p(s\,q^{-1})=p(s)\,q^{-1}). -$$ -Setting $s\defequi e$ and renaming $t\defequi q^{-1}$ in the last equation, we see that $p(t)=p(e)t$; that is $p$ is simply multiplication with an element $p(e):S$. in other words, the function -$$r_{\agp G}:S\to \sum_{p:S=S}\prod_{q,s:S}(p(s\,q^{-1})=p(s)\,q^{-1}),\qquad r_{\agp G}(u)\defequi(u\cdot\,,!) -$$ -is an equivalence of sets, which we by univalence is converted into an identity. -The abstract group structure of $\abstr(\concr({\agp G}))$ is given by it being the symmetries of $\princ {\agp G}^\abstr$; translated to $\sum_{p:S=S}\prod_{q,s:S}(p(s\,q^{-1})=p(s)\,q^{-1})$ this corresponds via the first projection to the symmetries of $S$. -This means that we need to know that if $u,v:S$ and consider the two symmetries $u\cdot,v\cdot:S=S$, then their composite (the operation on the symmetry on $S$) is equal to $(u\cdot v)\cdot:S=S$ (the abstract group operation), but this is true by associativity ($u\cdot(v\cdot s)=(u\cdot v)\cdot s$). That $r_{\agp G}$ also sends $e:S$ to $\refl S$ is clear. -Hence our identity $r_{\agp G}$ underlies an identity of abstract groups -$$r_{\agp G}:{\agp G}=_{\typegroup^\abstr}\abstr(\concr({\agp G})).$$ -\end{example} - -This shows that every abstract group encodes the symmetries of something essentially unique. Summing up the information we get -\begin{theorem} - \label{thm:Groupsareidentitytypes} - Let ${\agp G}$ be an abstract group. Then -$$\abstr:\typegroup\to\typegroup^\abstr$$ is an equivalence. -\end{theorem} - -\section{Homomorphisms; abstract vs.~concrete} -\label{sec:homabsisconcr} - -Now that we know that the type of groups is identical to the type of abstract groups, it is natural to ask if the notion of group homomorphisms also coincide. - -They do, and we provide two independent and somewhat different arguments. Translating from group homomorphisms to abstract group homomorphisms is easy: if $G$ and $H$ are groups, then we defined -$$\abstr:\Hom(G,H)\to\Hom^\abstr(\abstr(G),\abstr(H))$$ -in \cref{def:abstrisfunctor} as the function which takes a homomorphism, aka a pointed map $f=(\Bf_\div,p_f):\BG\ptdto\BH$ to the induced map of identity types -$$\US f\defequi \mathrm{ad}_{p_f}\ap{\Bf_\div}:\USymG\to\USymH$$ - together with the proofs that this is an abstract group homomorphism from $\abstr(G)$ to $\abstr(H)$, c.f~\cref{def:abstrisfunctor}. - - -Going back is somewhat more involved, and it is here we consider two approaches. -The first is a compact argument showing directly how to reconstruct a pointed map $\Bf:\BG\ptdto\BH$ from an abstract group homomorphism from $\abstr(G)$ to $\abstr(H)$, the second translates back and forth via our equivalence between abstract and concrete groups. - - - -The statement we are after is - - -\begin{lemma} - \label{lem:homomabstrconcr} - If $G$ and $H$ are groups, then -$$\abstr:\Hom(G,H)\to\Hom^\abstr(\abstr(G),\abstr(H))$$ -is an equivalence. -\end{lemma} -and the next two subsections offer two proofs. - - - -\sususe{``Delooping'' a group homomorphism} -\label{sec:delooping} %after Coquand, after Deligne -We now explore the first approach. -It might be helpful to review \cref{lem:S1-delooping} -for a simple example of delooping in the special case of the circle. -Here we elaborate the general case. - -\begin{proof} - Suppose we are given an abstract group homomorphism -$$f:\Hom^\abstr(\abstr(G),\abstr(H))$$ -and we explain how to build a map $g:\BG_\div \rightarrow \BH_\div$ with -a path $p:\shape_H = g(\shape_G)$ such that $p f(\omega) = g(\omega) p$ -for all $\omega:\shape_G = \shape_G$ (so that $g$ is a ``delooping'' of $f$, that is, $f=\abstr(g)$). -\marginnote{We will thus have displayed a map $\mathrm{deloop}:\Hom^\abstr(\abstr(G),\abstr(H))\to\Hom(G,H)$ with $\abstr\,\mathrm{deloop}=\refl{}$. We leave it to the reader to prove that $\mathrm{deloop}\,\abstr=\refl{}$. } - -To get an idea of our strategy, let us assume the problem solved. The map $g:\BG_\div\rightarrow \BH_\div$ -will then send any path $\alpha:{\shape_G} = x$ to a path $g(\alpha):g({\shape_G}) = g(x)$ -and so we get a family of paths $p(\alpha) \defequi g(\alpha) p$ in ${\shape_H} = g(x)$ such that -$$p(\alpha\omega) = g(\alpha)g(\omega)p - = g(\alpha)pf(\omega) = p(\alpha)f(\omega)$$ -for all $\omega:{\shape_G} = {\shape_G}$ and $\alpha : {\shape_G} = x$. - -This suggests to introduce the following family -$$ -C(x)~:=~ \sum_{y:\BH_\div}\sum_{p:({\shape_G}=x)\rightarrow ({\shape_H} = y)}~~~\prod_{\omega:{\shape_G}={\shape_G}}\prod_{\alpha:{\shape_G}=x}~ - p(\alpha\omega) = p(\alpha)f(\omega) -$$ - An element of $C(x)$ has three components, the last component being - a proposition since $\BH_\div$ is a groupoid. - - The type $C({\shape_G})$ has a simpler description. An element of $C({\shape_G})$ is - a pair $y,p$ such that $p(\alpha\omega) = p(\alpha)f(\omega)$ for - $\alpha$ and $\omega$ in ${\shape_G}={\shape_G}$. - Since $f$ is an abstract group homomorphism, this condition - can be simplified to $p(\omega) = p(1_{\shape_G})f(\omega)$, and the map $p$ - is completely determined by $p(1_{\shape_G})$. - Thus $C({\shape_G})$ is equal to $\sum_{y:\BH_\div}{\shape_H} = y$ and is contractible. - - - It follows that we have - $$ - \prod_{x:\BG_\div}~ ({\shape_G} = x)\rightarrow\iscontr~ C(x) - $$ -and so, since $\iscontr~C(x)$ is a proposition - $$ - \prod_{x:\BG_\div}~ \Trunc{a = x}\rightarrow\iscontr~ C(x) - $$ - Since $\BG_\div$ is connected, we have - $\prod_{x:\BG_\div}\iscontr~ C(x)$ - and so, in particular, we have an element of $\prod_{x:\BG_\div}C(x)$. - - We get in this way a map $g:\BG_\div\rightarrow \BH_\div$ - together with a map $p:(a=x)\rightarrow ({\shape_H} = g(x))$ such that - $p (\alpha\omega) = p(\alpha) f(\omega)$ - for all $\alpha$ in ${\shape_G}=x$ and $\omega$ in ${\shape_G}={\shape_G}$. -We have, for $\alpha:{\shape_G}=x$ -$$\prod_{x':\BG_\div}\prod_{\lambda:x=x'}~p(\lambda\alpha) = g(\lambda)p(\alpha)$$ -since this holds for $\lambda = 1_x$. -In particular, $p(\omega) = g(\omega)p(1_{\shape_G})$. - -We also have $p(\omega) = p(1_{\shape_G})f(\omega)$, hence -$p(1_{\shape_G})g(\alpha) = f(\alpha)p(1_{\shape_G})$ -for all $\alpha:\shape_G=\shape_G$ and we have found a delooping of $f$. - -%Security copy if things go wrong. BID: delete by May 1 -% Let $(X,a)$ and $(Y,b)$ be two pointed connected $1$-types. -% We suppose given a abstract group homomorphism -% $$f:a = a\rightarrow b = b$$ -% and we explain how to build a map $g:X \rightarrow Y$ with -% a path $p:b = g(a)$ such that $p f(\omega) = g(\omega) p$ -% for all $\omega:a = a$. (So $g$ is a ``delooping'' of $f$.) - -% \medskip - -% Let us assume the problem solved. The map $g:X\rightarrow Y$ -% will then send any path $\alpha:a = x$ to a path $g(\alpha):g(a) = g(x)$ -% and so we get a family of paths $p(\alpha) = g(\alpha) p$ in $b = g(x)$ such that -% $$p(\alpha\omega) = g(\alpha)g(\omega)p -% = g(\alpha)pf(\omega) = p(\alpha)f(\omega)$$ -% for all $\omega:a = a$ and $\alpha : a = x$. - -% \medskip - -% This suggests to introduce the following family -% $$ -% C(x)~:=~ \sum_{y:Y}\sum_{p:(a=x)\rightarrow (b = y)}~~~\prod_{\omega:a=a}\prod_{\alpha:a=x}~ -% p(\alpha\omega) = p(\alpha)f(\omega) -% $$ - -% An element of $C(x)$ has three components, the last component being -% a proof since $Y$ is a $1$-type. - -% The type $C(a)$ has a simpler description. An element of $C(a)$ is -% a pair $y,p$ such that $p(\alpha\omega) = p(\alpha)f(\omega)$ for -% $\alpha$ and $\omega$ in $a=a$. Since $f$ is a group morphism, this condition -% can be simplified to $p(\omega) = p(1_a)f(\omega)$, and the map $p$ -% is completely determined by $p(1_a)$. -% Thus $C(a)$ is equal to $\sum_{y:Y}b = y$ and is contractible. - -% \medskip - -% It follows that we have -% $$ -% \prod_{x:X}~ a = x\rightarrow\iscontr~ C(x) -% $$ -% and so, since $\iscontr~C(x)$ is a proposition -% $$ -% \prod_{x:X}~ \Trunc{a = x}\rightarrow\iscontr~ C(x) -% $$ -% Since $X$ is connected, we have -% $\prod_{x:X}\iscontr~ C(x)$ -% and so, in particular, we have an element of $\prod_{x:X}C(x)$. - -% We get in this way a map $g:X\rightarrow Y$ -% together with a map $p:(a=x)\rightarrow (b = g(x))$ such that -% $p (\alpha\omega) = p(\alpha) f(\omega)$ -% for all $\alpha$ in $a=x$ and $\omega$ in $a=a$. -% We have, for $\alpha:a=x$ -% $$\prod_{x':X}\prod_{\lambda:x=x'}~p(\lambda\alpha) = g(\lambda)p(\alpha)$$ -% since this holds for $\lambda = 1_x$. -% In particular, $p(\omega) = g(\omega)p(1_a)$. - -% We also have $p(\omega) = p(1_a)f(\omega)$, hence -% $p(1_a)g(\alpha) = f(\alpha)p(1_a)$ -% for all $\alpha:a=a$ and we have found a delooping of $f$. -\end{proof} - - -\sususe{The concrete vs. abstract homomorphisms via torsors.} -\label{sec:absconctorsor} - -The second approach to \cref{lem:homomabstrconcr} is as follows: - - -\begin{proof} - The equivalence of $\pathsp{}^G:\BG\we(\typetorsor_G,\princ G)$ of \cref{lem:BGbytorsor} gives an equivalence -$$\pathsp{}:\Hom(G,H)\we((\typetorsor_G,\princ G)\to_*(\typetorsor_H,\princ H)) -$$ -Consider the map -$$A:((\typetorsor_G,\princ G))\to_*(\typetorsor_H,\princ H)\to \Hom^\abstr(\abstr(G),\abstr(H))$$ -given by letting $A(f,p)$ be the composite -$$\xymatrix{\USymG\ar@{=}[d]^{\pathsp{}^G}_\downarrow&&& - \USymH\ar@{=}[d]^{\pathsp{}^H}_\downarrow\\ - (\princ G=\princ G)\ar[r]^-f& - (f\princ G=f\princ G)\ar@{=}[rr]^-{q\mapsto p^{-1}qp}_\to&& - (\princ H=\princ H) -}$$ -(together with the proof that this is an abstract group homomorphism). We -are done if we show that $A$ is an equivalence. -\marginnote{The reason to complicate $\abstr$ this way is that it gets easier to write out the inverse function.} - -If $(\phi,!):\Hom^\abstr(\abstr(G),\abstr(H))$ and $X:\BG\to\Set$ is a $G$-torsor, recall the induced $H$-torsor $\phi_*X$ from \cref{rem:inducedGsetfromabstracthomomorphisms} and the identity $\eta_\phi:\phi_*\princ G=\princ H$. -Let -$$B: \Hom^\abstr(\abstr(G),\abstr(H))\to ((\typetorsor_G,\princ G)\to_*(\typetorsor_H,\princ H)$$ -be given by $B(\phi,!)=(\phi_*X,\eta_\phi)$ - -We show that $A$ and $B$ are inverse equivalences. Given an abstract group homomorphism $(\phi,!):\Hom^\abstr(\abstr(G),\abstr(H))$, then $AB(\phi,!)$ has as underlying set map -$$\xymatrix{\USymG\ar@{=}[d]^{\pathsp{}^G}_\downarrow&&& - \USymH\ar@{=}[d]^{\pathsp{}^H}_\downarrow\\ - (\princ G=\princ G)\ar[r]^-{\phi_*}& - (\phi_*\princ G=\phi_*\princ G)\ar@{=}[rr]^-{q\mapsto \eta_\phi^{-1}q\eta_\phi}_\to&& - (\princ H=\princ H), -}$$ -and if we start with a $g:\USymG$, then $\pathsp{}^G$ sends it to $\pathsp g^G\oldequiv\preinv (g)$. Furthermore, $\phi_*\preinv (g)$ is $[\id,\preinv (g)]$ which is sent to $\preinv (\phi(g))$ in $\princ H=\princ H$ which corresponds to $\phi(g):\USymH$ under $\pathsp{}^H$. In other words, $AB(\phi,!)=(\phi,!)$. The composite $BA$ is similar. -\end{proof} - - -\section{Monomorphisms and epimorphisms} -\label{sec:monoepi} - -In set theory we say that a function $f:B\to C$ of sets is an injection if for all $b,b':B$ we have that $f(b)=f(b')$ implies that $b=b'$. This conforms with our definitions. -%\footnote{This continues to be true in type theory, but since equality needs not be unique, we should in addition require that the two identities $p, f(\sigma(p)):f(b)=f(b')$ are equal.} -Furthermore, since giving a term $b:B$ is equivalent to giving a (necessarily constant) function $c_b:\bn 1\to B$, we could alternatively say that a function $f:B\to C$ is an injection if and only if for any two $g,h:\bn 1\to B$ such that $fg=fh$ we have that $g=h$. In fact, by function extensionality we can replace $\bn 1$ by any set $A$ (two functions are identical if and only if they have identical values at every point). - -Similarly, a function $f:B\to C$ is surjective if for all $c:C$ the preimage $f^{-1}(c)=\sum_{b:B}c=f(b)$ is non-empty. A smart way to say this is to say that the first projection from $\sum_{c:C}\Trunc{f^{-1}(c)}$ to $C$ is an equivalence. Since $B$ is always equivalent to $\sum_{c:C}f^{-1}(c)$, we see that for a surjection $f:B\to C$ and family of propositions $P:C\to \Prop$, the propositions $\prod_{c:C}P(c)$ and $\prod_{b:B}Pf(b)$ are equivalent. In particular, if $g,h:C\to D$ are two functions into a set $D$ the proposition $\prod_{c:C}(g(c)=h(c))$ is equivalent to $\prod_{b:B}(gf(b)=hf(c))$. - -From this we condense the following characterizations of injections and surjections of sets which will prove to generalize nicely to other contexts. -% In other words, an injection between sets is a function $f:B\to C$ such that for any set $A$ and functions $g,h:A\to B$ such that $fg=fh:A\to C$ -% $$\xymatrix{A\ar[r]^f&B\ar@<1ex>[r]^g\ar@<-1ex>[r]_h&C}$$ -% we necessarily have that $g=h$. -\begin{lemma} - \label{lem:injofsetsaremono}Let $f:B\to C$ be a function between sets. - \begin{enumerate} - \item the function is an injection of and only if for any set $A$ and functions $g,h:A\to B$, -$$\xymatrix{A\ar@<1ex>[r]^g\ar@<-1ex>[r]_h&B\ar[r]^f&C},$$ then $fg=fh:A\to C$ implies $g=h$ -\item the function is an injection of and only if for any set $D$ and functions $g,h:C\to D$, -$$\xymatrix{B\ar[r]^f&C\ar@<1ex>[r]^g\ar@<-1ex>[r]_h&D},$$ then $gf=hf:A\to C$ implies $g=h$. - \end{enumerate} -\end{lemma} - - -By \cref{lem:injofsetsaremono} there is a pleasing reformulation which highlights that injections/surjections of sets are characterized by injections of sets of functions: a function of sets $f:B\to C$ is -\begin{enumerate} -\item an injection if and only if for any set $A$ postcomposition by $f$ given an injection from $A\to B$ to $A\to C$ -\item a surjection if and only if for any set $D$ precomposition by $f$ gives an injection from $B\to D$ to $B\to D$. -\end{enumerate} - -This observation about sets translates fruitfully to other contexts and in particular to groups. To make it clear that we talk about group homomorphisms (and not about the underlying unpointed functions of connected groupoids) we resort to standard categorical notation. -\begin{definition}\label{def:monomorphism} -Given groups $G,H$, a homomorphism $f: \Hom(G,H)$ is called a\label{def:epimorphism} -\begin{enumerate} -\item \emph{monomorphism}\index{monomorphism!of groups} if for any group $F$, - postcomposition by $f$ is an injection from $\Hom(F,G)$ to $\Hom(F,H)$, and an -\item \emph{epimorphism}\index{epimorphism!of groups} if for any group $I$, - precomposition by $f$ is an injection from $\Hom(H,I)$ to $\Hom(G,I)$. -\end{enumerate} -The corresponding families of propositions are called -\[ - \ismono,\isepi:\Hom(G,H)\to\Prop.\qedhere -\] -\end{definition} - -\marginnote{$$\xymatrix{\USymG\ar[d]^\simeq\ar[r]^{\US f}&\USymH\ar[d]^\simeq\\ - \Hom(\ZZ,G)\ar[r]^{f_*}\ar[d]^\simeq_\abstr&\Hom(\ZZ,H)\ar[d]^\simeq_\abstr\\ - \Hom^{\abstr}(\ZZ,\abstr(G))\ar[r]^{\abstr f_*}&\Hom^{\abstr}(\ZZ,\abstr(H)) - }$$ -commutes (we've written $\ZZ$ also for $\abstr(\ZZ$) since otherwise it wouldn't fit.} -We've seen that for any group $G$, the underlying set $\USymG\defequi(\shape_G=\shape_G)$ of $\abstr(G)$ is equivalent to the set of homomorphisms $\Hom(\ZZ,G)$ which in turn is equivalent to the set of abstract homomorphisms $\Hom^{\abstr}(\abstr(\ZZ),\abstr(G))$ and that abstraction preserves composition. -Hence, if $f:\Hom(G,H)$ is a group homomorphism, then saying that -$\US f$ is an injection is equivalent to saying that postcomposition by $f$ is an injection $\Hom(\ZZ,G)\to\Hom(\ZZ,H)$. -In this observation, the integers $\ZZ$ plays no more of a r\^ole than $\bn 1$ does in \cref{lem:injofsetsaremono}; we can let the source vary over any group $F$: - - -\begin{lemma}\label{lem:eq-mono-cover} -Let $G$ and $H$ be groups and $f: \Hom(G,H)$ a homomorphism. -The following propositions are equivalent:\label{lem:eq-epi-conn} -\begin{enumerate} -\item\label{it:mono} $f$ is a monomorphism; -\item\label{it:injection} $\US f:\USymG\to\USymH$ is an injection; -\item\label{it:cover} $\Bf_\div:\BG_\div\to \BH_\div$ is a \covering. -\end{enumerate} -\end{lemma} - -\begin{proof} - We have already seen that condition~\ref{it:mono} implies condition~\ref{it:injection} (let $F$ be $\ZZ$). - Conversely, suppose that \ref{it:injection} holds and $F$ is a group. Consider the commutative diagram -$$\xymatrix{\Hom(F,G)\ar[r]\ar[d]&\Hom(F,H)\ar[d]\\ - (\Hom(\ZZ,F)\to\Hom(\ZZ,G))\ar[r]&(\Hom(\ZZ,F)\to\Hom(\ZZ,H)),}$$ -where the vertical maps are the injections from the sets of (abstract) homomorphism to the sets of functions of underlying sets and the horizontal maps are postcomposition with $f$. Since the bottom function is by assumption is an injection, so is the upper one. -\footnote{ Alternatively: and $g,h:\Hom(F,G)$. Then $fg=fh$ implies that for all $p:\Hom(\ZZ,F)$ we have by associativity that $f(gp)=(fg)p=(fh)p=f(hp)$, and so, by assumption, that $gp=hp$. - Again, by function extensionality (of functions $\Hom(\ZZ,F)\to\Hom(\ZZ,G)$), this is exactly saying that $\US g$ is identical to $\US h$.} - - The equivalence of \ref{it:cover} and \ref{it:injection} follows -immediately from \cref{cor:fib-vs-path}\ref{set-fib-vs-path}, using -that $\BG$ is connected and $f$ is pointed and the equivalence between $\Hom(G,H)$ and $\BG\ptdto \BH$. -\end{proof} - -Similarly, we have: -\begin{lemma}\label{lem:epi-surj} - The following propositions are equivalent: -\begin{enumerate}[label=(\arabic*')] -\item\label{it:epi} $f$ is an epimorphism; -\item\label{it:surjection} $\US f:\USymG\to\USymH$ is a surjection. -\item\label{it:connfib} $\Bf_\div:\BG_\div\to \BH_\div$ has connected fibers. -\end{enumerate} -\end{lemma} - -\begin{proof} - The equivalence of \ref{it:surjection} and \ref{it:connfib} is immediate. - - For the rest, the easy direction is that \ref{it:surjection} implies \ref{it:epi}: - (TODO) - - The harder direction, that \ref{it:epi} implies \ref{it:surjection}, - is a corollary of the following lemma, which states that monos are equalizers. - Indeed, we can factor any $f : \Hom(G,H)$ via the image as a surjection followed - by a mono: - \[ - \begin{tikzcd}[cramped] - G \ar[r,"q"] & \im(f) \ar[r,"i"] & H - \end{tikzcd} - \] - If $f$ is an epi, then so is $i$. But $i$ is an equalizer, - \[ - \begin{tikzcd}[cramped] - \im(f) \ar[r,"i"] & H\ar[r,shift left,"\varphi"] - \ar[r,shift right,"\psi"'] & L, - \end{tikzcd} - \] - so as an epi, $\varphi i = \psi i$ implies $\varphi = \psi$, so $i$ - is an equalizer of already equal homomorphisms, so $i$ is an isomorphism, - which implies that $f$ is surjective. -\end{proof} - -\begin{lemma}\label{lem:monos-are-equalizers} - Every monomorphism $i : H \to G$ is an equalizer.\footnote{% - This proof follows an idea by \citeauthor{TrimbleEpisSurjective}\footnotemark{}.}% - \footcitetext{TrimbleEpisSurjective} -\end{lemma} -\begin{proof}[Proof draft.] Consider the projection $\pi : G \to G/H$ to the set of cosets. - Let $j : G/H \to A$ be an injection into a group $A$. - (We could for instance let $A$ be the free (abelian) group on $G/H$. [Add xref to statement that inclusion of generators in an injection.]) - - Consider the group $W \defeq \Aut_E(\sh_G,\cst{\sh_A})$, where - \[ - E \defeq \sum_{t : \BG}\bigl((\sh_G \eqto t) \to \BA\bigr). - \] - We have two homomorphisms $\varphi,\psi : G \to W$ with the same underlying map, - $t \mapsto (t , \cst{\sh_A})$, but with different pointing paths: - \[ - \varphi_\pt \defeq \refl{\sh_G,\cst{\sh_A}}, \quad - \psi_\pt \defeq (\refl{\sh_G}, j\pi). - \] - The equalizer of $\varphi$ and $\psi$ thus consists of all $g:\USymG$ - such that $j\pi(gg') = j\pi(g')$ for all $g':\USymG$. Since $j$ is injective, - this is equivalent to $\pi(gg')=\pi(g')$ for all $g':\USymG$, and this holds - if and only if $g$ belongs to $H$. -\end{proof} - -\subsection{Any symmetry is a symmetry in $\Set$} -\label{sec:groupssubperm} - - -The correspondence between groups and abstract groups allows for a cute proof of what is often stated as ``any group is a permutation group'', which in our parlance translates to ``any symmetry is a symmetry in $\Set$''. -% \footnote{which reminds me of the following: my lecturer in cosmology once tried to publish a paper about rotating black holes, only to have it rejected because it turned out that it was his universe, not the black hole, that was rotating} - -Recall the principal $G$-torsor $\princ G:\BG\to\Set$. -Since $\princ G(\shape_G)\defequi \USymG$ this defines a pointed function $\rho_G:\BG\to_* \BSigma_{\USymG}\defequi(\conncomp \Set {\USymG},\USymG)$, -\marginnote{the letter $\rho$ commemorates the word ``regular''} \ie a homomorphism from $G$ to the permutation group -$$\rho_G:\Hom(G,\Sigma_{\USymG}).$$ -\begin{theorem}[Cayley] - \label{lem:allgpsarepermutationgps} - \marginnote{By \cref{lem:eq-mono-cover} ``$\rho_G$ is a monomorphism'' means that the induced map $\rho_G^\abstr$ from the symmetries of $\shape_G$ in $\BG_\div$ to the symmetries of $\USymG$ in $\Set$ is an injection, \ie ``any symmetry is a symmetry in $\Set$''.}Let $G$ be a group. Then - $\rho_G:\Hom(G,\Sigma_{\USymG}) $ is a monomorphism. -\end{theorem} -\begin{proof} - In view of \cref{lem:eq-mono-cover} we need to show that $\rho_G:\BG\to \conncomp \Set {\USymG}$ is a - \covering. - Under the identity - $$\bar{\pathsp{}}:\BG=(\typetorsor_G,\princ G)\oldequiv (\conncomp{\Set}{\USymG},\USymG)$$ of - \cref{lem:BGbytorsor}, $\rho_G$ translates to the - evaluation map - $$\mathrm{ev}_{\shape_G}:\conncomp{(\BG\to\Set)}{\princ G}\to\conncomp{\Set}{\USymG},\qquad - \mathrm{ev}_{\shape_G}(E)=E(\shape_G).$$ - We must show that the preimages - $\inv{\ev_{\shape_G}}(X)$ for $X:\Sigma_{\USymG}$ are sets. This - fiber is equivalent to - $\sum_{E:\conncomp{(\BG\to\Set)}{\princ G}}(X=E(\shape_G))$ which is a - set precisely when $\sum_{E:\BG\to\Set}(X=E(\shape_G))$ is a set. We - must then show that if $(E,p),(F,q):\sum_{E:\BG\to\Set}(X=E(\shape_G))$, - then the type $(E,p)=(F,q)$, which is equivalent - \marginnote{Note that if $r:\shape_G=x$, then - $\phi(x)=F(r)qp^{-1}E(r)^{-1}$, in a picture - \begin{displaymath} - \xymatrix{&E(pt_G)\ar@{=}[r]^{E(r)}_\to\ar@{=}[dd]_{\phi(pt_G)}^\downarrow&E(x)\ar@{=}[dd]_{\phi(x)}^\downarrow\\ - X\ar@{=}[ur]^p_{\rotatebox{35}{\footnotesize$\to$}}\ar@{=}[dr]^q_{\rotatebox{-35}{\footnotesize$\to$}}&&\\ - &F(\shape_G)\ar@{=}[r]^{F(r)}_\to&F(x)}, - \end{displaymath} -and so $\phi(x)$ (which by nature is independent of such an -$r:\shape_G=x$) is uniquely determined by $(E,p)$ and $(F,q)$. The text says this formally.} -to - $$\prod_{x:\BG}\sum_{\phi(x):E(x)=F(x)}\phi(\shape_G)=qp^{-1},$$ - is a proposition. -If $\phi,\psi:((E,p)=(F,q))$, we - must show that $\phi=\psi$ and since that for $x:\BG$ both $E(x)$ and - $F(x)$ are sets, it is enough to show that the proposition - $\phi(x)=\psi(x)$ is not empty. Let - $f:(\shape_G=x)\to(\phi(x)=\psi(x))$ be given by letting $f(r)$ be the - composite of the identities $\phi(x)=F(r)qp^{-1}E(r)^{-1}=\psi(x)$ - given above. Since $\BG$ is connected, and $\phi(x)=\psi(x)$ is a - proposition, one can consider that $\shape_G=x$ is not empty, and we - are done. -\end{proof} - - -\section{Abelian groups} -\label{sec:abelian-groups} - -%% Remove/modify once the rest of the section is being refactored with -%% new notation/style for identity types. -Recall that given a pointed type $X$, we coerce it silently to its -underlying unpointed type $X_\div$ whenever this coercion can be -inferred from context. For example, given a group $G$, the type -$\BG\weq \BG$ can not possibly mean anything but -$\BG_\div\simeq \BG_\div$ as the operator ``$\weq$'' acts on bare -types. To refer to the type of pointed equivalences (that is the -pointed functions whose underlying functions are equivalences), we -shall use the notation $\BG \ptdweto \BG$.% - -\subsection{Center of a group} -\label{sec:center-group} - -\begin{definition} - Let $G$ be a group. The {\em center} of $G$, denoted - $\grpcenter(G)$, is the group - $\Aut_{(\BG_\div\eqto\BG_\div)}(\refl{\BG_\div})$.% - \marginnote{% - We work transparently through the equivalence - \begin{displaymath} - (\BG_\div=\BG_\div) \weq (\BG \weq \BG) - \end{displaymath} - so that $\id_{\BG_\div}$ is freely used in place of - $\refl {\BG_\div}$ when convenient.% - }% -\end{definition} - -There is a natural map -$\ev_{\shape_G} : (\BG_\div\eqto\BG_\div) \to \BG_\div$ defined by -$\ev_{\shape_G}(\varphi)\defequi \varphi(\shape_G)$, where the path -$\varphi$ is coerced to a function through univalence. In particular, -$\ev_{\shape_G}(\refl{\BG_\div}) \jdeq \shape_G$. It makes the -restriction of this map to the connected component of -$\refl{\BG_\div}$ a pointed map. In other words, it defines a group -homomorphism -\begin{displaymath} - \grpcenterinc G : \Hom(\grpcenter(G), G). -\end{displaymath} -such that $\B \grpcenterinc G \defequi \ev_{\shape_G}$. We will now -justify the name {\em center} for $\grpcenter(G)$, and connect it to -the notion of center for abstract groups in ordinary mathematics. The -homomorphism $\grpcenterinc G$ induces a homomorphism of abstract -groups from $\abstr(\grpcenter(G))$ to $\abstr(G)$. By induction on -$p:\refl{\BG_\div} \eqto \varphi$ for -$\varphi:\BG_\div \eqto \BG_\div$, one proves that -$\ap{\B \grpcenterinc G}(p) = p(\shape_G)$: indeed, this is true when -$p\jdeq \refl {\refl{\BG_\div}}$. One proves furthermore, again by -induction on $p:\refl{\BG_\div} \eqto \varphi$, that -$\ap \varphi = (q\mapsto \inv{p(\shape_G)} q p(\shape_G))$. In -particular, when $\varphi \jdeq \refl{\BG_\div}$, it shows that for -every $p:\refl{\BG_\div}\eqto\refl{\BG_\div}$, the following proposition -holds: -\begin{displaymath} - \prod_{g:\USymG }p(\shape_G) g = g p(\shape_G) -\end{displaymath} -In other words, $\abstr{(\grpcenterinc G)}$ maps elements of -$\abstr(Z(G))$ to elements of $\abstr(G)$ that commute with every -other elements. (The set of these elements is usually called the -center of the group $\abstr(G)$ in ordinary group theory.) - -\begin{lemma} - \label{lemma:center-is-subgroup}% - The map $\B \grpcenterinc G$ is a \covering over $\BG$. -\end{lemma} -\begin{proof} - One wants to prove the proposition - $\isset(\inv{(\B\grpcenterinc G)}(x))$ for each $x:\BG$. By - connectedness of $\BG$, it reduces to showing the proposition only - at $x\jdeq \shape_G$. However, - \begin{displaymath} - \inv{(\B\grpcenterinc G)}(\shape_G) \defequi \sum_{\varphi:{\B\grpcenter(G)}}{\shape_G \eqto \varphi(\shape_G)} - \end{displaymath} - Recall that $\B\grpcenter(G)$ is the connected component of - $\refl{\BG_\div}$ in $\BG_\div \eqto \BG_\div$. In particular, if - $(\varphi,p)$ and $(\psi,q)$ are two elements of the type on the - right hand-side above, % their identity type - % $(\varphi,p)\eqto(\psi,q)$ is equivalent to their identity type in - % $\BG_\div \eqto \BG_\div$, or in other words - the characterization of identity types in sum types gives an - equivalence: - \begin{displaymath} - ((\varphi,p) \eqto (\psi,q)) \equivto \sum_{\pi:\varphi\eqto\psi}\pi(\shape_G) p = q. - \end{displaymath} - We shall prove that the type on the right is a proposition, and it goes as - follows: - \begin{enumerate} - \item for $\pi:\varphi\eqto\psi$, the type $\pi(\shape_G) p = q$ is a - proposition; hence $\sum_{\pi:\varphi\eqto\psi}\pi(\shape_G) p = q$ is a - subset of the set $\varphi \eqto \psi$, so for elements $(\pi,!)$ and - $(\pi',!)$ of the subset, we have to prove $\pi=\pi'$, - % \item for all $x:\BG$, $\varphi(x)=\psi(x)$ is a set, hence for - % $\pi,\pi':\varphi=\psi$, the type $\pi=\pi'$ is a proposition, - \item because $\pi=\pi'$ is a proposition, by connectedness of $\BG$, it is - enough to prove $\pi(\shape_G)=\pi'(\shape_G)$, - \item finally the propositional condition on $\pi$ and $\pi'$ allows us to - conclude that $\pi(\shape_G)= q\inv p = \pi'(\shape_G)$. - \end{enumerate} -\end{proof} - -\begin{corollary} - \label{lemma:center-inc-inj-on-paths}% - The induced map - $\abstr {(\grpcenterinc G)}: \abstr(\grpcenter(G)) \to \abstr(G)$ is - injective. -\end{corollary} - -The following result explains how every element of the ``abstract -center'' of $G$ is picked out by $\abstr{(\grpcenterinc G)}$. -\begin{lemma} - \label{lemma:center-inc-surj-on-paths}% - Let $g:\USymG$ and suppose that $gh=hg$ for every - $h:\USymG$. The fiber $\inv{(\ap {\B\grpcenterinc G})}(g)$ contains - an element. -\end{lemma} -\begin{proof} - One must construct an element $\hat g:\refl{\BG_\div} = \refl{\BG_\div}$ such - that $g=\hat g(\shape_G)$. We shall use function extensionality and produce an - element $\hat g(x):x\eqto x$ for all $x:\BG$ instead. Note that $x\eqto x$ is - a set, and that connectedness of $\BG$ is not directly applicable here. We - will use a technique that has already proven useful in many situations in the - book, along the lines of the following sketch: - \begin{enumerate} - \item for a given $x:\BG$, if such a $\hat g(x):x\eqto x$ existed, it would - produce an element of the type $T(\hat g(x))$ for a carefully chosen type - family $T$, - \item aim to prove $\iscontr(\sum_{u:x\eqto x}T(u))$ for any $x:\BG$, - \item this is a proposition, so connectedness of $\BG$ can be applied - and only $\iscontr(\sum_{u:\USymG}T(u))$ needs to be proven, - \item hopefully, $\sum_{u:\USymG}T(u)$ reduces to an obvious - singleton type. - \end{enumerate} - Here, for any $x:\BG$, we define the type family $T: (x\eqto x) \to \UU$ - by - \begin{displaymath} - T(q) \defequi \prod_{p:\shape_G\eqto x} (pg=qp). - \end{displaymath} - And we claim that $\sum_{q:x\eqto x}T(q)$ is contractible for any - $x:\BG$. Because this is a proposition, one only need to check that it holds - on one point of the connected type $\BG$, say $x\jdeq \shape_G$. We consider - the following composition of equivalences: - \begin{displaymath}% - \begin{aligned} - \sum_{q:\USymG}T(q) &\jdeq - \sum_{q:\USymG}\prod_{p:\USymG}(pg=qp) - \\ - &\equivto \sum_{q:\USymG}\prod_{p:\USymG}(g=q) - \\ - &\equivto \sum_{q:\USymG}\USymG\to (g=q) - \\ - &\equivto \sum_{q:\USymG}\Trunc{\USymG}\to (g=q) - \\ - &\equivto \sum_{q:\USymG} (g=q) - \\ - &\equivto 1 - \end{aligned} - \end{displaymath}% - % \marginnote[-10\baselineskip]{% - In that composition, the first equivalence is using that $g$ commutes with - every other element $p:\USymG$, so that $pg \inv p = g$. The second - equivalence acknowledges the fact that the codomain $(g=q)$ does not depend on - $p$ anymore, so that the dependent function type inside the sum is a simple - function type. The third equivalence uses the universal property of - propositional truncation under the sum. The fourth equivalence is the - evaluation at $\trunc{\refl {\shape_G}}$ under the sum. The last equivalence - is the contractibility of singleton types.% - % }% - - We have just shown that for all $x:\BG$, the type $\sum_{q:x\eqto x}T(q)$ is - contractible. We define now $\hat g(x):x\eqto x$ as the chosen center of - contraction of that type. More precisely, by connectedness of $\BG$, the - inverse $\inv\varphi$ of the exhibited equivalence - $\varphi:\sum_{q:\USymG}T(q) \equivto 1$ produces a dependent function of - type $\prod_{x:\BG}1\equivto \sum_{q: x\eqto x}T(q)$, and $\hat g$ is the - pointwise evaluation at the unique element $\triv$ of $1$. In particular, - $\hat g (\shape_G) = \inv\varphi (\triv) = g$ as wanted. -\end{proof} - -Together, \cref{lemma:center-inc-inj-on-paths} and -\cref{lemma:center-inc-surj-on-paths} show that -$\abstr{(\grpcenterinc G)}$ establishes an equivalence -\begin{equation} - %\left( \id_{\BG_\div} = \id_{\BG_\div} \right) - \USym \grpcenter(G) \equivto \sum_{g:\USymG}\prod_{h:\USymG}gh=hg -\end{equation} -In yet other words, -$\B \grpcenter(G)\defequi \conncomp{(\BG_\div \eqto \BG_\div)} -{\refl{\BG_\div}}$ is (equivalent to) the classifying type of a -group whose abstract group is the ``abstract center'' of $\abstr(G)$. - -The following lemma is then immediate: -\begin{lemma} - \label{def:abelian-groups}% - A group $G$ is {\em abelian} if and only if $\grpcenterinc G$ is an - isomorphism of groups. -\end{lemma} - -%% TRANSFORM AS REMARK ON ALTERNATIVE DEF: -%% -% Directly from the definition and the computations above, one see that -% a group $G$ is abelian if and only if it satisfies the following -% property: -% \begin{displaymath} -% \prod_{g,h:\USymG}gh=hg -% \end{displaymath} -% which is the ordinary definition of an abstract abelian group in -% ordinary group theory. -\begin{remark} - In the style of this book, we could have - used~\cref{def:abelian-groups} directly as the definition of abelian - groups. However, the definition of $\grpcenterinc G$ would have been - too intricate to give properly as early as~\cref{def:abgp}. -\end{remark} - -\subsection{Universal cover and simple connectedness} -\label{sec:univ-cover-simple} -%% TO BE MOVED? - -%% CHANGE THAT: -% \begin{itemize} -% \item for any pointed type $X$, the pointed type $\loopspace X$ is -% defined as $(\pt_X = \pt_X)$ with designated point $\refl {\pt_X}$, -% \item the {\em abstract fundamental group} $\fundgrp(X)$ of a pointed type -% $X$ is the set truncation $\setTrunc{\loopspace X}$, -% \item equivalently, in presence of groupoid truncations -% $\grpdTrunc{\blank}$, the {\em (concrete) fundamental group} -% $\fundgrpd(X)$ of a pointed type $X$ is the pointed type -% $\conncomp{\left(\grpdTrunc X\right)}{\grpdtrunc{\pt_X}}$, -% \item a simply connected type is a connected pointed type $X$ such -% that $\pi_1(X)$ (equivalently $\fundgrpd(X)$) is contractible. -% \end{itemize} -%% -Let us say that a pointed type $(A,a)$ is {\em simply connected} when -both $A$ and $a\eqto a$ are connected types. - -\begin{definition} - \marginnote{% - The definition of the universal cover is reminiscent of the notion of - connected component: instead of selecting elements that are merely equal to - a fixed element $a$, the universal cover selects elements together with mere - witnesses of the equality with $a$.% - }% - Let $A$ be a type and $a:A$ an element. The {\em universal cover} of $A$ at - $a$ is the type - \begin{displaymath} - \univcover A a \defequi \sum_{x:A}\setTrunc{a\eqto x}. - \end{displaymath} -\end{definition} -When needed, we will consider $\univcover A a$ as a pointed type, with -distinguished point $(a,\settrunc{\refl a})$. Note that when $A$ is a -groupoid, then the set truncation is redundant and the universal cover -of $A$ at $a$ is then the singleton at $a$. In particular, groupoids -have contractible universal covers. - -The identity types in $\univcover A a$ can be understood easily once -we introduce the following function for elements $x,y,z:A$: -\begin{displaymath} - \blank\cdot\blank : \setTrunc{y\eqto z} \times \setTrunc{x\eqto y} \to \setTrunc{x\eqto z}. -\end{displaymath} -It is defined as follows: given $\chi : \setTrunc{y\eqto z}$, we want to define -$\chi\cdot\blank$ in the set $\setTrunc{x\eqto y} \to \setTrunc{x\eqto z}$, -hence we can suppose $\chi\jdeq\settrunc q$ for some $q:y\eqto z$; now given -$\pi:\setTrunc{x\eqto y}$, one want to define $\settrunc q \cdot \pi$ in the set -$\setTrunc{x\eqto z}$, hence one can suppose $\pi\jdeq\settrunc p$ for some -$p:x\eqto y$; finally, we define -\begin{displaymath} - \settrunc{q} \cdot \settrunc{p} \defequi \settrunc{q\cdot p}. -\end{displaymath} -Then one proves, by induction on $p:x\eqto y$, that -$\trp[\setTrunc{a\eqto\blank}]p$ is equal to the function -$\alpha\mapsto \settrunc{p}\cdot \alpha$. In particular, there exists an -equivalence from the type of path between two points $(x,\alpha)$ and -$(y,\beta)$ of the universal cover $\univcover A a$ to sum type, analagous to -the identification of paths in sum types: -\begin{equation} - \label{eq:id-types-universal-cover}% - \left((x,\alpha) \eqto (y,\beta)\right) - \equivto \sum_{p:x\eqto y}\settrunc{p} \cdot \alpha = \beta. -\end{equation} - -This description allows us to prove the following lemma. -\begin{lemma} - \label{lemma:universal-cover-simply-connected}% - Let $A$ be a type and $a:A$ an element. The universal cover - $\univcover A a$ is simply connected. -\end{lemma} -\begin{proof} - First, we prove that $\univcover A a$ is connected. It has a point - $(a,\settrunc{\refl a})$ and, for every $(x,\alpha):\univcover A a$, one wants - $\Trunc{(a,\settrunc{\refl a}) \eqto (x,\alpha)}$. This is proposition, hence - a set, so that one can suppose $\alpha \jdeq \settrunc p$ for a path - $p:a\eqto x$. Now, the proposition - $\settrunc p \cdot \settrunc {\refl a} = \settrunc p$ holds. So one can use - the inverse of the equivalence of~\cref{eq:id-types-universal-cover} to - produce a path $(a,\settrunc{\refl a}) \to (x,\alpha)$. - - Next, we prove that $(a,\settrunc{\refl a}) \eqto (a,\settrunc{\refl a})$ is - connected. One uses again the equivalence - of~\cref{eq:id-types-universal-cover} to produce a composition of - equivalences: - \begin{align*} - \left((a,\settrunc{\refl a}) \eqto (a,\settrunc{\refl a})\right) - &\equivto \sum_{p:a=a}\left( \settrunc p = \settrunc{\refl a} \right) - \\ - &\equivto \sum_{p:a=a}\left( \Trunc {p \eqto \refl a} \right) - \end{align*} - In other words, $(a,\settrunc{\refl a}) \eqto (a,\settrunc{\refl a})$ is - equivalent to the connected component of $\refl a$ in $a\eqto a$. In - particular, it is connected. -\end{proof} - -\begin{lemma} - \label{lemma:universal-cover-is-universal} - Let $A$ be a type pointed at $a:A$. The projection $\fst : \univcover A a \ptdto A$ is a universal \covering{} in the sense of~\cref{def:univ-cover}. -\end{lemma} -\begin{proof} - Let $f : B \ptdto A$ be a pointed \covering{}. We need to show that the type of pointed functions $\varphi : \univcover A a \ptdto B$ together - with an identification $q : \fst \eqto f \varphi$ is contractible. However, such a $\varphi$ is uniquely determined by the family of functions - $\varphi_x : \setTrunc{ a \eqto x } \to \inv f (x)$ for $x : A$. For each $x : A$, $\inv f (x)$ is a set, so $\varphi_x$ is uniquely - determined by $\varphi_x \circ \settrunc\blank : a \eqto x \to \inv f (x)$. By induction on $p : a \eqto x$, we prove that - $\varphi_x (\settrunc p) = \trp [\inv f] p (b , f_0) $ where $b$ is the element pointing $B$ and $f_0$ the path pointing $f$. Indeed, for - $p \jdeq \refl a$, we get $\varphi_a (\settrunc {\refl a}) \jdeq (\varphi (\settrunc {\refl a}) , q_{\settrunc {\refl a}}) = (b , f_0)$ - because $q$ is an indentification $\fst \eqto f \varphi$ of pointed functions. -\end{proof} - -\subsection{Abelian groups and simply connected $2$-types} -\label{sec:abel-groups-simply} - -We will now give an alternative characterization of the type of -abelian groups, more in line with the geometrical intuition we are -trying to build in this chapter. Recall that a type $A$ is called a -{\em $2$-truncated type}, or {\em $2$-type} for short, when the -identity type $x\eqto y$ is a groupoid for every $x,y:A$. - -%% OLD -%% -% We also settle some notations that should ease the reading of the -% proof of the next result. For any type $A:\UU$, we define -% \begin{displaymath} -% \univcover \UU A \defequi \sum_{X:\UU}\setTrunc{A=X}. -% \end{displaymath} -% This is the analog of the connected component of $\UU$ at $A$ but with -% a set truncation involved. In particular, $\univcover \UU A$ is {\em -% not} a subtype of $\UU$. To understand identity types better in this -% type $\univcover \UU A$, let us introduce the following function for -% any types $X,Y,Z:\UU$: -% \begin{displaymath} -% \blank\cdot\blank : \setTrunc{Y=Z} \times \setTrunc{X=Y} \to \setTrunc{X=Z}. -% \end{displaymath} -% It is defined as follows: given $a: \setTrunc{Y=Z}$, we want to define -% $a\cdot\blank$ in the set $\setTrunc{X=Y} \to \setTrunc{X=Z}$, hence -% we can suppose $a\jdeq\settrunc p$ for some $p:Y=Z$; now given -% $b:\setTrunc{X=Y}$, one want to define $\settrunc p \cdot b$ in the -% set $\setTrunc{X=Z}$, hence one can suppose $b\jdeq\settrunc q$ for some -% $q:X=Y$; finally, we define -% \begin{displaymath} -% \settrunc{q} \cdot \settrunc{p} \defequi \settrunc{q\cdot p}. -% \end{displaymath} -% Then one proves, by induction on $\varphi:X=Y$, that -% $\trp[\setTrunc{A=\blank}]\varphi$ is equal to the function -% $a\mapsto \settrunc{\varphi}\cdot a$. In particular, one gets an -% equivalence between the type $(X,a) = (Y,b)$ of identities between -% elements $(X,a), (Y,b): \univcover\UU A$ and the type -% $\sum_{\varphi:X=Y}\settrunc{\varphi} \cdot a = b$. - -% From this, we deduce two important properties of $\univcover\UU A$: -% \begin{itemize} -% \item The type $\univcover\UU A$ is connected. Indeed, for any -% $(X,a):\univcover \UU A$, one wants to prove the proposition -% $\Trunc{(A,\refl A) = (X,a)}$. A proposition being in particular a -% set, one can suppose that $a\jdeq \settrunc p$ for some -% $p:A=X$. Then -% \begin{displaymath} -% !:\settrunc p \cdot \settrunc{\refl A} = \settrunc{p}, -% \end{displaymath} -% and the pair $(p,!)$ is an element of $(A,\refl A) = (X,a)$ whose -% propositional truncation allows us to conclude. -% \item Consider $\univcover \UU A$ as pointed at -% $(A,\settrunc{\refl A})$. Then $\univcover\UU A$ is simply -% connected. Indeed, one has an equivalence: -% \begin{displaymath} -% \loopspace {\univcover\UU A} -% \weq \sum_{\varphi:A=A}\left( \settrunc{\varphi} = \settrunc{\refl A}\right) -% \weq \sum_{\varphi:A=A}\Trunc{\varphi = \refl A} -% \end{displaymath} -% which proves that $\loopspace {\univcover\UU A}$ is the connected -% component of $\refl A$ in $A=A$. -% \end{itemize} - -\begin{theorem}\label{thm:abelian-groups-weq-sc2types}% - The type $\typeabgroup$ of abelian groups is equivalent to the type - of pointed simply connected $2$-types. -\end{theorem} -\begin{proof} - Define the map $\BB : \typeabgroup \to \UUp$ by - $\BB G\defequi \univcover{\UU}{\BG_\div}$.\footnote{% - This is slightly misleading: If $G$ is an abelian group in - universe $\UU$, then this definition makes $\BB G$ a pointed type - in a successor universe, which is not what we want. The solution - is to note that $\BB G$ is a locally $\UU$-small type, which as a - connected type is the image of the base point map - $\pt : \bn{1} \to \BB G$, so it's an essentially $\UU$-small type - by the Replacement~\cref{pri:replacement}. So really, $\BB G$ - should be the $\UU$-small type equivalent to - $\univcover{\UU}{\BG_\div}$.} Proving that $\BB G$ is a $2$-type - is equivalent to proving the proposition $\isset(p\eqto q$) for all - $p,q:x\eqto y$ and all $x,y:\BB G$. One can then use connectedness - of $\BB G$ and restrict to only show that $p\eqto q$ is a set for - all path - $p,q:(\BG_\div,\settrunc{\id_{\BG_\div}})\eqto ({\B - G}_\div,\settrunc{\id_{\BG_\div}})$. Recall that there is a - canonical equivalence of type: - \begin{equation}\label{eq:} - \left( - (\BG_\div,\settrunc{\id_{\BG_\div}})\eqto (\BG_\div,\settrunc{\id_{\BG_\div}}) - \right) - \equivto - \sum_{r:\BG_\div \eqto \BG_\div}\trp r (\settrunc{\id_{\BG_\div}}) \eqto \settrunc{\id_{\BG_\div}} - \end{equation} - Under that equivalence, $p$ and $q$ can be rewritten as $(p_0,!)$ - and $(q_0,!)$ with $p_0,q_0 : \BG_\div\eqto \BG_\div$ and the - elements $!$ are proofs of the proposition - $\trp {p_0} {(\settrunc{\id_{\BG_\div}})} = - \settrunc{\id_{\BG_\div}}$ and - $\trp {q_0} {(\settrunc{\id_{\BG_\div}})} = - \settrunc{\id_{\BG_\div}}$ respectively. As a consequence, the - proposition $\isset(p\eqto q)$ is equivalent to the proposition - $\isset(p_0\eqto q_0)$. As part of the definition of the group $G$, - the type $\BG_\div$ is a $1$-type, hence $\BG_\div\eqto \BG_\div$ is - also a $1$-type through univalence. This means that - $\isset(p_0\eqto q_0)$ holds. - - So one gets a map, denoted again $\BB$ abusively, - \begin{displaymath} - \BB : \typeabgroup \to \UUsctwo - \end{displaymath} - where the codomain $\UUsctwo$ is the type of pointed simply - connected $2$-types, that is - \begin{displaymath} - \UUsctwo \defequi \sum_{(A,a):\UUp}\left( - \isconn(A) \times \isconn(a\eqto a) \times \isgrpd(a\eqto a) - \right) - \end{displaymath} - We shall now provide an inverse for this map. Given a pointed simply - connected $2$-type $(A,a)$, one can construct a group, denoted - $\loopspace (A,a)$, with classifying type: - \begin{displaymath} - \B\loopspace (A,a) \defequi (a\eqto a,\refl a). - \end{displaymath} - Indeed, this pointed type is connected because $(A,a)$ is simply - connected, and it is a $1$-type because $A$ is a $2$-type. Moreover, - $\loopspace (A,a)$ is abelian. To see it, let us use the bare - definition of abelian groups (cf.\ ~\cref{def:abgp}). We shall then - prove that for all elements $g,h:\refl a \eqto \refl a$, the - proposition $gh=hg$ holds. This property holds in even more - generality and is usually called ``Eckmann-Hilton's argument''. It - goes as follows: for $x,y,z:A$, for $p,q:x\eqto y$ and - $r,s:y \eqto z$ and for $g:p\eqto q$ and $h:r\eqto s$, one prove - \begin{equation} - \label{eq:horizontal-comp}% - \ap{\blank\cdot q}(h) \cdot \ap{r\cdot\blank}(g) - = \ap{s\cdot \blank}(g) \cdot \ap{\blank\cdot p}(h). - \end{equation} - This equality takes place in $r\cdot p \eqto s\cdot q$ and is better - represented by the diagram in~\cref{fig:horizontal-comp}. - \begin{figure}[h] - \begin{sidecaption} - {% - Visual representation of~\cref{eq:horizontal-comp}. The vertical - dotted lines denotes composition.% - }[fig:horizontal-comp] - \centering% - \begin{tikzpicture}[node distance=4em, baseline=(basenode.base)] - \node[] (x1) {$x$}; - \node[right of=x1] (y1) {$y$}; - \node[right of=y1] (z1) {$z$}; - \node[below of=x1] (x2) {$x$}; - \node[right of=x2] (y2) {$y$}; - \node[right of=y2] (z2) {$z$}; - \draw[bend left] (x1) to node[above] (p) {\footnotesize$p$} (y1); - \draw[bend right] (x1) to node[below] (q1) {\footnotesize$q$} (y1); - \draw[bend left] (y1) to node[above] (r1) {\footnotesize$r$} (z1); - \draw[bend left] (y2) to node[above] (r2) {\footnotesize$r$} (z2); - \draw[bend right] (y2) to node[below] (s) {\footnotesize$s$} (z2); - \draw[bend right] (x2) to node[below] (q2) {\footnotesize$q$} (y2); - \draw[double, shorten >=.1em, shorten <=.1em] (p) to node[right] {\footnotesize$g$} (q1); - \draw[double, shorten >=.1em, shorten <=.1em] (r2) to node[right] {\footnotesize$h$} (s); - \draw[gray,densely dotted] (x1) to node (basenode){} (x2) (y1) to (y2) (z1) to (z2); - \end{tikzpicture}% - =% - \begin{tikzpicture}[node distance=4em, baseline=(basenode.base)] - \node[] (x1) {$x$}; - \node[right of=x1] (y1) {$y$}; - \node[right of=y1] (z1) {$z$}; - \node[below of=x1] (x2) {$x$}; - \node[right of=x2] (y2) {$y$}; - \node[right of=y2] (z2) {$z$}; - \draw[bend left] (x2) to node[above] (p) {\footnotesize$p$} (y2); - \draw[bend right] (x2) to node[below] (q1) {\footnotesize$q$} (y2); - \draw[bend right] (y2) to node[above] (r1) {\footnotesize$s$} (z2); - \draw[bend left] (y1) to node[above] (r2) {\footnotesize$r$} (z1); - \draw[bend right] (y1) to node[below] (s) {\footnotesize$s$} (z1); - \draw[bend left] (x1) to node[above] (p2) {\footnotesize$p$} (y1); - \draw[double, shorten >=.1em, shorten <=.1em] (p) to node[right] {\footnotesize$g$} (q1); - \draw[double, shorten >=.1em, shorten <=.1em] (r2) to node[right] {\footnotesize$h$} (s); - \draw[gray,densely dotted] (x1) to node (basenode){} (x2) (y1) to (y2) (z1) to (z2); - \end{tikzpicture}% - \end{sidecaption} - \end{figure}% - % - One prove such a result by induction on $h$. Indeed, when - $h\jdeq \refl r$, then both sides of the equation reduces through - path algebra to $\ap {r\cdot\blank} (g)$. Now we are interested in - this result when $x,y,z$ are all equal to $a$ by definition, and $p,q,r,s$ - are all equal to $\refl a$ by definition. In that case, one has that - $\ap {\refl a\cdot \blank}$ and $\ap {\blank\cdot\refl a}$ both act - trivially, and the equation becomes: $h\cdot g = g \cdot h$. - - One still has to prove that the function $\loopspace$ is an inverse - for $\BB$. Given an abelian group $G$, the proof - of~\cref{lemma:universal-cover-simply-connected} gives an - equivalence between $\B\loopspace {(\BB G)}$ and the connected - component of $\refl {\BG_\div}$ in $\BG_\div\eqto \BG_\div$. By - definition, this is the classifying type of $\grpcenter(G)$. Being - abelian, $G$ is isomorphic to its center - (\cref{def:abelian-groups}), and so it yields an element of - $\loopspace {(\BB G)} \eqto_{\typegroup} G$. % - \marginnote[-1.5\baselineskip]{% - If $X \ptdweto Y$ denote the type of pointed equivalences between - pointed types $X,Y:\UUp$, then the univalence axiom implies that - there is an equivalence - \begin{displaymath} - (X=Y) \weq (X \ptdweto Y). - \end{displaymath}% - }% - Conversely, take a pointed simply connected $2$-type $(A,a)$. We - want to produce a pointed equivalence - $\Phi : (A,a) \equivto \BB (\loopspace {(A,a)}) $. One should first - notice that the function - \begin{fullwidth} - \begin{equation} - \label{eq:loopspace-A-abelian}% - \ev^a_{refl a}{\B\loopspace \left( \BB (\loopspace {(A,a)}) \right)} - \jdeq \conncomp{((a\eqto a)\eqto (a\eqto a))}{\refl{a\eqto a}} \to (a\eqto a,\refl a). - \end{equation} - \end{fullwidth} - that maps a path - \begin{displaymath} - (p,!):(a\eqto a,\settrunc{\refl{a\eqto a}})\eqto (a\eqto a,\settrunc{\refl{a\eqto a}}) - \end{displaymath} - to the evaluation $p(\refl a): a\eqto a$ is an equivalence, because - $\loopspace (A,a)$ is an abelian group. - - %% OLD MATERIAL, can still be useful. - %% - % We will now provide - % \begin{displaymath} - % \Phi : \BB {(\loopspace {(A,a)})} \ptdto (A,a) - % \end{displaymath} - % such that $\loopspace(\Phi)$ is the previous equivalence. - % To be able to - % express $\Phi$, we need a small gadget about truncations of - % function - % types: for types $X,Y:\UU$, given an element - % $f_0:\setTrunc{X\to Y}$, one constructs a map - % $\lceil f_0 \rceil : \setTrunc X \to \setTrunc Y$; the type of - % $\lceil f_0 \rceil$ being a set, one might as well suppose that - % $f_0 \jdeq \settrunc f$ for some $f:X\to Y$; then we set - % $\lceil f_0 \rceil (\settrunc x) = \settrunc{f(x)}$, which - % suffices - % in order to define $\lceil f_0 \rceil$ entirely because its - % codomain - % $\setTrunc Y$ is a set. If we assume the axiom of - % choice\footnote{What is the status of AC in this book??}, then - % $\lceil \blank \rceil$ is injective when $Y$ is a set. - %% - We will now define a pointed map - $\Phi : (A,a) \ptdto \BB (\loopspace {(A,a)})$, and prove - subsequently that this is an equivalence. Let $T : A \to \UU$ be the - type family (of sets) define by - \begin{displaymath} - T(a') \defequi \sum_{\alpha:\setTrunc{(a\eqto a)\weq(a\eqto a')}} - \prod_{p:a\eqto a'}\alpha=\settrunc {p\cdot\blank} - \end{displaymath} - We claim that $T(a')$ is contractible for all $a':A$. By - connectedness of $A$, it is equivalent to show that $T(a)$ is - contractible. However, - \begin{align*} - T(a) - &\jdeq \sum_{\alpha:\setTrunc{(a\eqto a)\equivto(a\eqto a)}}\prod_{p:a\eqto a} - \alpha = \settrunc {p\cdot \blank} - \\ - &\weq \sum_{\alpha:\setTrunc{(a\eqto a)\equivto(a\eqto a)}} \alpha = \settrunc{\id_{a=a}} - \\ - &\weq 1 - \end{align*} - Then, we define $\Phi (a')$ to be the element - $(a\eqto a', \kappa_{a'}):\univcover \UU {a\eqto a}$ where - $\kappa_{a'}$ is the first projection of the center of contraction - of $T(a')$. In particular, following the chain of equivalences - above, $\Phi(a)$ is defined as - $(a\eqto a, \settrunc{\refl {a\eqto a}})$, hence $\Phi(a)$ is - trivially pointed by a reflexivity path. To verify that $\Phi$, thus - defined, is an equivalence, one can use connectedness of - $\BB(\loopspace (A,a))$ and only check that - $\inv\Phi(a\eqto a,\settrunc{\refl {a\eqto a}})$ is - contractible. However, there is a canonical equivalence of type: - \begin{displaymath} - \inv\Phi(a\eqto a,\settrunc{\refl {a\eqto a}}) \equivto \sum_{a':A} - \sum_{\varphi : (a\eqto a) \equiv (a\eqto a')}\settrunc{\varphi} = \kappa_{a'}. - \end{displaymath} - So we will show that the type on the right hand-side is - contractible. For an element $a':A$ together with - $\varphi: (a\eqto a) \equiv (a\eqto a')$ such that the proposition - $\settrunc \varphi = \kappa_{a'}$ holds, a path between - $(a,\id_{a\eqto a},!)$ and $(a',\varphi,!)$ consists of a path - $p:a\eqto a'$ and a path $q:(x\mapsto p x) \eqto \varphi$. We have a - good candidate for $p$, namely $p\defequi \varphi(\refl - a):a\eqto a'$. However we don't have quite $q$ yet. Consider, for any - $a':A$, the function - \begin{displaymath} - \ev_{\refl a}^{a'} : - \left( - (a\eqto a, \settrunc{\refl{a\eqto a}} ) = - (a\eqto a', \kappa_{a'} ) - \right) - \to (a\eqto a') - \end{displaymath} - defined as $(\psi,!) \mapsto \psi(\refl a)$. Note that - $\ev_{\refl a}^{a}$ is precisely the equivalence - $\B\loopspace{(\BB\loopspace(A,a))}_\div \equiv (a=a)$ described - in~\cref{eq:loopspace-A-abelian}. Hence, by connectedness of $A$, - one gets that the proposition $\isEq(\ev_{\refl a}^{a'})$ holds for - all $a':A$. In particular, because the propositions - $\settrunc \varphi = \kappa_{a'}$ and - $\settrunc {p\cdot\blank} = \kappa_{a'}$ holds, one gets elements - $(\varphi,!)$ and $(x\mapsto px,!)$ in the domain of - $\ev_{\refl a}^{a'}$. Their images $\ev_{\refl a}^{a'}(\varphi,!)$ - and $\ev_{\refl a}^{a'}(x\mapsto px,!)$ are both identifiable with - $p$. By composition, we obtain a path - $(x\mapsto px,!)\eqto (\varphi,!)$ in the domain. The first - component provide the path $q:(x\mapsto px) \eqto \varphi$ that we - wanted. -\end{proof} - -\subsection{Higher deloopings} - -The function $\BB$ defined in the proof -of~\cref{thm:abelian-groups-weq-sc2types} provides a delooping of -$\BG$ whenever $G$ is abelian. That is, there is an identification -$\loops \BB G \eqto \BG$. A systematic way of obtaining such -deloopings has been developed by David W\"{a}rn\footcite{Warn-EM}, -that can be applied here to give an alternative definition of $\BB G$, -and to obtain further deloopings of it. - -\begin{definition}[W\"{a}rn] - Given a pointed type $X$, the type of {\em $X$-torsors} is - \begin{displaymath} - TX \defequi \sum_{Y : \UU} \Trunc{Y} \times \left( \prod_{y:Y}(Y,y) \ptdweto X \right). - \end{displaymath} - The type of {\em pointed $X$-torsors} is - $TX_\ast \defequi \sum_{t : TX}\fst t$. -\end{definition} -The usefulness of these definitions in the context of deloopings comes -from the following proposition. -\begin{lemma}[W\"{a}rn] - Let $X$ be a pointed type. If $TX_\ast$ is contractible, then for - any pointed $X$-torsors $(t,y)$, the pointed type $(TX,t)$ is a - delooping of $X$. -\end{lemma} -\begin{proof} - Suppose $(t,y)$ is a center of contraction for $TX_\ast$. By - contracting away (\cref{lem:contract-away}) in two different ways, - we obtained a composition of equivalences: - \begin{displaymath} - (t \eqto t) \equivto \sum_{u : TX}\fst u \times (t \eqto u) \equivto \fst t - \end{displaymath} - that maps $\refl t$ to $y$. In other words, this equivalence, - trivially pointed, presents $(TX, t)$ as a delooping of - $(\fst t, y)$. Moreover, the $X$-torsor $t$ comes by definition with - an identification $(\fst t,y) \ptdweto X$. So in the end, we have an - equivalence $(TX, t) \ptdweto X$. -\end{proof} - -\begin{exercise}\label{xca:sections-as-dependent-functions} - Recall that a {\em section} (see~\cref{def:surjection} and its - accompanying footnote) of a function $f:A \to B$ is a function - $s: B \to A$ together with an identification $f\circ s \eqto \id_B$. - Construct an equivalence from the type $\secfun f$ of sections of - $f$ to the type $\prod_{b:B}\sum_{a:A}b \eqto f(a)$. -\end{exercise} - -Consider the evaluation function -$\ev_{X_\div,Y} : (X_\div \eqto Y) \to Y$ (defined by path-induction, -sending $\refl X$ to the distinguished point of $X$). In other words, -the function $\ev_{X_\div,Y}$ takes an identification of $X_\div$ with -$Y$ and returns the point in $Y$ corresponding to the distinguished -point of $X$ under this identification. Applying -\cref{xca:sections-as-dependent-functions} to $\ev_{X_\div,Y}$ we get -an equivalence of type -\begin{displaymath} - TX \equivto \sum_{Y : \UU} \Trunc{Y} \times \secfun(\ev_{X_\div,Y}). -\end{displaymath} -This alternative description of the type of $X$-torsors is the key -ingredient to compare W\"arn's delooping of the classifying type of -an abelian group with our. - -\begin{lemma}\label{lem:warn-abelian-group} - For any abelian group $G$, the type $T(\BG)$ can be identified with - $\BB G$. -\end{lemma} -\begin{proof} - Let $G$ be an abelian group. We first construct, for each type - $Y$, a function - $f_Y : \Trunc{Y} \times \secfun(\ev_{\BG_\div,Y}) \to - \setTrunc{\BG_\div \eqto Y}$, and then prove that $f_Y$ is an - equivalence. Given a type $Y$ and an element - $(!,s) : \Trunc{Y} \times \secfun(\ev_{X_\div,Y})$, we can easily - prove that $Y$ is connected: being connected is a proposition, so - we can assume that we have an actual $y:Y$ and then - $s(y) : \BG_\div \eqto Y$ proves that $Y$ is as connected as - $\BG_\div$ is. Consequently $s$ must send $Y$ into one of the - connected component of $\BG_\div \eqto Y$, that we choose to be - $f_Y(!,s)$. With this definition, the fiber of $f_Y$ at any given - $c : \setTrunc{\BG_\div \eqto Y}$ can be identified with the type - of sections $s$ of $\ev_{\BG_\div,Y}$ with values in $c$. However, - for any $Z$ and $p: \BG_\div \eqto Z$ the restriction of the - evaluation - $\ev_{\BG_\div,Z}\restriction_p : \conncomp{(\BG_\div \eqto Z)} p - \to Z$ is an equivalence: indeed, by induction, we only have to - show it for $p\jdeq \refl {\BG_\div}$, in which case - $\ev_{\BG_\div,\BG_\div}\restriction_{\refl {\BG_\div}}$ is - exactly the map $\B\grpcenterinc G$ defined in - \cref{sec:center-group}, which is an equivalence since $G$ is - abelian by \cref{def:abelian-groups}. Thus, given any $p$, the - fiber of $f_Y$ at $\settrunc p$ is contractible. Being - contractible is a proposition, hence a set, so it follows that the - fiber of $f_Y$ at any $c:\setTrunc{\BG_\div \eqto Y}$ is - contractible. In other words, $f_Y$ is an equivalence, as - announced. We have thus a chain of equivalences:\footnote{Notice - that the construction of an equivalence - $TX \equivto \univcover \UU {X_\div}$ that we carried for - $X\jdeq\BG$ relies only on $X_\div$ being connected and - $\ev_{X_\div,X_\div}\restriction_{\refl {X_\div}}$ being an - equivalence. Such types $X$ are called \emph{central} and are - studied in details by~\citeauthor{BCFR}\footnotemark{}.}.% - \footcitetext{BCFR} - \begin{displaymath} - T(\BG) \equivto \sum_{Y : \UU} \Trunc{Y} \times \secfun(\ev_{X_\div,Y}) - \equivto \sum_{Y : \UU} \setTrunc{\BG_\div \eqto Y} \jdeq \BB G - \end{displaymath} -\end{proof} - -Notice that where W\"arn's method shines, compared to our, is in -producing further delooping $\B^n G$ for $n\geq 3$. - - -\section{$G$-sets vs $\abstr(G)$-sets} -\label{sec:Gsetsabstrconcr} -\marginnote{Recall from \cref{def:abstrGtorsors} that the type of $\abstr(G)$-set is - $$\Set_{\abstr(G)}^\abstr\defequi \sum_{\mathcal X:\Set}\Hom_\abstr({\abstr(G)},\abstr(\Sigma_{\mathcal X})).$$} - -Given a group $G$ it should by now come as no surprise that the type of $G$-sets is equivalent to the type of $\abstr(G)$-sets. -According to \cref{lem:homomabstrconcr} -$$\abstr:\Hom(G,\Sigma_{\mathcal X})\to\Hom^\abstr(\abstr(G),\abstr(\Sigma_{\mathcal X}))$$ -is an equivalence, where the group $\Sigma_{\mathcal X}$ (as a pointed connected groupoid) is the component of the groupoid $\Set$, pointed at $\mathcal X$. The component information is moot since we're talking about pointed maps from $\BG$ and we see that $\Hom(G,\Sigma_{\mathcal X})$ is equivalent to $\sum_{F:\BG_\div\to\Set}(\mathcal X=F(\shape_G))$. Finally, -$$\mathrm{pr}:\sum_{\mathcal X}\sum_{F:\BG_\div\to\Set}(\mathcal X=F(\shape_G))\we -(\BG_\div\to\Set),\quad \mathrm{pr}(\mathcal X,F,p)\defequi F -$$ -is an equivalence (since $\sum_{\mathcal X}(\mathcal X=F(\shape_G))$ is contractible). -Backtracking these equivalences we see that we have established -\begin{lemma} - \label{lem:actionsconcreteandabstract} - Let $G$ be a group. Then the map - $$\ev_{\shape_G}:\GSet\to\Set^\abstr_{\abstr(G)},\qquad \ev_{\shape_G}(X)\defequi(X(\shape_G),a_X) -$$ -is an equivalence, where the homomorphism $a_X:\Hom^\abstr(\abstr(G), \abstr(\Sigma_{X(\shape_G)}))$ is given by transport $X:\USymG\defequi(\shape_G=\shape_G)\to (X(\shape_G)=X(\shape_G))$. -\end{lemma} -If $X$ is a $G$-set, $g:\USymG$ and $x:X(\shape_G)$, we seek forgiveness for writing $g\cdot x:X(\shape_G)$ instead of $\cast(a_X(g))(x)$.\footnote{and I ask forgiveness for strongly disliking the use of ``$\cast$'' as a name for some tacitly understood map!} - -\begin{example} - \label{ex:abstrandconj} - Let $H$ and $G$ be groups. Recall that the set of homomorphisms from $H$ to $G$ is a $G$-set in a natural way: -$$\Hom(H,G):\BG\to\Set,\quad \Hom(H,G)(y)\defequi \sum_{F:\BH_\div\to \BG_\div}(y=F(\shape_H)).$$ - -What abstract $\abstr(G)$-set does this correspond to? -In particular, under the equivalence $\abstr:\Hom(H,G)\to\Hom^\abstr(\abstr(H),\abstr(G))$, what is the corresponding action of $\abstr(G)$ on the abstract homomorphisms? - -The answer is that $g:\USymG$ acts on $\Hom^\abstr(\abstr(H),\abstr(G))$ by postcomposing with conjugation $\conj^g$ by $g$ as defined in \cref{ex:conjhomo}. - -Let us spell this out in some detail: -If $(F,p):\Hom(H,G)(\shape_G)\defequi - \sum_{F:\BH_\div\to \BG_\div}(\shape_G=F(\shape_H))$ and $g:\USymG$, then $g\cdot(F,p)\defequi(F,p\,g^{-1})$. If we show that the action of $g$ sends $\abstr(F,p)$ to $\conj^g\circ\abstr(F,p)$ we are done. - -Recall that $\abstr(F,p)$ consists of the composite -$$\xymatrix{\USymH\ar[r]^-{F^=}&(F(\shape_H)=F(\shape_G))\ar[rr]^-{t\mapsto p^{-1}t\,p}&&\USymG},$$ -(\ie $\abstr(F,p)$ applied to $q:\USymH $ is $p^{-1}F^=(q)\,p$) together with the proof that this is an abstract group homomorphism. -We see that $\abstr(F,p\,g^{-1})$ is given by conjugation: -$q\mapsto(p\,g^{-1})^{-1}F^=(q)\,(p\,g^{-1})=g\,(p^{-1}F^=(q)\,p)\,g^{-1}$, or in other words $\conj^g\circ\abstr(F,p)$. -\end{example} -For reference we list the conclusion of this example as a lemma: -\begin{lemma}\label{lem:abstrandconj} - If $H$ and $G$ are groups, then the equivalence of \cref{lem:actionsconcreteandabstract} sends the $G$-set $\Hom(H,G)$ to the $\abstr(G)$-set $\Hom^\abstr(\abstr(H),\abstr(G))$ with action given by postcomposing with conjugation by elements of $\abstr(G)$. -\end{lemma} - -If $f:\Hom(G,G')$ is a homomorphism, then precomposition with $\Bf:\BG\to \BG'$ defines a map $$f^*:(G'\text{-}\Set)\to(G\text{-}\Set).$$ -\marginnote{Recall that \cref{lem:eq-mono-cover} told us that $f$ is an epimorphism precisely when $\USymf$ is a surjection.} -We will have the occasion to use the following result which essentially says that if $f:\Hom(G,G')$ is an epimorphism, then $f^*$ embeds the type of $G'$-sets as some of the components of the type of $G$-sets. -\begin{lemma} - \label{lem:epifullyfaithful} - Let $G$ and $G'$ be groups and let $f:\Hom(G,G')$ be an epimorphism. - Then the map $f^*:(G'\text{-}\Set)\to(G\text{-}\Set)$ (induced by precomposition with $\Bf:\BG\to \BG'$) is ``fully faithful'' in the sense that if $X,Y$ are $G'$-sets, then -$$f^*:(X=Y)\to(f^*X=f^*Y) -$$ -is an equivalence. -\end{lemma} -\begin{proof} - Evaluation at $\shape_G$ yields an injective map -$$\mathrm{ev}_{\shape_G}:(f^*X=f^*Y)\to(X(f(\shape_G)=Y(f(\shape_G)))$$ and the composite -$$\mathrm{ev}_{\shape_G}f^*=\mathrm{ev}_{f(\shape_G)}:(X=Y)\to(X(f(\shape_G)=Y(f(\shape_G)))$$ - is the likewise injective, so $f^*:(X=Y)\to(f^*X=f^*Y)$ is injective. - -For surjectivity, let $F':f^*X=f^*Y$ and write, for typographical convenience, $a:X(f(\shape_G)=Y(f(\shape_G))$ for $\mathrm{ev}_{\shape_G}F'\defequi F'_{\shape_G}$. -By the equivalence between $G$-sets and $\abstr(G)$-sets, $F'$ is uniquely pinned down by $a$ and the requirement that for all $g'=f(g)$ with $g:\USymG$ the diagram -$$\xymatrix{X(f(\shape_G))\ar@{=}[r]^{X({g'})}\ar@{=}[d]_{a}& - X(f(\shape_G))\ar@{=}[d]_{a}\\ - Y(f(\shape_G))\ar@{=}[r]^{Y({g'})}&Y(f(\shape_G))} -$$ -commutes. Likewise, (using transport along the identity $p_f:\shape_{G'}=f(\shape_G)$) an $F:X=Y$ in the preimage of $a$ is pinned down by the commutativity of the same diagram, but with $g':f(\shape_G)=f(\shape_G)$ arbitrary (an a priori more severe requirement, again reflecting injectivity). However, when $f:\USymG\to\USymG'$ is surjective these requirements coincide, showing that $f^*$ is an equivalence. - - -% Fix for the moment an $a:X(f(\shape_G)=Y(f(\shape_G))$ - -% Now, by transport along the identity $p_f:\shape_{G'}=f(\shape_G)$ and the equivalence between $G'$-sets and $\abstr(G')$-sets, an identity $F':X=Y$ of $G'$-sets is uniquely pinned down by an identity $F'_{f(\shape_G)}:X(f(\shape_G)=Y(f(\shape_G))$ together with the proposition that for all $g':f(\shape_G)=f(\shape_G)$ the diagram $$\xymatrix{X(f(\shape_G))\ar@{=}[r]^{X_{g'}}\ar@{=}[d]_{F'_{f(\shape_G)}}& -% X(f(\shape_G))\ar@{=}[d]_{F'_{f(\shape_G)}}\\ -% Y(f(\shape_G))\ar@{=}[r]^{Y_{g'}}&Y(f(\shape_G))} -% $$ -% commutes. Likewise, an identity $F:f^*X=f^*Y$ is given by exactly the same data, except that the diagram is only required to commute for $g'=f(g)$ for all $g:\USymG$. But when $f:\USymG\to\USymG'$ these requirements coincide. - - -% ; $F:X=Y$ is in the preimage of $a:X(f(\shape_G)=Y(f(\shape_G))$ if and only if $a=F_{f(\shape_G)}$ and for all $g':f(\shape_G)=f(\shape_G)$ the diagram -% $$\xymatrix{X(f(\shape_G))\ar@{=}[r]^{X_{g'}}\ar@{=}[d]_{F_{f(\shape_G)}}& -% X(f(\shape_G))\ar@{=}[d]_{F_{f(\shape_G)}}\\ -% Y(f(\shape_G))\ar@{=}[r]^{Y_{g'}}&Y(f(\shape_G))} -% $$ -% commutes. However, since $f$ is surjective there is a $g:\USymG$ so that $g'=f(g)$. Therefore, anything in $f^*X=f^*Y$ which is in the preimage of $a$ is in the image of $f^*:X=Y$ and we have shown that $f^*$ is also a surjection. -\end{proof} - -\section{Semidirect products} -\label{sec:Semidirect-products}{\color{red} just moved without proofreading BID 211116. Problem with $\USym$ followed by composite MAB 240815.} - -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{xca:connected-trivia-1} 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} -\footnote{{\color{red}MUST BE MOVED TO THE SUBGROUP CHAPTER}} - -\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 \USymG \times \USymH$. -Now use that to transport the multiplication operation of the group $\USym { G \ltimes \tilde H }$ to the set $\USymG \times \USymH$. -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 $\USymG \times \USymH$, 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 pullback} -\label{sec:pullback} -Given two functions $f:B\to D$ and $g:C\to D$ with common target, the ``pullback'' which we will now define should be thought about as the type of all pairs of elements $(b,c):B\times C$ so that $f(b)=g(c)$. This construction is important in many situations also beyond group theory. - -\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 $\prj_B:\prod(f,g)\to B$ and $\prj_C:\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]^{\prj_C}\ar[d]^{\prj_B}&C\ar[d]^g\\B\ar[r]^f&\,D.}$$ -\end{definition} -\begin{xca} - \marginnote{Illustrating the exercise: if the solid diagram commutes there is a unique dotted arrow so that the resulting diagram commutes: - $$\xymatrix{A\ar@{.>}[dr]\ar[drr]\ar[ddr]&&\\ - &B\times_DC\ar[r]\ar[d]&C\ar[d]\\&B\ar[r]&D} - $$} - \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} -In view of \cref{xca:univpropofpullback} we will say that we have a \emph{pullback diagram}\index{pullback diagram} -$$\xymatrix{A\ar[d]^{g'}\ar[r]^{f'}&C\ar[d]^g\\B\ar[r]^f&D}$$ -to indicate that we have an element in $(A\to B)\times_{(A\to D)}(A\to C)$ such that the resulting map $A\to B\times_DC$ is an equivalence. - -\begin{example} - \marginnote{Preimage as a pullback: $$\xymatrix{f^{-1}(d)\ar[d]\ar[r]&\bn1\ar[d]^d\\B\ar[r]^f&D}$$} - 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 \coverings of the circle: we % will see in \cref{lem:iso2} we - have a pullback -$$\xymatrix{S^1\times\B 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 \covering 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'\gcd(a,b)$ and $b=b'\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 $\gcd(a,b)$\th root of unity. Each of the $\gcd(a,b)$-choices of $\zeta$ contributes in this way to a component of the pullback. In more detail: identifying the cyclic group $C_{\gcd(a,b)}$ of order $\gcd(a,b)$ with the group of $g$\th roots of unity, the top horizontal map $S^1\times C_{\gcd(a,b)}\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 $\lcm(a,b)=a'b$ is hidden in the pullback; in the present example it is demonstrated that the map(s) across the diagram makes each component of the pullback a copy of the $\lcm(a,b)$-fold \covering. -\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$.\qedhere - \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(\shape_H,\pt_{H'},p_{f'}p_f^{-1})$$ of the pullback $\BH\times_{\BG}\BH'$ (where $p_f:\shape_G=f(\shape_H)$ is the name we chose for the data displaying $f$ as a pointed map, so that $p_{f'}p_f^{-1}:f(\shape_H)=f'(\pt_{H'})$). - -If $(H,f,!)$ and $(H',f',!)$ are monomorphisms into $G$, then the pullback is called the \emph{intersection}\index{intersection! of monomorphisms} 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 intersection $a\ZZ\cap b\ZZ$ of the subgroups $a\ZZ$ and $b\ZZ$ of $\ZZ$. -\end{example} -% \begin{example}this came out wrong DELETE June -% If $H,K:\typemono_G$ with $X,Y:\BG\to\Set$ being the corresponding transitive $G$-sets under the equivalence $E$, then the intersection of $H$ and $K$ corresponds to the $G$-set $X\times Y:\BG\to\Set$ (with $(X\times Y)(x)\defequi X(x)\times Y(x)$). -% \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 - $$ - \Hom(K,H)\times_{\Hom(K,G)}\Hom(K,H')\simeq \Hom(K,H\times_GH') - $$ - for all groups $K$ and an equivalence - \[ - \USymH \times_{\USymG} \USymH' - \simeq (\shape_{H\times_GH'}=\shape_{H\times_GH'}).\text{\footnotemark} - \] - Elevate the last equivalence to a statement about abstract groups.\footnotetext{% - Hint: set $A\defequi \Sc$, $B\defequi \BH$, $C\defequi \BH'$ and $D\defequi \BG$.} -\end{xca} - -\begin{remark} - The pullback is an example of when a construction of types \emph{not} preserving connectivity can be used profitably also for groups. - We get the pullback of groups by restricting to a pointed component, but also the other components have group theoretic importance. - We will return to this when discussing subgroups. -\end{remark} - - - -\section{Sums of groups} -\label{sec:coprod} -We have seen how the group of integers $\ZZ=(S^1,\base)$ synthesizes the notion of one symmetry with no relations: every symmetry in the circle is of the form $\Sloop^n$ for some unique $n$. Also, given any group $G=\Aut_A(a)$, the set $a=a$ of symmetries of $a$ corresponds to the set of homomorphisms $\ZZ\to G$, \ie to pointed functions $(S^1,\base)\to_*(A,a)$ by evaluation at $\Sloop$. What happens if we want to study more than one symmetry at the time? - -For instance, is there a group $\ZZ\vee\ZZ$ so that for any group $G=\Aut_A(a)$ a homomorphism $\ZZ\vee\ZZ\to G$ corresponds to \emph{two} symmetries of $a$? -At the very least, $\ZZ\vee\ZZ$ itself would have to have two symmetries and these two can't have any relation, since in a general group $G=\Aut_A(a)$ there is a priori no telling what the relation between the symmetries of $a$ might be. -Now, \emph{one} symmetry is given by a pointed function $(S^1,\base)\to_*(A,a)$ and so a \emph{pair} of symmetries is given by a function $f:S^1+S^1\to A$ with the property that $f$ sends each of the base points of the circles to $a$. But $S^1+S^1$ is not connected, and so not a group. To fix this we take the clue from the requirement that both the base points were to be sent to a common base point and \emph{define} $S^1\vee S^1$ to be what we get from $S^1+S^1$ when we \emph{insert an identity} between the two basepoints. -\marginnote{$S^1\vee S^1$ if formed from $S^1+S^1$ by inserting an identity$$\xymatrix{\base\ar@(ul,dl)[]|{\Sloop}\ar@{.>}[rr]^{\text{identify!}}&&\base\ar@(ur,dr)[]|{\Sloop}} - $$} - -The amazing thing is that this works -- an enormous simplification of the classical construction of the ``free products'' or ``amalgamated sum'' of groups. We need to show that the ``wedge'' $S^1\vee S^1$ is indeed a group, and this proof simultaneously unpacks the classical description. - -We start by giving a definition of the wedge construction which is important for pointed types in general and then prove that the wedge of two groups is a group whose symmetries are arbitrary ``words'' in the original symmetries. - -\begin{definition} - \label{def:wedge} - Let $(A_1,a_1)$ and $(A_2,a_2)$ be pointed types. The \emph{wedge}\index{wedge of pointed types} is the pointed type $(A_1\vee A_2,a_{12})$ given as a higher inductive type by - \begin{enumerate} - \item functions $i_1:A_1\to A_1\vee A_2$ and $i_2:A_2\to A_1\vee A_2$ - \item an identity $g:i_1a_1=i_2a_2$. - \end{enumerate} -We point this type at $a_{12}\defequi i_1a_1$. - The function -$$i^g_2:(a_2=_{A_2}a_2)\to(a_{12}=_{A_1\vee A_2}a_{12})$$ -is defined by $i^g_2(p)\defequi g^{-1}i_2(p)g$, whereas (for notational consistency only) we set $i_1^g\defequi i_1:(a_1=_{A_1}a_1)\to(a_{12}=_{A_1\vee A_2}a_{12})$. -Simplifying by writing $i:A_1+A_2\to A_1\vee A_2$ for the function given by $i_1$ and $i_2$ (with basepoints systematically left out of the notation), -the induction principle is -$$\prod_{C:(A_1\vee A_2)\to\UU}\sum_{s:\prod_{a:A_1+A_2}Ci(a)} -((s(a_1)=C(g^{-1})s(a_2))\,\to\,\prod_{x:(A_1\vee A_2)}C(x)).$$ -\end{definition} - -Unraveling the induction principle we see that if $B$ is a pointed type, then a pointed function $f:A_1\vee A_2\to_* B$ is given by providing pointed functions $f_1:A_1\to_* B$ and $f_2:A_2\to_* B$ -- the identity $f_1(a_1)=f_2(a_2)$ which seems to be missing is provided by the requirement of the functions being pointed. For the record -\begin{lemma} - \label{lem:univvee} - If $B$ is a pointed type, then the function - $$i^*:(A_1\vee A_2\to_*B)\to(A_1\to_*B)\times(A_2\to_*B),\qquad i^*(f)=(fi_1,fi_2) -$$ -is an equivalence. -\end{lemma} - - - -To the right you see a picture of $i_2^g(p)$: \marginnote{$$ -\xy (-20,20)*+{};(-20,20)*+{} -**\crv{(15,20)&(18,20)&(-10,35)&(10,45)&(25,30)&(20,19)&(0,20)} -%?>*\dir{>} -?(0)*{} *!LD!/^-20pt/{i_1A_1} -?(.45)*{} *!LD!/^2pt/{>} -?(.95)*{} *!LD!/^-15pt/{g^{-1}} -?(.03)*{} *!LD!/^-5pt/{g} -?(.55)*{} *!LD!/^-7pt/{i_2p} -?(.65)*{} *!LD!/^-30pt/{i_2A_2} -?(.87)*{} *!LD!/^-12pt/{i_2a_2} -?(.86)*{} *!LD!/^-2pt/{\bullet} -?(1)*{} *!LD!/^-2pt/{\bullet} -?(1)*{} *!LD!/^-12pt/{a_{12}} -\endxy -$$}it is the symmetry of the base point $a_{12}\defequi i_1a_1$ you get by \emph{first} moving to $i_2a_2$ with $g$, \emph{then} travel around with $p$ ($i_2p$, really) and finally go home to the basepoint with the inverse of $g$. - -\marginnote{The idea is that an identity in $a_{12}=x$ can be factored into a string of identities, each lying solely in $A_1$ or in $A_2$. We define a family of sets consisting of exactly such strings of identities -- it is a set since $A_1$ and $A_2$ are groupoids -- and prove that it is equivalent to the family $P(x)\defequi(a_{12}=_{A_1\vee A_2}x)$ which consequently must be a family of sets. -We need to be able to determine whether a symmetry is reflexivity or not, but once we know that, the symmetries of the base point in the wedge are then given by ``words $p_0p_1\dots p_n$'' where the $p_j$ alternate between being symmetries in the first or the second group, and none of the $p_j$ for positive $j$ are allowed to be reflexivity. Note that there order of the $p_j$s is not negotiable: if I shuffle them I get a new symmetry.} - - -\begin{definition} - \label{def:sumofgroup} - If $G_1=\Aut_{A_1}(a_1)$ and $G_2=\Aut_{A_2}(a_2)$ are groups, then their \emph{sum}\index{sum of groups} is defined as - $$G_1\vee G_2\defequi \Aut_{A_1\vee A_2}(a_{12}).$$ - The homomorphisms $i_1:G_1\to G_1\vee G_2$ and $i_2:G_2\to G_1\vee G_2$ induced from the structure maps $i_1:A_1\to A_1\vee A_2$ and $i_2:A_2\to A_1\vee A_2$ are also referred to as \emph{structure maps}. -\end{definition} -\begin{lemma} - \label{lem:sumofgroupsISsum} If $G_1$, $G_2$ and $G$ are groups, then the function - $$\Hom(G_1\vee G_2,G)\to\Hom(G_1,G)\times\Hom(G_2,G)$$ -given by restriction along the structure maps is an equivalence. -\end{lemma} -\begin{proof} - This is a special case of \cref{lem:univvee}. -\end{proof} -Specializing further, we return to our initial motivation and see that mapping out of a wedge of two circles \emph{exactly} captures the information of two independent symmetries: -\begin{corollary} - \label{cor:ZplusZuniv} - If $G$ is a group, then the functions - $$\Hom(\ZZ\vee\ZZ,G)\to \Hom(\ZZ,G)\times\Hom(\ZZ,G)\simeq \USymG\times \USymG$$ - is an equivalence. -\end{corollary} - -\begin{xca}\label{xca:whatAREabeliangroups} - This leads to the following characterization of abelian groups\marginnote{% - \wip{Do we know at this point that this extension problem is a proposition, - \ie that the wedge inclusion is an epimorphism? - Check re pointedness.}} - formulated purely in terms of pointed connected groupoids - (with no direct reference to identity types). - A group $G$ is abelian if and only if the canonical map\marginnote{% - \begin{tikzcd}[ampersand replacement=\&] - \BG\vee\BG\ar[r,"\fold"]\ar[d,"\text{inclusion}"'] \& \BG \\ - \BG\times\BG\ar[ur,dashed] - \end{tikzcd}} - \[ - \fold :\BG\vee \BG\ptdto \BG - \] - (given via \cref{lem:sumofgroupsISsum} by $\id_G:G\to G$) - extends over the inclusion - \[ - i:\BG\vee \BG\ptdto \BG\times \BG - \] - (given by the inclusions $\incl_1,\incl_2:G\to G\times G$). - - As a cute aside, one can see that the required map $\BG\times\BG\ptdto\BG$ - actually doesn't need to be pointed: - factoring - $\fold:\BG\vee\BG\to\BG$ over $i:\BG\vee\BG\to\BG\times\BG$ - -- even in an unpointed way -- kills all ``commutators'' - $ghg^{-1}h^{-1}:\USym(G\vee G)$. - (\wip{is this still a proposition, or do we need to truncate?}) -\end{xca} - -We end the section by proving that wedges of decidable groups are decidable groups and that they can be given the classical description in terms of words. - - -\begin{lemma} - \label{lem:wedgeofgpoidisgpoid} - Let $G_1\defequi\Aut_{A_1}(a_1)$ and $G_2\defequi\Aut_{A_2}(a_2)$ be decidable groups, then the wedge sum $G_1\vee G_2\defequi\Aut_{A_1\vee A_2}(a_{12})$ is a decidable group. - -Let $C_1$ be the set of strings $(p_0,n,p_1,\dots,p_n)$ with $n:\NN$ and, for $0\leq j\leq n$ -\begin{itemize} -\item $p_{j}:\USymG_1%\defequi (a_1=a_1) - $ for even $j$ -\item $p_{j}:\USymG_2%\defequi (a_2=a_2) - $ for odd $j$ and -\item $p_j$ is not reflexivity for $j$ positive -\end{itemize} -(the last requirement makes sense and is a proposition since our groups are decidable). - - Then the function given by composition in $\USymG_{12}\defequi(a_{12}=a_{12})$ - $$\beta:C_1\to\USymG_{12}%\defequi(a_{12}=a_{12}) - ,\qquad\beta(p_0,n,p_1,\dots p_n)\defequi i_1^gp_0i_2^gp_1i_1^gp_2\dots i_?^gp_n$$ -(where $i_?^gp_n$ is $i_1^gp_n$ or $i_2^gp_n$ according to whether $n$ is even or odd) is an equivalence. -\end{lemma} -\begin{proof} - That the wedge is connected follows by transitivity of identifications, - if necessary passing through the identification $g:i_1a_1=i_2a_2$ in the wedge. - -We must prove that the wedge is a groupoid, \ie that all identity types are sets, which we do by giving an explicit description of the universal \covering. - - We use the notation of \cref{def:wedge} freely, and for ease of notation, let $a_{2k+i}\defequi a_i$ and $i_{2k+i}^g\defequi i_i^g$ for $i=1,2$, $k:\NN$. -Define families of sets -$$C_i:A_i\to\Set,\qquad i=1,2$$ -by -$$ -C_i(x)\defequi(a_i=_{A_i}x)\times -\sum_{n:\NN}\prod_{1\leq k\leq n}\sum_{p_k:a_{i+k}= a_{i+k}}(p_k\neq\refl {a_{i+k}}) -$$ -when $x:A_i$. Note that $p_k\neq\refl{a_{i+k}}$ is a proposition; we leave it out when naming elements. Hence, an element in $C_1(a)$ is a tuple -$(p_0,n,p_1,\dots,p_n)$ where $p_0:a_1=_{A_1}a$, $p_1:a_2=_{A_2}a_2$, $p_2:a_1=_{A_1}a_1$, and so on -- alternating between symmetries of $a_1$ and $a_2$, and where $p_0$ is the only identity allowed to be $\refl{}$. Define $C_{12}:C_1(a_1)\to C_2(a_2)$ by -$$C_{12}(p_0,n,p_1\dots,p_n)= -\begin{cases} - (\refl{a_2}0,)&\text{ if }p_0=\refl{a_1}, n=0,\\ - (p_1,n-1,p_2\dots,p_n)& \text{ if }p_0=\refl{a_1},n\neq0,\\ - (\refl{a_2},n+1,p_0,\dots,p_n)& \text{ if }p_0\neq\refl{a_1}. -\end{cases} -$$ -It is perhaps instructive to see a table of the values $C_{12}(p_0,n,p_1,\dots,p_n)$ for $n<3$: -\begin{center} - \begin{tabular}{r|c cc} - &$(p_0,0)$&$(p_0,1,p_1)$&$(p_0,2,p_1,p_2)$\\ - \hline - $p_0=\refl{a_1}$&$(\refl{a_2},0)$&$(p_1,0)$&$(p_1,1,p_2)$\\ - $p_0\neq\refl{a_1}$&$(\refl{a_2},1,p_0)$&$(\refl{a_2},2,p_0,p_1)$&$(\refl{a_2},3,p_0,p_1,p_2)$ - \end{tabular} -\end{center} -Since $C_{12}$ is an equivalence, the triple $(C_1,C_2,C_{12})$ defines a family -$$C:A_1\vee A_2\to\Set.$$ -In particular, $C(a_{12})\defequi C_1(a_1)$. -For $x:A_1$ we let $i^C_1:C_1(x)\to C(i_1(x))$ be the induced equivalence, and likewise for $i^C_2$. -We will show that $C$ is equivalent to $P\defequi \pathsp{a_{12}}$, where $P(x)\defequi(a_{12}=x)$, and so that the identity types in the wedge are equal to the sets provided by $C$. - -One direction is by transport in $C$; more precisely, -$$\alpha:\prod_{x:A_1\vee A_2}(P(x)\to C(x))$$ is given by transport with $\alpha(a_{12})(\refl{a_{12}})\defequi(\refl{a_{1}},0):C(a_{12})$. -The other way, -$$\beta:\prod_{x:A_1\vee A_2}(C(x)\to P(x))$$ is given by composing identities, using the glue $g$ to make their ends meet: -$$\beta(i_1a)(p_0,n,p_1,\dots,p_n)\defequi i_1(p_0)i_2^g(p_1)i_3^g(p_2) \dots i_{n+1}^g(p_n)$$ -(here the definition $\dots i_3^g\defequi i_1^g\defequi i_1$ proves handy since we don't need to distinguish the odd and even cases) -and likewise -$$\beta(i_2a)(p_0,n,p_1,\dots,p_n)\defequi i_2(p_0)g\,i_1^g(p_1)i_2^g(p_2) \dots i_{n}^g(p_n)$$ and compatibility with the glue $C_{12}$ is clear since the composite $\refl{x}p$ is equal to $p$. - -For notational convenience, we hide the $x$ in $\alpha(x)(p)$ and $\beta(x)(p)$ from now on. - -That $\beta\alpha(p)=p$ follows by path induction: it is enough to prove it for $x=a_{12}$ and -$p\defequi\refl{a_{12}}$: -$$\beta\alpha(\refl{a_{12}})=\beta(\refl{a_1},0)=i_1^g\refl{a_1}=\refl{a_{12}}.$$ - -That $\alpha\beta(p_0,n,p_1\dots,p_n)=(p_0,n,p_1,\dots,p_n)$ follows by induction on $n$ and $p_0$. For $n=0$ it is enough to consider $x=a_{12}$ and $p_0=\refl{a_1}$, and then -$\alpha\beta(\refl{a_1},0)\defequi\alpha(\refl{a_{12}})\defequi(\refl{a_1},0)$. In general, (for $n>0$) -\begin{align*} - \alpha\beta(p_0,n,p_1\dots,p_n) -=&\trp[C]{i_1(p_0)i_2^g(p_1)i_1^g(p_2) \dots i_{n+1}^g(p_n)}(\refl{a_1,0})\\ -=&\trp[C]{i_1(p_0)}\dots\trp[C]{i_{n+1}^g(p_n)}(\refl{a_1,0}). -\end{align*} - The induction step is as follows: let $0< k\leq n$, then -\begin{align*} - &\trp[C]{i_k^gp_{k-1}}i^C_{k-1}(p_k,n-k-1,p_{k+1},\dots,p_n)\\ - =&\trp[C]{i_k^gp_{k-1}}i^C_k(\refl{a_{k-1}},n-k,p_k,\dots,p_n)\\ - =&i^C_k\trp[C_k]{p_{k-1}}(\refl{a_{k-1}},n-k,p_k,\dots,p_n)\\ - =&(p_{k-1},n-k,p_k,\dots,p_n). -\end{align*} -%((please see whether this makes sense to anybody but yvt)) -\end{proof} - \section{Heaps \texorpdfstring{$(\dagger)$}{(\textdagger) \color{red} just moved from symmetry without proofreading BID211116}} \label{sec:heaps} diff --git a/subgroups.tex b/subgroups.tex index 73c7ca1..6c765f5 100644 --- a/subgroups.tex +++ b/subgroups.tex @@ -7,6 +7,203 @@ \section{Brief overview of the chapter} TBW (and stolen from the below) +\section{Monomorphisms and epimorphisms} +\label{sec:monoepi} + +In set theory we say that a function $f:B\to C$ of sets is an injection if for all $b,b':B$ we have that $f(b)=f(b')$ implies that $b=b'$. This conforms with our definitions. +%\footnote{This continues to be true in type theory, but since equality needs not be unique, we should in addition require that the two identities $p, f(\sigma(p)):f(b)=f(b')$ are equal.} +Furthermore, since giving a term $b:B$ is equivalent to giving a (necessarily constant) function $c_b:\bn 1\to B$, we could alternatively say that a function $f:B\to C$ is an injection if and only if for any two $g,h:\bn 1\to B$ such that $fg=fh$ we have that $g=h$. In fact, by function extensionality we can replace $\bn 1$ by any set $A$ (two functions are identical if and only if they have identical values at every point). + +Similarly, a function $f:B\to C$ is surjective if for all $c:C$ the preimage $f^{-1}(c)=\sum_{b:B}c=f(b)$ is non-empty. A smart way to say this is to say that the first projection from $\sum_{c:C}\Trunc{f^{-1}(c)}$ to $C$ is an equivalence. Since $B$ is always equivalent to $\sum_{c:C}f^{-1}(c)$, we see that for a surjection $f:B\to C$ and family of propositions $P:C\to \Prop$, the propositions $\prod_{c:C}P(c)$ and $\prod_{b:B}Pf(b)$ are equivalent. In particular, if $g,h:C\to D$ are two functions into a set $D$ the proposition $\prod_{c:C}(g(c)=h(c))$ is equivalent to $\prod_{b:B}(gf(b)=hf(c))$. + +From this we condense the following characterizations of injections and surjections of sets which will prove to generalize nicely to other contexts. +% In other words, an injection between sets is a function $f:B\to C$ such that for any set $A$ and functions $g,h:A\to B$ such that $fg=fh:A\to C$ +% $$\xymatrix{A\ar[r]^f&B\ar@<1ex>[r]^g\ar@<-1ex>[r]_h&C}$$ +% we necessarily have that $g=h$. +\begin{lemma} + \label{lem:injofsetsaremono}Let $f:B\to C$ be a function between sets. + \begin{enumerate} + \item the function is an injection of and only if for any set $A$ and functions $g,h:A\to B$, +$$\xymatrix{A\ar@<1ex>[r]^g\ar@<-1ex>[r]_h&B\ar[r]^f&C},$$ then $fg=fh:A\to C$ implies $g=h$ +\item the function is an injection of and only if for any set $D$ and functions $g,h:C\to D$, +$$\xymatrix{B\ar[r]^f&C\ar@<1ex>[r]^g\ar@<-1ex>[r]_h&D},$$ then $gf=hf:A\to C$ implies $g=h$. + \end{enumerate} +\end{lemma} + + +By \cref{lem:injofsetsaremono} there is a pleasing reformulation which highlights that injections/surjections of sets are characterized by injections of sets of functions: a function of sets $f:B\to C$ is +\begin{enumerate} +\item an injection if and only if for any set $A$ postcomposition by $f$ given an injection from $A\to B$ to $A\to C$ +\item a surjection if and only if for any set $D$ precomposition by $f$ gives an injection from $B\to D$ to $B\to D$. +\end{enumerate} + +This observation about sets translates fruitfully to other contexts and in particular to groups. To make it clear that we talk about group homomorphisms (and not about the underlying unpointed functions of connected groupoids) we resort to standard categorical notation. +\begin{definition}\label{def:monomorphism} +Given groups $G,H$, a homomorphism $f: \Hom(G,H)$ is called a\label{def:epimorphism} +\begin{enumerate} +\item \emph{monomorphism}\index{monomorphism!of groups} if for any group $F$, + postcomposition by $f$ is an injection from $\Hom(F,G)$ to $\Hom(F,H)$, and an +\item \emph{epimorphism}\index{epimorphism!of groups} if for any group $I$, + precomposition by $f$ is an injection from $\Hom(H,I)$ to $\Hom(G,I)$. +\end{enumerate} +The corresponding families of propositions are called +\[ + \ismono,\isepi:\Hom(G,H)\to\Prop.\qedhere +\] +\end{definition} + +\marginnote{$$\xymatrix{\USymG\ar[d]^\simeq\ar[r]^{\US f}&\USymH\ar[d]^\simeq\\ + \Hom(\ZZ,G)\ar[r]^{f_*}\ar[d]^\simeq_\abstr&\Hom(\ZZ,H)\ar[d]^\simeq_\abstr\\ + \Hom^{\abstr}(\ZZ,\abstr(G))\ar[r]^{\abstr f_*}&\Hom^{\abstr}(\ZZ,\abstr(H)) + }$$ +commutes (we've written $\ZZ$ also for $\abstr(\ZZ$) since otherwise it wouldn't fit.} +We've seen that for any group $G$, the underlying set $\USymG\defequi(\shape_G=\shape_G)$ of $\abstr(G)$ is equivalent to the set of homomorphisms $\Hom(\ZZ,G)$ which in turn is equivalent to the set of abstract homomorphisms $\Hom^{\abstr}(\abstr(\ZZ),\abstr(G))$ and that abstraction preserves composition. +Hence, if $f:\Hom(G,H)$ is a group homomorphism, then saying that +$\US f$ is an injection is equivalent to saying that postcomposition by $f$ is an injection $\Hom(\ZZ,G)\to\Hom(\ZZ,H)$. +In this observation, the integers $\ZZ$ plays no more of a r\^ole than $\bn 1$ does in \cref{lem:injofsetsaremono}; we can let the source vary over any group $F$: + + +\begin{lemma}\label{lem:eq-mono-cover} +Let $G$ and $H$ be groups and $f: \Hom(G,H)$ a homomorphism. +The following propositions are equivalent:\label{lem:eq-epi-conn} +\begin{enumerate} +\item\label{it:mono} $f$ is a monomorphism; +\item\label{it:injection} $\US f:\USymG\to\USymH$ is an injection; +\item\label{it:cover} $\Bf_\div:\BG_\div\to \BH_\div$ is a \covering. +\end{enumerate} +\end{lemma} + +\begin{proof} + We have already seen that condition~\ref{it:mono} implies condition~\ref{it:injection} (let $F$ be $\ZZ$). + Conversely, suppose that \ref{it:injection} holds and $F$ is a group. Consider the commutative diagram +$$\xymatrix{\Hom(F,G)\ar[r]\ar[d]&\Hom(F,H)\ar[d]\\ + (\Hom(\ZZ,F)\to\Hom(\ZZ,G))\ar[r]&(\Hom(\ZZ,F)\to\Hom(\ZZ,H)),}$$ +where the vertical maps are the injections from the sets of (abstract) homomorphism to the sets of functions of underlying sets and the horizontal maps are postcomposition with $f$. Since the bottom function is by assumption is an injection, so is the upper one. +\footnote{ Alternatively: and $g,h:\Hom(F,G)$. Then $fg=fh$ implies that for all $p:\Hom(\ZZ,F)$ we have by associativity that $f(gp)=(fg)p=(fh)p=f(hp)$, and so, by assumption, that $gp=hp$. + Again, by function extensionality (of functions $\Hom(\ZZ,F)\to\Hom(\ZZ,G)$), this is exactly saying that $\US g$ is identical to $\US h$.} + + The equivalence of \ref{it:cover} and \ref{it:injection} follows +immediately from \cref{cor:fib-vs-path}\ref{set-fib-vs-path}, using +that $\BG$ is connected and $f$ is pointed and the equivalence between $\Hom(G,H)$ and $\BG\ptdto \BH$. +\end{proof} + +Similarly, we have: +\begin{lemma}\label{lem:epi-surj} + The following propositions are equivalent: +\begin{enumerate}[label=(\arabic*')] +\item\label{it:epi} $f$ is an epimorphism; +\item\label{it:surjection} $\US f:\USymG\to\USymH$ is a surjection. +\item\label{it:connfib} $\Bf_\div:\BG_\div\to \BH_\div$ has connected fibers. +\end{enumerate} +\end{lemma} + +\begin{proof} + The equivalence of \ref{it:surjection} and \ref{it:connfib} is immediate. + + For the rest, the easy direction is that \ref{it:surjection} implies \ref{it:epi}: + (TODO) + + The harder direction, that \ref{it:epi} implies \ref{it:surjection}, + is a corollary of the following lemma, which states that monos are equalizers. + Indeed, we can factor any $f : \Hom(G,H)$ via the image as a surjection followed + by a mono: + \[ + \begin{tikzcd}[cramped] + G \ar[r,"q"] & \im(f) \ar[r,"i"] & H + \end{tikzcd} + \] + If $f$ is an epi, then so is $i$. But $i$ is an equalizer, + \[ + \begin{tikzcd}[cramped] + \im(f) \ar[r,"i"] & H\ar[r,shift left,"\varphi"] + \ar[r,shift right,"\psi"'] & L, + \end{tikzcd} + \] + so as an epi, $\varphi i = \psi i$ implies $\varphi = \psi$, so $i$ + is an equalizer of already equal homomorphisms, so $i$ is an isomorphism, + which implies that $f$ is surjective. +\end{proof} + +\begin{lemma}\label{lem:monos-are-equalizers} + Every monomorphism $i : H \to G$ is an equalizer.\footnote{% + This proof follows an idea by \citeauthor{TrimbleEpisSurjective}\footnotemark{}.}% + \footcitetext{TrimbleEpisSurjective} +\end{lemma} +\begin{proof}[Proof draft.] Consider the projection $\pi : G \to G/H$ to the set of cosets. + Let $j : G/H \to A$ be an injection into a group $A$. + (We could for instance let $A$ be the free (abelian) group on $G/H$. [Add xref to statement that inclusion of generators in an injection.]) + + Consider the group $W \defeq \Aut_E(\sh_G,\cst{\sh_A})$, where + \[ + E \defeq \sum_{t : \BG}\bigl((\sh_G \eqto t) \to \BA\bigr). + \] + We have two homomorphisms $\varphi,\psi : G \to W$ with the same underlying map, + $t \mapsto (t , \cst{\sh_A})$, but with different pointing paths: + \[ + \varphi_\pt \defeq \refl{\sh_G,\cst{\sh_A}}, \quad + \psi_\pt \defeq (\refl{\sh_G}, j\pi). + \] + The equalizer of $\varphi$ and $\psi$ thus consists of all $g:\USymG$ + such that $j\pi(gg') = j\pi(g')$ for all $g':\USymG$. Since $j$ is injective, + this is equivalent to $\pi(gg')=\pi(g')$ for all $g':\USymG$, and this holds + if and only if $g$ belongs to $H$. +\end{proof} + +\subsection{Any symmetry is a symmetry in $\Set$} +\label{sec:groupssubperm} + + +The correspondence between groups and abstract groups allows for a cute proof of what is often stated as ``any group is a permutation group'', which in our parlance translates to ``any symmetry is a symmetry in $\Set$''. +% \footnote{which reminds me of the following: my lecturer in cosmology once tried to publish a paper about rotating black holes, only to have it rejected because it turned out that it was his universe, not the black hole, that was rotating} + +Recall the principal $G$-torsor $\princ G:\BG\to\Set$. +Since $\princ G(\shape_G)\defequi \USymG$ this defines a pointed function $\rho_G:\BG\to_* \BSigma_{\USymG}\defequi(\conncomp \Set {\USymG},\USymG)$, +\marginnote{the letter $\rho$ commemorates the word ``regular''} \ie a homomorphism from $G$ to the permutation group +$$\rho_G:\Hom(G,\Sigma_{\USymG}).$$ +\begin{theorem}[Cayley] + \label{lem:allgpsarepermutationgps} + \marginnote{By \cref{lem:eq-mono-cover} ``$\rho_G$ is a monomorphism'' means that the induced map $\rho_G^\abstr$ from the symmetries of $\shape_G$ in $\BG_\div$ to the symmetries of $\USymG$ in $\Set$ is an injection, \ie ``any symmetry is a symmetry in $\Set$''.}Let $G$ be a group. Then + $\rho_G:\Hom(G,\Sigma_{\USymG}) $ is a monomorphism. +\end{theorem} +\begin{proof} + In view of \cref{lem:eq-mono-cover} we need to show that $\rho_G:\BG\to \conncomp \Set {\USymG}$ is a + \covering. + Under the identity + $$\bar{\pathsp{}}:\BG=(\typetorsor_G,\princ G)\oldequiv (\conncomp{\Set}{\USymG},\USymG)$$ of + \cref{lem:BGbytorsor}, $\rho_G$ translates to the + evaluation map + $$\mathrm{ev}_{\shape_G}:\conncomp{(\BG\to\Set)}{\princ G}\to\conncomp{\Set}{\USymG},\qquad + \mathrm{ev}_{\shape_G}(E)=E(\shape_G).$$ + We must show that the preimages + $\inv{\ev_{\shape_G}}(X)$ for $X:\Sigma_{\USymG}$ are sets. This + fiber is equivalent to + $\sum_{E:\conncomp{(\BG\to\Set)}{\princ G}}(X=E(\shape_G))$ which is a + set precisely when $\sum_{E:\BG\to\Set}(X=E(\shape_G))$ is a set. We + must then show that if $(E,p),(F,q):\sum_{E:\BG\to\Set}(X=E(\shape_G))$, + then the type $(E,p)=(F,q)$, which is equivalent + \marginnote{Note that if $r:\shape_G=x$, then + $\phi(x)=F(r)qp^{-1}E(r)^{-1}$, in a picture + \begin{displaymath} + \xymatrix{&E(pt_G)\ar@{=}[r]^{E(r)}_\to\ar@{=}[dd]_{\phi(pt_G)}^\downarrow&E(x)\ar@{=}[dd]_{\phi(x)}^\downarrow\\ + X\ar@{=}[ur]^p_{\rotatebox{35}{\footnotesize$\to$}}\ar@{=}[dr]^q_{\rotatebox{-35}{\footnotesize$\to$}}&&\\ + &F(\shape_G)\ar@{=}[r]^{F(r)}_\to&F(x)}, + \end{displaymath} +and so $\phi(x)$ (which by nature is independent of such an +$r:\shape_G=x$) is uniquely determined by $(E,p)$ and $(F,q)$. The text says this formally.} +to + $$\prod_{x:\BG}\sum_{\phi(x):E(x)=F(x)}\phi(\shape_G)=qp^{-1},$$ + is a proposition. +If $\phi,\psi:((E,p)=(F,q))$, we + must show that $\phi=\psi$ and since that for $x:\BG$ both $E(x)$ and + $F(x)$ are sets, it is enough to show that the proposition + $\phi(x)=\psi(x)$ is not empty. Let + $f:(\shape_G=x)\to(\phi(x)=\psi(x))$ be given by letting $f(r)$ be the + composite of the identities $\phi(x)=F(r)qp^{-1}E(r)^{-1}=\psi(x)$ + given above. Since $\BG$ is connected, and $\phi(x)=\psi(x)$ is a + proposition, one can consider that $\shape_G=x$ is not empty, and we + are done. +\end{proof} + \section{Subgroups} \label{sec:subgroups} In our discussion of the group $\ZZ\defequi\Aut_{S^1}(\base)$ of integers in \cref{cha:circle} we discovered that some of the symmetries of $\base$ were picked out by the $n$-fold covering (for some particular natural number $n$). On the level of the set $\base\eqto{}\base$, the symmetries picked out are all the iterates (positive or negative or even zero-fold) of $\Sloop^n$. The important thing is that we can compose or invert any of the iterates of $\Sloop^n$ and get new symmetries of the same sort (because of distributivity $nm_1+nm_2=n(m_1+m_2)$). So, while we do not get all symmetries of $\base$ (unless $n=1$), we get what we'd like to call a subgroup of the group of integers. diff --git a/symmetry.tex b/symmetry.tex index f5fa8c6..f90fd97 100644 --- a/symmetry.tex +++ b/symmetry.tex @@ -363,113 +363,6 @@ % on the set $\USymG \times \USymH$, 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)}\trunc{[x]}=_{X/G}\trunc{(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(t,y,!) \defeq (\shape_G \eqto t)$. - Then we calculate: - \begin{align*} - \tilde G_{hG_x} - &\defeq \sum_{u : \BG_x}\tilde G(u) \\ - &\eqto \sum_{t:\BG}\sum_{y:X(t)}\trunc{(\shape_G,x)} =_{X/G} \trunc{(t,y)} - \times (\shape_G \eqto t) \\ - &\equivto \sum_{y:X(\shape_G)}[x] =_{X/G} [y] \defeq \mathcal O_x.\qedhere - \end{align*} -\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} @@ -514,45 +407,6 @@ \section{The isomorphism theorems} $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}