further polish intro

intro.tex

@@ -24,7 +24,7 @@ \chapter{Introduction to the topic of this book}
 
 Since this book is called ``Symmetry'' it is reasonable to hope
 that by the time you've reached the end you'll have a clear idea of
-what ``symmetry'' means.
+what symmetry means.
 
 Ideally the answer should give a solid foundation for dealing with
 questions about symmetries. It should also equip you with language
@@ -33,8 +33,7 @@ \chapter{Introduction to the topic of this book}
 
 So, we should start by talking about how one intuitively can approach the
 subject while giving hints about how this intuition can be made into
-the solid, workable tool, 
-which is the topic \MB{goal, aim, purpose?} of this book.
+the solid, workable tool, which is the topic of this book.
 
 \sususe{What is symmetry?}
 
@@ -51,7 +50,12 @@ \chapter{Introduction to the topic of this book}
 \begin{enumerate}
 \item
   are these \emph{all} the symmetries?
-\item ``rotation'' indicates a \emph{motion}, through different squares, joining $\square$ with itself via a ``journey in the world of squares''.
+\item ``rotation'' indicates a \emph{motion}, through different squares,
+joining $\square$ with itself via a ``journey in the world of squares''.
+
+The following cartoon animates a rotation of $\square$ by $90$\textdegree.
+The center of the square should be thought of as being in the same place
+all the time.
 \end{enumerate}
 \begin{center}
   \begin{tikzpicture}
@@ -88,14 +92,13 @@ \chapter{Introduction to the topic of this book}
   \end{tikzpicture}
 \end{center}
 How is that reconcilable with a precise notion of symmetry?
-\MB{Clarify rotation versus rolling. ?Practical example:
-car wheel with four bolts. Reflections are naturally absent.}
 
 The answer to the first question clearly depends on the context. 
-For example, if we allow reflections \MB{leave out?: or even more exotic symmetries} the answer is ``no''.  Each context has its own answer to what the symmetries of the square are.
+For example, if we allow reflections the answer is ``no''.
+Each context has its own answer to what the symmetries of the square are.
 
 Actually, the two questions should be seen as connected. 
-If a symmetry of $\square$ is like a \MB{roundtrip?} journey (loop) 
+If a symmetry of $\square$ is like a round trip (loop) 
 in the world (type) of squares, what symmetries are allowed is 
 dependent on how big a ``world of squares'' we consider. 
 Is it, for instance, big enough to contain a loop representing a reflection?
@@ -108,25 +111,24 @@ \chapter{Introduction to the topic of this book}
 It is (almost) that simple!
 
 Note that this presupposes that our setup is strong enough to support the
-notion of a ``loop'', \MB{I prefer roundtrip here, and to postpone:}
-which in the \MB{objection YH:} real world perhaps could be envisioned as a continuous path starting and ending at the same place.
+notion of a round trip.
 
 \sususe{From ``things'' to mathematical objects}
 
 Different setups have different advantages.
 The theory of sets is an absolutely wonderful setup, but supporting the
-notion of a roundtrip in sets requires at the very least developing fields
-like \MB{why quotes here and in the next sentence?}``topology'' and ``homotopy theory'', 
+notion of a round trip in sets requires at the very least developing fields
+like \emph{mathematical analysis}, \emph{topology} and \emph{homotopy theory},
 which (while fun and worthwhile in itself) is something of a detour.
 
-The setup we adopt, ``HoTT'' or ``univalent foundations'', 
-seems custom-built for supporting the notion of a roundtrip of
-a thing $x$ in a type $X$. \MB{Some glue preparing for groups:}
-In addition we get support for important operations on roundtrips
-of $x$: one can do such roundtrips after another (composition),
-one can go any roundtrip in the reversed direction (inverse), and there
-is always the trivial roundtrip of staying in place (unit).
-This provides roundtrips with a structure that is called a group
+The setup we adopt, homotopy type theory, or univalent foundations, 
+seems custom-built for supporting the notion of a round trip of
+a thing $x$ in a type $X$. 
+We get support for important operations on round trips
+of $x$: one can do such round trips after another (composition),
+one can go any round trip in the reversed direction (inverse), and there
+is always the trivial round trip of staying in place (unit).
+This provides round trips with a structure that is called a \emph{group}
 in mathematics, satisfying all the properties that these operations
 ought to have. 
 
@@ -175,7 +177,7 @@ \chapter{Introduction to the topic of this book}
   \end{scope}
 \end{tikzpicture}
 \end{center}
-While such comparisons of symmetries are traditionally handled by something called a ``group homomorphism'' which is a function satisfying a rather long list of axioms, in our setup the only thing we need to know of the function is that it really does take thing 1 to thing 2 -- everything else then follows naturally.
+While such comparisons of symmetries are traditionally handled by something called a \emph{group homomorphism} which is a function satisfying a rather long list of axioms, in our setup the only thing we need to know of the function is that it really does take thing~1 to thing~2 -- everything else then follows naturally.
 
 Some important examples have provocatively simple representations in
 this framework.  For instance, consider the circle shown in the margin,
