new lem:E-preserves-symms

actions.tex

@@ -642,24 +642,21 @@ \subsection{Subgroups as monomorphisms}
 
   The \emph{type of monomorphisms into $G$}\footnote{%
   The similarity of this type with the type of subtypes
-  $\Sub_T \defeq \sum_{S:\UU}\sum_{f:S\to T}\isinj(f)$ 
-  is not coincidental. Both express the idea that a substructure
-  of a structure $X$ is given by a structure preserving map $i$ into $X$
-  that is `injective'. What `injective' means depends on the
-  structure in question. For a group, where the symmetries are key,
-  this means that $\USymi$ is injective.
-  \MB{Integrate with:}
-
- In classical set theory there is an important difference between saying 
-that a function is the inclusion of a subset (which is what one classically
-wants) and saying that it is an injection.  We'll address this in a moment,
-so rest assured that all is well as you read on.\MB{And also with:}
-
-If you're familiar with the set-theoretic flavor of things, you know that it is important to distinguish between subgroups and injective group homomorphisms.
-Our use of monomorphisms can be defended because two monomorphisms into $G$ are identical exactly if they differ by precomposition by an identitification.
-In set-theoretic language this corresponds to saying that a subgroup is an injective abstract homomorphism \emph{modulo} the relation forcing that precomposing with an isomorphism yields identical subgroups.
-Classical set-theory offers the luxury of having a preferred representative in every equivalence class: namely the image of the injection, type theory does not.  We only know that the type $\typemono$ is a set.}
-  \index{type! of monomorphisms into a groups}
+  $\Sub_T \defeq \sum_{S:\UU}\sum_{f:S\to T}\isinj(f)$ in
+  \cref{def:subtype} is not coincidental, and the remarks made 
+  there in \cref{ft:incl-vs-inj} apply here as well.
+
+  In particular, the identity relation on $\typemono_G$
+  identifies precisely the triples that define the same subgroup,
+  namely when their monomorphisms differ by precomposition by an 
+  identification of their underlying groups.
+
+  \MB{We should add in \cref{ch:absgroup} an equivalence between
+  $\typemono_G$ and the subsets of $\USymG$ with the usual closure
+  properties --- the ultimate proof that we have the right 
+  notion of concrete subgroup.}
+  }
+  \index{type! of monomorphisms into a group}
   \glossary(MonoG){$\protect{\typemono_G}$}{type of monomorphisms%
   into the group $G$} 
   is
@@ -769,11 +766,14 @@ \subsection{Subgroups as monomorphisms}
   can be identified with $(\SG_2,i_3,!)$.
 
   Why do we say that $(X_3,3,!):\Sub_{\SG_3}$ from \cref{exa:fix1subSGn}
-  defines the same subgroup as $(\SG_2,i_3,!):\typemono_{\SG_3}$?
-  The reason is that $(X_3,3,!)$ and $E(\SG_2,i_3,!)$ can be identified.
+  defines the same subgroup as $(\SG_2,i_3,!):\typemono_{\SG_3}$
+  from \cref{ex:SGninSGn+1}? The reason is that they pick out
+  the same symmetries in $\SG_3$, as argued in these examples.
+  Moreover, $(X_3,3,!)$ and $E(\SG_2,i_3,!)$ can be identified.
   Note that $X_3(A,!) \jdeq A$ and 
   $\inv\Bi_3 \jdeq \sum_{B:\BSG_2}(A\eqto{}(B+\true))$.
   Now apply \cref{xca:A-is-A-1+1} and verify that the points correspond.
+  \cref{lem:E-preserves-symms} below offers a general result of this kind.
   \end{example}
 
 \begin{xca}\label{xca:SubG=MonoG}
@@ -787,6 +787,30 @@ \subsection{Subgroups as monomorphisms}
 Let $G$ be a group. Then $\typemono_G$ is a set since $\Sub_G$ is.
 \end{corollary}
 
