intro.tex

%% introduction to the book
\label{ch:intro}

\begin{quote}
  \itshape Poincar\'e sagte gelegentlich,
  dass alle Mathematik eine Gruppengeschichte war.
  Ich erz\"ahlte ihm dann \"uber dein Programm,
  das er nicht kannte.

  \smallskip

  \noindent Poincar\'e said casually
  that all of mathematics was a tale about groups.
  I then told him about your program,
  which he didn't know about.
\end{quote}
\hfill (Letter from Sophus Lie to Felix Klein, October 1882)

\bigskip

%{\em If this book is about group theory, then here we will explain what's interesting about groups and why one would want to study them.}

This book is about symmetry and its many manifestations in mathematics.
There are many kinds of symmetry and many ways of studying it.
Euclidean plane geometry is the study of properties that are invariant under rigid motions of the plane.
Other kinds of geometry arise by considering other notions of transformation.
Univalent mathematics gives another perspective.
Motions of the plane are a form of identifying the plane with itself.
It may also be useful to consider different planes
(for instance embedded in a common three-dimensional space)
and different identifications between them.
For instance, when drawing images in perspective
we identify planes in the scene with the image plane,
but not in a rigid Euclidean way, but
rather via a perspectivity (see Fig.~?).
This gives rise to projective geometry.

Does that mean that a plane from the point of view of Euclidean
geometry is not the same as a plane from the point of view of
projective or affine geometry?
Yes.
These are of different types,
because they have different notions of identification,
and thus they have different properties.

TODO: discussion about symmetries as identifications in univalent math.

Propositions, sets, and $1$-types (groupoids).

Group theory emerge from many different directions in the latter half of the 19'th century.
Lagrange initiated the study of the invariants under permutations
of the roots of a polynomial equation $f(x)=0$,
which culminated in the celebrated work of Abel and Galois.
In number theory, Gauss had made detailed studies of modular arithmetic,
proving for instance that the group of units of $\ZZ/p\ZZ$ is cyclic.
Klein was bringing order to geometry by considering groups of transformation,
while Lie was applying group theory in analysis to the study of differential equations.

Galois was the first to use the word ``group'' in a technical sense,
speaking of collections of permutations closed under composition.
He realized that the existence of resolvent equation is equivalent
to the existence of a normal subgroup of prime index
in the group of the equation.

Groupoids vs groups.
The type of all squares in a euclidean plane form a groupoid.
It is connected,
because between any two there exist identifications between them.
But there is no canonical identification.

When we say ``the symmetry group of the square'',
we can mean two things:
1) the symmetry group of a particular square;
this is indeed a group,
or 2) the connected groupoid of all squares;
this is a ``group up to conjugation''.

Vector spaces. Constructions and fields. Descartes and cartesian geometry.

Klein's EP:
\begin{quote}
  Given a manifold and a transformation group acting on it,
  to investigate those properties of figures on that manifold
  that are invariant under transformations of that group.
\end{quote}
and
\begin{quote}
  Given a manifold, and a transformation group acting on it,
  to study its \emph{invariants}.
\end{quote}
Invariant theory had previously been introduced in algebra
and studied by Clesch and Jordan.

(Mention continuity, differentiability, analyticity and Hilbert's 5th problem?)

Any finite automorphism group of the Riemann sphere is conjugate to a
rotation group (automorphism group of the Euclidean sphere).
[Dependency: diagonalizability] (Any complex representation of a
finite group is conjugate to a unitary representation.)

% Groups up to conjugation: $\Gal(\bar\Q/Q)$?

All of mathematics is a tale, not about groups,
but about $\infty$-groupoids.
However, a lot of the action happens already with groups.

\newpage

\section*{Glossary of coercions}

MOVE TO BETTER PLACE
Throughout this book we will use the following coercions to make the text more readable.
\begin{itemize}[noitemsep]
\item If $X$ is the pointed type $(A,a)$, then $x:X$ means $x:A$.
\item On hold, lacking context: If $p$ and $q$ are paths, then $(p,q)$ means $(p,q)^=$.
\item If $e$ is a pair of a function and a proof, we also use $e$ for the function.
\item If $e$ is an equivalence between types $A$ and $B$, we use $\etop e$ for the
identification of $A$ and $B$ induced by univalence.
\item If $p: A= B$ with $A$ and $B$ types, then we use $\ptoe p$ for the canonical
equivalence from $A$ to $B$ (also only as function).
%\item If $G$ is the group $(A,a,p,q)$, then $g:G$ means $g: a=_A a$. %TODO: El
\item If $X$ is $(A,a,\ldots)$ with $a:A$, then $\pt_X$ and even just $\pt$ mean $a$. 
\end{itemize}

\bigskip

\section*{Acknowledgement.}
The authors acknowledge the support of the Centre for Advanced Study (CAS)
at the Norwegian Academy of Science and Letters
in Oslo, Norway, which funded and hosted the research project Homotopy  
Type Theory and Univalent Foundations during the academic year 2018/19.



%%% Local Variables:
%%% mode: latex
%%% fill-column: 144
%%% TeX-master: "book"
%%% End: