EuclideanGeometry.tex

%% \section{euclidean frames, relation to determinants(?)}
%% \section{the euclidean group as a semidirect product}
%% \section{euclidean properties (length, angle, etc.)}


In this chapter we study Euclidean geometry.  We assume some standard linear
algebra over real numbers, including the notion of finite dimensional vector
space over the real numbers and the notion of inner product.  In our context,
the field of real numbers, $\RR$, is a set, and so are vector spaces over it.
Moreover, a vector space $V$ has an underlying additive abstract group, and we
will feel free to pass from it to the corresponding group.

\section{Inner product spaces}

\begin{definition}\label{def:InnerProductSpace}
  An {\em inner product space} $V$ is a real vector space of finite dimension
  equipped with an inner product $H : (V \times V) \to \RR $.
\end{definition}

Let $\OS$ denote the type of inner product spaces.  It is a type of pairs whose
elements are of the form $(V,H)$.

For each natural number $n$, we may construct the {\em standard} inner product
space $\VV^n \defeq (V,H)$ of dimension $n$ as follows.  For $V$ we take the
vector space $\RR^n$, and we equip it with the standard inner product given by
the dot product
$$ H ( x , y) \defeq x \cdot y, $$
where the dot product is defined as usual as
$$ x \cdot y \defeq \sum_i x_i y_i . $$

\begin{theorem}\label{thm:GramSchmidt}
  Any inner product space $V$ is merely equal to $\VV^n$, where $n$ is $\dim V$.
\end{theorem}

For the definition of the adverb ``merely'', refer to \cref{def:merely}.

\begin{proof}
  Since any finite dimensional vector space merely has a basis, we may assume
  we have a basis for $V$.  Now use Gram-Schmidt orthonormalization to show
  that $V = \VV^n$.
\end{proof}

\begin{lemma}\label{lem:InnerProductSpace1Type}
  The type $\OS$ is a $1$-type.
\end{lemma}

\begin{proof}
  Given two inner product spaces $V$ and $V'$, we must show that the type
  $V=V'$ is a set.  By univalence, its elements correspond to the linear
  isomorphisms $f : V \xrightarrow \weq V'$ that are compatible with the
  inner products.  Those form a set.
\end{proof}

\begin{definition}\label{def:OrthogonalGroup}
  Given a natural number $n$, we define the {\em orthogonal group} $\OrthGp n$
  by letting $\B (\OrthGp n)$ be the connected component of $\OS$ containing
  the point $\VV^n$ and equipping it with the proof that it is a connected
  groupoid provided by \cref{thm:GramSchmidt} and
  \cref{lem:InnerProductSpace1Type}.
\end{definition}

We may also omit the parentheses and write $\B\OrthGp n$.
From \cref{thm:GramSchmidt}, we see that $\OS$ is equivalent to $\sum_n \B \OrthGp n$.

Let $\typeRealVectorSpace$ denote the type of finite dimensional real vector spaces.

\begin{definition}\label{def:OrthogonalGroupStandardAction}
  The {\em standard action} of $\OrthGp n$ on the inner product space $\VV^n$ is given
  by the inclusion $\B \OrthGp n \to \OS$.
  (The basepoint of $\B \OrthGp n$ is $\VV^n$.)

  The {\em standard action} of $\OrthGp n$ on the vector space $\RR^n$ is given
  by the function of type $\B \OrthGp n \to \typeRealVectorSpace$ given by
  $(V,H) \mapsto V$.
  (The basepoint of $\B \OrthGp n$ maps to $\RR^n$.)

  The {\em standard action} of $\OrthGp n$ on the underlying additive group of $\RR^n$ is given
  by the function of type $\B \OrthGp n \to \typegroup$ that sends
  $(V,H)$ to the underlying additive group of $V$.
  (The basepoint of $\B \OrthGp n$ maps to the underlying additive group of $\RR^n$.)
\end{definition}
  
\section{Euclidean spaces}

\begin{definition}\label{def:EuclideanSpace}
  A {\em Euclidean space} $E$ is a torsor $A$ for the additive group
  underlying an inner product space $V$.