+The following lemma states that $E$ preserves the subsets of
+symmetries that are picked out.
+\begin{lemma}\label{lem:E-preserves-symms}
+  \MB{New:} Let $G$ be a group.
+  For all $(H,i,!) : \typemono_G$ and $g:\USymG$ we have
+  $\exists_{h:\USymH} g = \USymi(h)$ if and only if 
+  $g\cdot_{\inv\Bi}(\sh_H,\Bi_\pt) =(\sh_H,\Bi_\pt)$.
+\end{lemma}
+\begin{proof}
+We spell out:
+$g = \USymi(h)\jdeq(\loops\Bi)(h)\jdeq(\inv\Bi_\pt\cdot\Bi(h)\cdot\Bi_\pt)$.
+
+The action of $g$ on $\inv\Bi(\sh_G) \defeq \sum_{x:\BH}(\sh_G\eqto\Bi(x))$
+is by mapping $(x,p)$ to $(x,p\inv g)$ for any $p:\sh_G\eqto\Bi(x)$.
+Hence, if $g = \USymi(h)$, then
+\begin{align*} 
+g\cdot_{\inv\Bi}(\sh_H,\Bi_\pt) & = (\sh_H,\Bi_\pt\cdot \inv g)\\
+& = (\sh_H,\Bi_\pt \cdot (\inv\Bi_\pt\cdot\Bi(\inv h)\cdot\Bi_\pt))\\
+& = (\sh_H,\Bi(\inv h)\cdot\Bi_\pt) \\
+& = (\sh_H,\Bi_\pt) \quad \text{by transport along $h$.}
+\end{align*}
+The other direction is easy.
+\end{proof}
+
 \marginnote{%
   Which of the equivalent sets $\typemono_G$ and $\Sub_G$ is allowed to be called ``the set of subgroups of $G$'' is, of course, a choice.  It could easily have been the other way around and we informally refer to elements in either sets as ``subgroups'' and use the given equivalence $E$ as needed.
 }%
@@ -818,32 +842,41 @@ \subsection{Subgroups as monomorphisms}
 \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$''.
+For abstract groups there is a result, attributed to Cayley,
+which is often stated as ``any group is a permutation group''. 
+In our parlance this translates to ``any symmetry is a symmetry in $\Set$''.
+The aim of this section is to give a precise formulation of the latter
+and prove it.
 % \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}
 
 %which is equivalent to saying that $X$ is the universal \covering
-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}).$$
+Let $G$ be a group.
+Recall from \cref{def:universalcover} the universal \covering 
+$\uc{\sh_G}:\BG\to\Set: z\mapsto \sh_G\eqto z$, pointed by $\refl{\sh_G}$.
+Since $\uc{\sh_G}(\shape_G)\defequi \USymG$, $\uc{\sh_G}$ restricts to
+a pointed function $\BG\ptdto \BSG_{\USymG}$,
+\marginnote{The letter $\rho$ commemorates the word ``regular''} \ie 
+induces a homomorphism from $G$ to the permutation group $\SG_{\USymG}$,
+denoted by $$\rho_G:\Hom(G,\SG_{\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.
+  $\rho_G:\Hom(G,\SG_{\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
+  $$\bar{\pathsp{}}:\BG=(\typetorsor_G,\princ G)\oldequiv (\conncomp{\Set}{\USymG},\USymG) \MB{typo???}$$ 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
+  $\sum_{E:\conncomp{(\BG\to\Set)}{\uc{\sh_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

intro-uf.tex

@@ -3191,27 +3191,26 @@ \section{Predicates and subtypes}
 \end{corollary}
 In particular, if $T$ is a set, then $T_P$ is again a set;
 we then call $T_P$ a \emph{subset} of $T$ and we may denote it by
-$\setof{t:T}{P(t)}$.\footnote{The full notation of the
+$\setof{t:T}{P(t)}$.\footnote{\label{ft:incl-vs-inj}
+The full notation of this
 subset would be $(\setof{t:T}{P(t)},\fst,p)$, 
 with $p$ witnessing that $\fst$ is an injection.
 In traditional set theory one would call $\fst$ the inclusion
-of the subset, which is unique, and this is what one traditionally wants.
-However, there can be many pairs $(X,i)$ with $i: X\to T$ 
-an injection defining the same subsets of $T$. In set theory
-one has to solve a size issue and define an equivalence relation
-such that equivalent pairs define the same subset. In type theory
+of the subset, which is unique.
+
+In contrast, there can be many pairs $(X,i)$, $i: X\to T$ 
+an injection, defining the same subset of $T$. In set theory
+this approach to subsets would require 
+one to solve a size issue and define an equivalence relation
+such that equivalent pairs define the same subset. In type theory, however,
 we have universes, and the identity type on $\Sub^\UU_T$ identifies
-the triples defining the same subset.}
+precisely the triples defining the same subset.
+
+Such considerations also apply to subtypes, and
+later to subgroups in \cref{def:typeofmono}.}
 \glossary(subset){$\setof{t:T}{P(t)}$}{set comprehension}
 \index{set!comprehension}
 
-It is important to distinguish between $T_P$ as a sum type
-and the triple $(T_P,\fst,p)$, with $p$ witnessing that $\fst$
-is an injection. The latter triple is of type $\Sub_T$,
-whereas $T_P$ as a sum type is an element of some universe.
-It will always be clear from the context which one we mean
-when we use the denotation $T_P$.
-
 \begin{xca}\label{xca:subsets-inclusion}
   Let $T$ be a set, and $S_0$ and $S_1$ be subsets of $T$ with respective
   inclusions $\fst_0 : S_0 \to T$ and $\fst_1 : S_1 \to T$. Prove that the type%