From 3798fde9db99db1646c20887688651c49e3b65fc Mon Sep 17 00:00:00 2001 From: marcbezem Date: Wed, 30 Oct 2024 16:57:17 +0100 Subject: [PATCH] new lem:E-preserves-symms --- actions.tex | 89 +++++++++++++++++++++++++++++++++++----------------- intro-uf.tex | 27 ++++++++-------- 2 files changed, 74 insertions(+), 42 deletions(-) diff --git a/actions.tex b/actions.tex index 499f467..da11aa9 100644 --- a/actions.tex +++ b/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,24 +842,33 @@ \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 @@ -843,7 +876,7 @@ \subsection{Subgroups as monomorphisms} 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 diff --git a/intro-uf.tex b/intro-uf.tex index 6dd9f4d..1467625 100644 --- a/intro-uf.tex +++ b/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%