\end{definition}

We will write $V$ also for the additive group underlying $V$.  Thus an
expression such as $\B V$ or $\typetorsor_V$ will be understood as applying to
the underlying additive group\footnote{We are careful not to refer to the group
  as an Abelian group at this point, even though it is one, because the
  operator $\B$ may be used in some contexts to denote a different construction
  on Abelian groups.}
of $V$.

We denote the type of all Euclidean spaces by $\ES \defeq \sum_{V:\OS} \typetorsor_V$.
For a pair $E = (V,A) : \ES$, we introduce the notation $\Vectors E \defeq V$ and $\Points E \defeq A$.

For $E:\ES$, we let $P:E$ serve as notation for $P:\Points E$.  These will be
the {\em points} in the geometry of $E$.

The torsor $\Points E$ is a nonempty set upon which $V$ acts.  Since $V$ is an
additive group, we prefer to write the action additively, too: given $v:V$ and
$P:E$ the action provides an element $v+P:E$.  Moreover, given $P,Q:E$, there
is a unique $v:V$ such $v+P = Q$; for it we introduce the notation $Q-P \defeq
v$, in terms of which we have the identity $(Q-P)+P=Q$.

For each natural number $n$, we may construct the {\em standard} Euclidean
space $\EE^n : \ES$ of dimension $n$ as follows.  For $\Vectors E$ we take the
standard inner product space $\VV^n$, and for $\Points E$ we take the
corresponding principal torsor $\princ {\RR^n}$.

\begin{theorem}\label{thm:EuclideanNormalization}
  Any Euclidean space $E$ is merely equal to $\EE^n$, where $n$ is $\dim E$.
\end{theorem}

\begin{proof}
  Since we are proving a proposition and any torsor is merely trivial, by
  \cref{thm:GramSchmidt} we may assume $\Vectors E$ is $\VV^n$.  Similarly, we
  may assume that $\Points E$ is the trivial torsor.
\end{proof}

\begin{lemma}\label{lem:EuclideanSpace1Type}
  The type $\ES$ is a $1$-type.
\end{lemma}

\begin{proof}
  Observe using \cref{lem:BGbytorsor} that
  $\ES \weq \sum_n \sum_{V:\B \OrthGp n} \B V$ and that the
  types $\B \OrthGp n$ and $\B V$ are 1-types.
\end{proof}

\begin{definition}\label{def:EuclideanGroup}
  Given a natural number $n$, we define the {\em Euclidean group} $\EucGp n$ by
  letting $\B \EucGp n$ be the connected component of $\ES$ containing the
  point $\EE^n$ and equipping it with the proof that it is a connected
  groupoid provided by \cref{thm:EuclideanNormalization} and
  \cref{lem:EuclideanSpace1Type}.
\end{definition}

We see that $\ES$ is equivalent to the sum $\sum_n \B \EucGp n$.

\begin{definition}\label{def:EuclideanGroupStandardAction}
  The {\em standard action} of $\EucGp n$ on the Euclidean space $\EE^n$ is given
  by the inclusion $\B \EucGp n \to \ES$.
\end{definition}

\begin{theorem}\label{thm:EuclideanGroupSemidirect}
  For each $n$, the Euclidean group $\EucGp n$ is equivalent to a semidirect
  product $\OrthGp n \ltimes \RR^n$.
\end{theorem}

\begin{proof}
  Recall \cref{def:semidirect-product} and apply it to the standard action
  $\tilde H : \B \OrthGp n \to \typegroup$ of $\OrthGp n$ on the additive group
  underlying $\RR^n$, as defined in \cref{def:OrthogonalGroupStandardAction}.
  The semidirect product $\OrthGp n \ltimes \RR^n$ has
  $\sum_{V:\B \OrthGp n} \B V$ as its underlying pointed type.
  Finally, observe that $\EucGp n \weq \sum_{V:\B \OrthGp n} \B V$, again
  using \cref{lem:BGbytorsor}.
\end{proof}