Merge branch 'master' of github.com:UniMath/SymmetryBook

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,76 +403,113 @@ \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
    two circles with a common base point. }
   \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$.
 

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);

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);