@@ -184,9 +186,9 @@ \chapter{Introduction to the topic of this book}
     \node[dot,label=right:$x$] (base) at (1,0) {};
     \draw (0,0) circle (1);
   \end{tikzpicture}}
-Since symmetries of $x$ are interpreted as loops, you see that you have a loop for every integer -- the number $7$ can be represented by looping seven times counterclockwise.  As we shall see, in our setup any loop \MB{?in the circle} is naturally identified with a unique integer (the ``winding number'' if you will).  Everything you can wish to know about the structure of the ``group of integers'' is encoded\MB{?better verb} in the circle.
+Since symmetries of $x$ are interpreted as loops, you see that you have a loop for every integer -- the number $7$ can be represented by looping seven times counterclockwise.  As we shall see, in our setup any loop in the circle is naturally identified with a unique integer (the \emph{winding number} if you will).  Everything you can wish to know about the structure of the \emph{group of integers} is built-in in the circle.
 
-Another example is the ``free group of words in two letters $a$ and $b$''.  This is represented by the figure eight in the margin.\marginnote{%
+Another example is the \emph{free group of words in two letters $a$ and $b$}.  This is represented by the figure eight in the margin.\marginnote{%
   \begin{tikzpicture}
     \node[dot,label=right:$x$] (base) at (1,0) {};
     \draw (0,0) circle (1);
@@ -196,7 +198,7 @@ \chapter{Introduction to the topic of this book}
   \end{tikzpicture}}
 In order to be able to distinguish the two circles we call them $a$ and $b$,
 with the point $x$ as the (only) point on both.
-The word $ab^2a^{-1}$ is represented by looping around circles $a$ and $b$ respectively $1$, $2$ and $-1$ times in succession -- notice that since the $b^2$ is in the middle it prevents the $a$ and the $a^{-1}$ from meeting and cancelling each other out.  If you wanted the ``\emph{abelian} group on the letters $a$ and $b$'' (where $a$ and $b$ are allowed to move past each other), you should instead look at the torus:
+The word $ab^2a^{-1}$ is represented by looping around circles $a$ and $b$ respectively $1$, $2$ and $-1$ times in succession -- notice that since the $b^2$ is in the middle it prevents the $a$ and the $a^{-1}$ from meeting and cancelling each other out.  If you wanted the \emph{abelian} group on the letters $a$ and $b$ (where $a$ and $b$ are allowed to move past each other), you should instead look at the torus:
 \begin{center}
 \begin{tikzpicture}
   \useasboundingbox (-3,-1.5) rectangle (3,1.5);
@@ -223,9 +225,26 @@ \chapter{Introduction to the topic of this book}
 
 \sususe{The importance of the ambient type $X$ ``of things''}
 
-In some situations, the type $X$ ``of things'' can be more difficult to draw,
-let alone to define mathematically.  For instance, what is the ``type of all squares'' which we discussed earlier, representing all rotational symmetries of $\square$?  While it is harder to draw, you have perhaps already visualized it as the type of all squares in the plane, with $\square$ being the shape the loop must start and stop in. \MB{Discuss how to exclude the reflections. Otherwise
-the next sentence is plane (sic) wrong.} In addition, we see that any symmetry can be reached by doing the $90$\textdegree-rotation a few times, together with the fact that taking any loop four times reduces to not doing anything at all: it represents the ``cyclic group of order four''.
+In many situations, the type $X$ ``of things'' can be more difficult to draw,
+or to define mathematically.  For instance, what is the ``type of all squares'' which we discussed earlier, representing all rotational symmetries of $\square$?  You have perhaps already visualized it as the type of all squares in the plane, with $\square$ being the shape the loop must start and stop in. This idea works well for the \emph{oriented square} depicted\marginnote{%
+\begin{tikzpicture}
+\draw[->] (0,0) -- (0,1);
+\draw[->] (0,1) -- (1,1);
+\draw[->] (1,1) -- (1,0);
+\draw[->] (1,0) -- (0,0);
+\end{tikzpicture}
+}
+in the margin. Note that the only reflective symmetry of the oriented
+square is reflection in the center -- and the outcome is the same
+as a rotation by $180$\textdegree. However, for $\square$ we would get
+reflective symmetries that are not rotations.
+It is actually a little difficult to come
+up with a simple geometry of the plane that gives exactly the rotational
+symmetries of $\square$. Later in the book, we will first pursue an
+algebraic approach, using that any rotational symmetry of $\square$
+can be reached by doing the $90$\textdegree-rotation a few times, 
+together with the fact that taking any loop four times reduces to not doing
+anything at all: they represent the \emph{cyclic group of order four}.
 
 A by-product of this line of thinking is the distinguished position of the circle. To express this it is convenient to give names to things: let $\base$ be the chosen base point in the circle and $\Sloop$ the loop winding once around the circle counterclockwise. Then a symmetry of a shape $x_0$ in $X$ is uniquely given by the image of $\Sloop $ under a function $\Sc\to X$ taking $\base$ to $x_0$. So,
 \begin{quote}