From cc479d3fedb9af5c09cefb141aa85d648b18c84a Mon Sep 17 00:00:00 2001 From: marcbezem Date: Sun, 25 Aug 2024 11:42:29 +0200 Subject: [PATCH] Rem. 4.2.21 replaced by mn 8 --- group.tex | 83 +++++++++++++++++-------------------------------------- 1 file changed, 25 insertions(+), 58 deletions(-) diff --git a/group.tex b/group.tex index 0abd1d5..4263a7c 100644 --- a/group.tex +++ b/group.tex @@ -436,33 +436,10 @@ \subsection{First examples} so we can also identify the trivial group with $\mkgroup (\true,\triv)$, or with $\mkgroup (C,c)$ for any contractible type $C$ and element $c:C$, or - with $\Aut_{S}(x)$ for any set $S$ and element $x:S$. - - \item\label{ex:permgroup} - If $n:\NN$, then the \emph{permutation group of $n$ letters} - (also known as the \emph{symmetric group of order $n$}) is% - \glossary(918Sigma2){$\protect\SG_n$}{symmetric group of order $n$, - \cref{ex:groups}\ref{ex:permgroup}}\index{symmetric group}% - \index{group!symmetric group} - \[ - \SG_n\defequi \Aut_{\Set}(\bn n). %\mkgroup(\FinSet_n,\bn{n}), - \] - The classifying type is thus $\BSG_n\jdeq (\FinSet_n,\bn{n})$, - where $\FinSet_n \jdeq \Set_{(\bn{n})}$ is the groupoid of - sets of cardinality $n$ (\cf \ref{def:groupoidFin}). - - Again, we can also identify the group $\SG_n$ with - $\Aut_\FinSet(\bn{n})$ (by \cref{xca:group-example-details}), with - $\Aut_{\FinSet_n}(\bn n)$ (by \cref{rem:symmetriesofnonconnectedgroupoids}), - or even with $\Aut_{\UU}(\bn n)$ (by stretching the definition of $\Aut$, - using that $\UU_{(\bn n)}$ is a connected groupoid, see~\cref{rem:autinfgp}). - - - If the reader starts worrying about size issues, - see~\cref{rem:groupsarebig}.\footnote{% -This footnote is for those who worry about size issues -- a + with $\Aut_{S}(x)$ for any set $S$ and element $x:S$.\footnote{% +This note is for those who worry about size issues -- a theme we usually ignore in our exposition. -Recall from \MB{updated} \cref{sec:universes} the chain of +Recall from \cref{sec:universes} the chain of universes $\UU_0 : \UU_1 : \UU_2 : \dots$ such that for each $i$ all types in $\UU_i$ are also in $\UU_j$ for all $j>i$. Let $\Set_0$ be the type of sets in $\UU_0$, @@ -494,9 +471,30 @@ \subsection{First examples} However, even with this principle there are groups that only belong to $\typegroup_i$ for $i>0$ large enough. -These matters concerning universes are nontrivial and important, +Issues concerning universes are nontrivial and important, but in this text we have chosen to focus on other matters. } + + \item\label{ex:permgroup} + If $n:\NN$, then the \emph{permutation group of $n$ letters} + (also known as the \emph{symmetric group of order $n$}) is% + \glossary(918Sigma2){$\protect\SG_n$}{symmetric group of order $n$, + \cref{ex:groups}\ref{ex:permgroup}}\index{symmetric group}% + \index{group!symmetric group} + \[ + \SG_n\defequi \Aut_{\Set}(\bn n). %\mkgroup(\FinSet_n,\bn{n}), + \] + The classifying type is thus $\BSG_n\jdeq (\FinSet_n,\bn{n})$, + where $\FinSet_n \jdeq \Set_{(\bn{n})}$ is the groupoid of + sets of cardinality $n$ (\cf \ref{def:groupoidFin}). + + Again, we can also identify the group $\SG_n$ with + $\Aut_\FinSet(\bn{n})$ (by \cref{xca:group-example-details}), with + $\Aut_{\FinSet_n}(\bn n)$ (by \cref{rem:symmetriesofnonconnectedgroupoids}), + or even with $\Aut_{\UU}(\bn n)$ (by stretching the definition of $\Aut$, + using that $\UU_{(\bn n)}$ is a connected groupoid, see~\cref{rem:autinfgp}). + + \item\label{ex:genpermgroup} More generally, if $S$ is a set, is there a pointed connected groupoid $(A,a)$ so that $a\eqto_Aa$ models all the ``permutations'' $S\eqto_{\Set}S$ of $S$? @@ -524,37 +522,6 @@ \subsection{First examples} Also, give an identification of type $\Aut_\Set(\NN)\eqto\Aut_\Set(\zet)$. \end{xca} -\begin{remark} - \label{rem:groupsarebig} - This remark is for those who worry about size issues -- a theme we usually ignore in our exposition. If we - start with a base universe $\UU_0$, the groupoid $\FinSet_n$ of sets of cardinality $n$ is the $\Sigma$-type - $\sum_{A:\UU_0}\Trunc{A\eqto\bn{n}}$ over $\UU_0$ and so (without any modification) will lie in any bigger - universe $\UU_1$. In order to accommodate the permutation groups of sets in $\UU_0$, the universe ``$\UU$'' appearing as - a subscript of the first $\Sigma$-type in \cref{def:pt-conn-groupoid}, appearing later in the definition of - ``group'', needs to be at least as big as $\UU_1$. If $\UU$ is taken to be $\UU_1$, then the type - $\typegroup$ of groups will not be in $\UU_1$, but in some bigger universe $\UU_2$. - If we then choose some group $G:\typegroup$ - and look at its group of automorphisms, $\Aut_\Group(G)$,\footnote{% - \Cref{xca:typegroupisgroupoid} below asks you to verify that $\Group$ - is a (large) groupoid.} - based on the identity type $G \eqto_\Group G$, this will be an element of $\typegroup$ only if the universe $\UU$ in the definition of - $\typegroup$ is at least as big as $\UU_2$. Our convention from \cref{sec:universes} is - that the universes form an ascending chain $\UU_0\subseteq\UU_1\subseteq\UU_2\subseteq\dots$, corresponding - to which there will an ascending chain of types of groups, - \[ - \typegroup_i \defequi \Copy_{\mkgroup}\bigl( (\UU_i)_*^{=1} \bigr) : \UU_{i+1}, - \] - and any group we encounter will be an element of $\typegroup_i$ for $i$ - large enough. - - These matters concerning universes are nontrivial and important, - but in this text we have chosen to focus on other matters.\footnote{% - We will note, however, that the Replacement~\cref{pri:replacement} - often allows us to conclude that a group $G$ belongs to $\typegroup_0$. - This is the case for $\SG_S$, for $S:\Set_0$, and for $\Aut_\Group(G)$, - for $G:\Group_0$, as we invite the reader to check. - Hint: use \cref{xca:comp-loc-small-ess-small}.} -\end{remark} \begin{example}\label{ex:cyclicgroups} In \cref{cor:id-m-cycle} we studied the symmetries of the