diff --git a/actions.tex b/actions.tex index 7daef21..f78ed9d 100644 --- a/actions.tex +++ b/actions.tex @@ -80,7 +80,8 @@ \section{Group actions ($G$-sets)} if $G$ is (a group or) an infinity group, a \emph{$G$-type} is a function $X : \BG\to\UU$, with \emph{underlying type} $X(\sh_G)$. - More generally, an action of $G$ on an element of type $A$ + This is an \emph{action in $\UU$}, and + more generally, an action of $G$ on an element of type $A$ is a function $X : \BG\to A$, see~\cref{sec:actions} below.} \begin{example}\label{def:trivGset} @@ -229,14 +230,14 @@ \section{Group actions ($G$-sets)} $x:X(z)$, $g:z\eqto w$. In other words, the following diagram commutes: \[ \begin{tikzcd} - z\ar[d,eqr,"g"] &X(z) \ar[r,"f_z"] \ar[d,eql,"X(g)"'] - &Y(z) \ar[d,eqr,"Y(g)"] \\ + z\ar[d,eql,"g"'] &X(z) \ar[r,"f_z"] \ar[d,eql,"g\cdot_X\blank"'] + &Y(z) \ar[d,eqr,"g\cdot_Y\blank"] \\ w &X(w) \ar[r,"f_w"'] & Y(w) \end{tikzcd} \] An important special case is when $Y$ is the $G$-set that is constant $\Prop$: Given a map $P$ from $X$ to $\triv_G\Prop$, -we have $P_w(g\cdot x)$ iff $g\cdot P_z(x)$ +we have $P_w(g\cdot x)$ if and only if $g\cdot P_z(x)$ for all $z,w:\BG$, $x:X(z)$, $g:z\eqto w$. This applies to the following definition. \end{remark} @@ -294,6 +295,15 @@ \section{Group actions ($G$-sets)} \] \end{remark} +\begin{definition}\label{def:Gaction} + If $G$ is a group and $X$ is a set, then an \emph{action} + of $G$ on $X$ + is a homomorphism from $G$ to the permutation group of $\SG_X$ of $X$.% + \index{actions!of a group on a set} +\end{definition} +By the construction in~\cref{remark:GsetsareGsets} we identify $G$-sets +and sets with an action of $G$ on a set. + \begin{xca} Show that if $X$ is a type family with parameter type $\BG$ and $X(\sh_G)$ is a set, then $X$ is a $G$-set. @@ -362,15 +372,16 @@ \subsection{Transitive $G$-sets} 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. -\Cref{fig:not-normal} illustrates what can go wrong. +The action in \cref{fig:not-normal,fig:not-normal-graph} +illustrates what can go wrong. We'll study exactly when we get surjectivity in~\cref{sec:normal} on ``normal'' subgroups. \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) {}; + \coordinate (two) at (0, 10); + \coordinate (one) at (0, 6); + \coordinate (zero) at (0, 2); + \coordinate (base) at (0,-5); \pgfmathsetmacro\cc{.55228475}% = 4/3*tan(pi/8) \pgfmathsetmacro\cy{2*\cc}% @@ -380,7 +391,7 @@ \subsection{Transitive $G$-sets} \pgfmathsetmacro\ay{.35165954}% % right 3-cycle - \draw (zero.center) .. controls ++(0,-\cy+\ay) and ++(-\cx,-\ay) + \draw[casblue] (zero) .. controls ++(0,-\cy+\ay) and ++(-\cx,-\ay) .. (10,1) .. controls ++(\cx,+\ay) and ++(0,-\cy-\ay) .. (20,4) \foreach \y in {4,8} { @@ -392,38 +403,44 @@ \subsection{Transitive $G$-sets} .. 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); + .. (zero); % left 2-cycle - \draw (one.center) .. controls ++(0,-\cy+\ay) and ++(\cx,-\ay) + \draw[casred] (one) .. 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) + .. (two) .. 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); + .. (one); % left 1-cycle - \draw (zero.center) .. controls ++(0,\cy) and ++(\cx,0) + \draw[casred] (zero) .. 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); + .. (zero); % base right - \draw (base.center) .. controls (0,-5+\cy) and ++(-\cx,0) + \draw (base) .. 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); + .. (10,-7) .. controls ++(-\cx,0) and ++(0,-\cy) .. (base); % base left - \draw (base.center) .. controls (0,-5 + \cy) and (-10+\cx,-3) + \draw (base) .. 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); + .. (base); + + % draw dots last + \node[dot,label=above:$x$] (ntwo) at (two) {}; + \node[dot] (none) at (one) {}; + \node[dot] (nzero) at (zero) {}; + \node[dot] (nbase) at (base) {}; \end{tikzpicture} \caption{A $\mkgroup(\Sc\vee\Sc)$-set for which $\protect\ev_x$ is not surjective. At the bottom the type $\Sc\vee\Sc$ is visualized as @@ -431,37 +448,68 @@ \subsection{Transitive $G$-sets} \label{fig:not-normal} \end{marginfigure} +\begin{marginfigure} + \noindent\begin{tikzpicture} + \pgfmathsetmacro{\len}{1} + \node[vertex,label=above:$x$] (n1) at (0:\len) {}; + \node[vertex] (n2) at (120:\len) {}; + \node[vertex] (n3) at (240:\len) {}; + \begin{scope}[every to/.style={bend right=22}] + % generator a + \draw[gena] (n1) to (n2); + \draw[gena] (n2) to (n3); + \draw[gena] (n3) to (n1); + \end{scope} + % generator b + \draw[genb] (n1) to[out=-30,in=30,looseness=25] (n1); + \draw[genb,out=205,in=155] (n2) to (n3); + \draw[genb,out=45,in=-45] (n3) to (n2); + \end{tikzpicture} + \caption{Alternative representation of the $\mkgroup(\Sc\vee\Sc)$-set + from~\cref{fig:not-normal}, + using colors and arrows to represent which + parts lies over which circle in which orientation.} + \label{fig:not-normal-graph} +\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 + Let $X,Y:\BG\to\Set$ be $G$-sets. Let $z:\BG$ and $x:X(z)$. + If $X$ is transitive, then the evaluation map \[ - \ev_x:(X \eqto X')\to X'(z),\qquad \ev_x(f)\defequi f_z(x) + \ev_x:\Hom_G(X, Y)\to Y(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$.} + Recall that for type families $X,Y:T\to\UU$, and + $f:\prod_{z:T}(X(z)\to Y(z))$, we may write $f_z:(X(z)\to Y(z))$ + (instead of the more correct $f(z)$) for its evaluation at $z:T$.} \end{lemma} \begin{proof} - In view of function extensionality, our claim is that the evaluation - map $\ev_x:(\prod_{s:\BG}(X(s)\eqto X'(s)))\to X'(z)$ given by the - same formula is injective; that is all $f$s with the same - value $f_z(x)$ are identical. - - Fix a value $a:X'(z)$, and consider an $f:X\eqto X'$ with $f_z(x)=a$. - We will show that $f$ is uniquely determined by $f_z(x)=a$. - Let $s:\BG$ and $y:X(s)$. It suffices to show that the value - of $f_s(y)$ is independent of $f$. - For any $g:z=s$ such that $g\cdot_X x=y$ (which exists by the - transitivity of $X$, using \cref{lem:conistrans}) we have - $f_s(y)=f_s(g\cdot_X x)=g \cdot_{X'} f_z(x)=g \cdot_{X'} a$, - and the latter value does indeed not depend on $f$. - Since we try to prove a proposition we are done. + Fix a value $y:Y(z)$, and consider an $f:\Hom_G(X,Y)$ with $f_z(x)=y$. + We will show that $f$ is uniquely determined by this. + Let $w:\BG$ and $x':X(w)$. It suffices to show that the value + of $f_w(x')$ is independent of $f$. + For any $g:z\eqto w$ such that $g\cdot_X x=x'$ + (which exists by the transitivity of $X$, using \cref{lem:conistrans}) + we have + \[ + f_w(x')=f_w(g\cdot_X x)=g \cdot_Y f_z(x)=g \cdot_Y y, + \] + using~\cref{rem:map-of-Gsets}, + and the latter value indeed doesn't depend on $f$. + Since we're proving a proposition, we are done. \end{proof} +Via function extensionality, +the identity type $X \eqto Y$, for $G$-sets $X,Y$ +is a subtype of the type $\Hom_G(X,Y)$. +Hence we likewise have that evaluation at some $x:X(z)$ is an +injection +\[ + \ev_x:(X \eqto Y)\to Y(z). +\] \begin{xca}\label{xca:not-normal} -Reverse engineer the $\mkgroup(\Sc\vee\Sc)$-set in \cref{fig:not-normal}. +Reverse engineer the $\mkgroup(\Sc\vee\Sc)$-set in \cref{fig:not-normal,fig:not-normal-graph}. Let's call it $X$. Show that $X\eqto X$ is contractible. Conclude that $\ev_x$ cannot be surjective. (Hint: the induction principle for $\Sc\vee\Sc$ is a generalization @@ -474,24 +522,90 @@ \subsection{Actions in a type} \begin{definition}\label{action} If $G$ is any group\footnote{% - Even an $\infty$-group in the sense of \cref{sec:inftygps}.} + Even an $\infty$-group in the sense of \cref{sec:inftygps}.} 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 + then we define an \emph{action of $G$ in $A$} as a function \[ - X : \BG \to A.\qedhere + X : \BG \to A. \] + The particular object of type $A$ being acted on is $X(\sh_G):A$, + the \emph{underlying object}, + and the action itself is given by transport.% + \index{action!of a group in a type} + + Fixing $a:A$ as the underlying object, we define an \emph{action of $G$ on $a$} + to be a homomorphism from $G$ to $\Aut_A(a)$.% + \index{action!of a group on an element} \end{definition} - -The particular object of type $A$ being acted on is $X(\sh_G):A$, -and the action itself is given by transport. -This generalizes our earlier definition of $G$-sets, $X : \BG \to \Set$. +This generalizes our earlier definition of $G$-sets +from~\cref{def:Gset}, $X : \BG \to \Set$, +and harmonizes with~\cref{remark:GsetsareGsets}, relating $G$-sets and +actions of $G$ on a set. +Indeed, we identify +an action of $G$ in $A$ with a pair of an underlying object +$a:A$ and an action of $G$ on $a$: +\[ + (\BG \to A) \equivto \sum_{a:A}\Hom(G,\Aut_A(a)) +\] +This equivalence maps an action $X:\BG\to A$ +to the pair consisting of $a \defeq X(\sh_G)$ +and the homomorphism represented by the pointed map +from $\BG$ to the pointed component $\conncomp A a$ given by $X$. \begin{definition}\label{std-action} The \emph{standard action} of $G$ on its designated shape $\sh_G$ is obtained by taking $A \defeq \BG$ and $X \defeq \id_{\BG}$. \end{definition} +\begin{example}\label{ex:S2-acts-on-C3} + The symmetric group $\SG_2$ acts on the cyclic group $\CG_3$ as follows. + Given a $2$-element set $S$ consider the + type $\sum_{X:\Set}S \to X\to X$ of pairs $(X,f)$ of a set $X$ + and a ``pair'' of functions $f_s:X\to X$ (one for each $s:S$). + Within this type we have the pair $(\bn 1 \amalg S,f)$, + where + \begin{align*} + f_s(\inl 0) &\defeq \inr s,\\ + f_s(\inr s) &\defeq \inr{\swap(s)},\\ + f_s(\inr{\swap(s)}) &\defeq \inl 0. + \end{align*} + Then $G(S) \defeq \Aut_{\sum_{X:\Set}S\to X\to X}(\bn1\amalg S,f)$ defines an action + $\BSG_2 \to \Group$.\footnote{% + If $S$ is $\set{s,s'}$, then we can picture the + designated shape as follows, + where the blue and red arrows denote $f_s$ and $f_{s'}$, + respectively:\par + \begin{tikzpicture} + \draw (-.1,1) ellipse (.35 and .35); + \node (X) at (0,1.5) {$\bn 1$}; + \draw (1,1) ellipse (.4 and 1); + \node (Y) at (.9,2.2) {$S$}; + \node[dot,label=left:$0$] (x) at (0,1) {}; + \node[dot,label=above:$s$] (s1) at (1,1.5) {}; + \node[dot,label=below:$s'$] (s2) at (1,.5) {}; + \draw[dashed] (0.6,1.1) ellipse (1.2 and 1.6); + \begin{scope}[every to/.style={bend left=30}] + % generator a + \draw[gena] (x) to (s1); + \draw[gena] (s1) to (s2); + \draw[gena] (s2) to (x); + \end{scope} + % generator b + \draw[genb] (x) to (s2); + \draw[genb] (s2) to (s1); + \draw[genb] (s1) to (x); + \node (XY) at (-0.75,2.35) {$\bn1\amalg S$}; + \end{tikzpicture}} + Furthermore, we identify $G(\bool)$ with $\BCG_3$ by mapping + a shape $(X,f)$ in $\BG(\bool)$ to the $3$-cycle $(X,f_\yes)$ + and identifying the $3$-cycle $(\bn1\amalg\bool,f_\yes)$, for the $f$ defined above, + with the standard $3$-cycle $(\bn3,\zs)$, correlating $\inl 0$ with $0:\bn 3$. +\end{example} +\begin{xca}\label{xca:AutC3} + Show that action of $\SG_2$ on $\CG_3$ from~\cref{ex:S2-acts-on-C3} + gives an identification $\SG_2 \eqto \Aut(\CG_3)$. +\end{xca} + \begin{example} By composing constructions we can build new actions starting from simple building blocks. @@ -504,22 +618,6 @@ \subsection{Actions in a type} 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(\sh_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)$. - \section{Subgroups} \label{sec:subgroups} In our discussion of the group $\ZZ\defequi\Aut_{\Sc}(\base)$ of integers @@ -589,7 +687,7 @@ \subsection{Subgroups through $G$-sets} $R(\Sloop) \defis \etop\zs$, see \cref{def:RtoS1}. Again we point by $0: R(\base)$ and transitivity of $R$ is obvious. The only symmetry that keeps $0$ in place is $\refl{\base}$, -since $R(\Sloop)= \zs$ iff $k=0$. +since $R(\Sloop)= \zs$ if and only if $k=0$. Again, no surprise in view of the results in \cref{sec:symcirc} identifying $R$ as the universal \covering over $\Sc$. diff --git a/fggroups.tex b/fggroups.tex index dbb3e36..a8a92f7 100644 --- a/fggroups.tex +++ b/fggroups.tex @@ -174,11 +174,6 @@ \section{Graphs and Cayley graphs} In this case, then, $G$ can be identified with the automorphism group of $\rho_S(\sh_G)$ in the type $\sum_{X:\UU}(S \to X \to X)$, or even in the larger type (of which it's a subtype), $\sum_{X:\UU}(S \to X \to X \to \UU)$. - -\tikzset{vertex/.style={circle,fill=black,inner sep=0pt,minimum size=4pt}} -\tikzset{gena/.style={draw=casblue,-stealth}} -\tikzset{genb/.style={draw=casred,-stealth}} - \begin{figure} \begin{sidecaption}% {Cayley graph for {$\protect\SG_3$} with respect to $S = \{(1\;2),(2\;3)\}$.}[fig:cayley-s3] @@ -191,7 +186,7 @@ \section{Graphs and Cayley graphs} \node[vertex,label=210:$e$] (ne) at (210:\len) {}; \node[vertex,label=270:$(2\;3)$] (n23) at (270:\len) {}; \node[vertex,label=330:$(1\;2\;3)$] (n123) at (330:\len) {}; - \begin{scope}[every to/.style={bend left=22}] + \begin{scope}[every to/.style={bend right=22}] % generator a is (12) \draw[gena] (ne) to (n12); \draw[gena] (n12) to (ne); diff --git a/intro-uf.tex b/intro-uf.tex index a183287..eb72740 100644 --- a/intro-uf.tex +++ b/intro-uf.tex @@ -1796,7 +1796,7 @@ \subsection{Binary sums} \glossary(2amalg){$\amalg$}{sum of two types}$X \amalg Y$, is an inductive type with two constructors: $\inl{} : X \to X \amalg Y$ and $\inr{} : Y \to X \amalg Y$.\footnote{% - Be aware that in a picture, the same point may refer + Beware that in a picture, the same point may refer either to $x$ in $X$ or to $\inl x$ in the sum $X \amalg Y$:\par \begin{tikzpicture} \draw (0,0.9) ellipse (.25 and 1); diff --git a/tikzsetup.tex b/tikzsetup.tex index 21038ec..2c5e685 100644 --- a/tikzsetup.tex +++ b/tikzsetup.tex @@ -109,12 +109,16 @@ } \tikzset{>=pxto,% - mapsto/.style={pxbar-pxto}} + mapsto/.style={pxbar-pxto},% + vertex/.style={circle,fill=black,inner sep=0pt,minimum size=4pt},% + gena/.style={draw=casblue,-stealth},% + genb/.style={draw=casred,-stealth}} + \tikzcdset{arrow style=tikz,% arrows={line width=0.59pt},% invisible/.style={/tikz/draw=none},% - mapsto/.style={pxbar-pxto}} - + mapsto/.style={pxbar-pxto} +} \tikzcdset{ equals/.add code={\PackageError{cas}{Please don't use the TikZ-cd equals style}{}}{} }