diff --git a/sections/introduction.tex b/sections/introduction.tex
@@ -723,14 +723,29 @@ over the ring of \(G\)-invariant differential operators -- i.e.
Proposition~\ref{thm:geometric-realization-of-uni-env} is in fact only the
beginning of a profound connection between the theory of \(D\)-modules and and
-the so called \emph{representations} of Lie algebras. These will be the focus
-of our next section.
-
-\section{Representations}
-
-Let \(\mathfrak{g}\) be a Lie algebra over \(K\). We begin by describing the
-concept of a \(\mathcal{U}(\mathfrak{g})\)-module entirely in terms of
-\(\mathfrak{g}\).
+\emph{representation theory}, which we will explore in the next section.
+
+\section{Representation Theory}
+
+First introduced in 1896 by Georg Frobenius in his paper \citetitle{frobenius}
+\cite{frobenius} in the context of group theory, representation theory is now
+one of the cornerstones of modern mathematics. In this section we provide a
+brief overview of basic concepts of the representation theory of Lie algebras.
+We should stress, however, that the representation theory of Lie algebras is
+only a small fragment of what is today known as representation theory, which is
+in general concerned with a diverse spectrum of algebraic and combinatorial
+structures -- such as groups, quivers and associative algebras.
+
+We begin by noting that any \(\mathcal{U}(\mathfrak{g})\)-module \(V\) may be
+regarded as a \(K\)-vector space endowed with a ``linear action'' of
+\(\mathfrak{g}\). Indeed, by restricting the action map
+\(\mathcal{U}(\mathfrak{g}) \to \operatorname{End}(V)\) to \(\mathfrak{g}\)
+yields a homomorphism of Lie algebras \(\mathfrak{g} \to \mathfrak{gl}(V) =
+\operatorname{End}(V)\). In fact proposition~\ref{thm:universal-env-uni-prop}
+implies that given a vector space \(V\) there is a one-to-one correspondence
+between \(\mathcal{U}(\mathfrak{g})\)-module structures for \(V\) and
+homomorphisms \(\mathfrak{g} \to \mathfrak{gl}(V)\). This leads us to the
+following definition.
\begin{definition}
Given a Lie algebra \(\mathfrak{g}\) over \(K\), \emph{a representation \(V\)
@@ -760,9 +775,9 @@ concept of a \(\mathcal{U}(\mathfrak{g})\)-module entirely in terms of
representation of \(\mathfrak{g}\)}.
\end{example}
-It is usual practice to think of a representation \(V\) of \(\mathfrak{g}\) in
-terms of an action of \(\mathfrak{g}\) in a vector space and write simply \(X
-\cdot v\) or \(X v\) for \(\rho(X) v\). For instance, one might say\dots
+It is usual practice to write simply \(X \cdot v\) or \(X v\) for \(\rho(X)
+v\) when the map \(\rho\) is clear from the context. For instance, one might
+say\dots
\begin{example}\label{ex:sl2-polynomial-rep}
The space \(K[x, y]\) is a representation of \(\mathfrak{sl}_2(K)\) with
@@ -798,8 +813,8 @@ terms of an action of \(\mathfrak{g}\) in a vector space and write simply \(X
respectively.
\end{example}
-Of course, there is a natural notion of \emph{transformations} between
-representations too.
+Of course, there is also a natural notion of \emph{transformations} between
+representations.
\begin{definition}
Given a Lie algebra \(\mathfrak{g}\) and two representations \(V\) and \(W\)
@@ -818,16 +833,10 @@ representations too.
\end{definition}
The collection of representations of a fixed Lie algebra \(\mathfrak{g}\) thus
-forms a category, which we call \(\mathfrak{g}\text{-}\mathbf{Mod}\). As
-promised, representations of \(\mathfrak{g}\) are intimately related to
-\(\mathcal{U}(\mathfrak{g})\)-modules. In fact, given a \(K\)-vector space
-\(V\) proposition~\ref{thm:universal-env-uni-prop} implies there is a
-one-to-one correspondence between homomorphisms of Lie algebras \(\mathfrak{g}
-\to \mathfrak{gl}(V)\) and homomorphisms of algebras
-\(\mathcal{U}(\mathfrak{g}) \to \operatorname{End}(V)\) -- which takes a
-homomorphism \(f : \mathfrak{g} \to \mathfrak{gl}(V)\) to its extension
-\(\mathcal{U}(\mathfrak{g}) \to \operatorname{End}(V) = \mathfrak{gl}(V)\). It
-then follows\dots
+forms a category, which we call \(\mathfrak{g}\text{-}\mathbf{Mod}\). This
+allow us formulate the correspondence between representations of
+\(\mathfrak{g}\) and \(\mathcal{U}(\mathfrak{g})\)-modules in more precise
+terms.
\begin{proposition}
There is a natural equivalence of categories
@@ -836,6 +845,25 @@ then follows\dots
finite-dimensional representations to finitely generated modules.
\end{proposition}
+\begin{proof}
+ We've seen that given a \(K\)-vector space \(V\) there is a one-to-one
+ correspondence between \(\mathfrak{g}\)-module structures for \(V\) -- i.e.
+ homomorphisms \(\mathfrak{g} \to \mathfrak{gl}(V)\) -- and
+ \(\mathcal{U}(\mathfrak{g})\)-module structures for \(V\) -- i.e.
+ homomorphisms \(\mathcal{U}(\mathfrak{g}) \to \operatorname{End}(V)\). This
+ gives us a map that takes objects in \(\mathfrak{g}\text{-}\mathbf{Mod}\) to
+ objects in \(\mathcal{U}(\mathfrak{g})\text{-}\mathbf{Mod}\). This map
+ preserves the dimension of the representations, so it takes
+ finite-dimensional representations to finately generated modules.
+
+ As for the corresponding maps \(\operatorname{Hom}_{\mathfrak{g}}(V, W) \to
+ \operatorname{Hom}_{\mathcal{U}(\mathfrak{g})}(V, W)\), it suffices to note
+ that a \(K\)-linear map between representations \(V\) and \(W\) is an
+ intertwiner if, and only if it is a homomorphism of
+ \(\mathcal{U}(\mathfrak{g})\)-modules. Our functor thus takes an intertwiner
+ \(V \to W\) to itself.
+\end{proof}
+
\begin{note}
We should point out that the monoidal structure of
\(\mathfrak{g}\text{-}\mathbf{Mod}\) is \emph{not} the same as that of
@@ -846,22 +874,20 @@ then follows\dots
products.
\end{note}
-Representations are the subjects of \emph{representation theory}, a field
-dedicated to understanding a Lie algebra \(\mathfrak{g}\) via its
-\(\mathfrak{g}\)-modules. The fundamental problem of representation theory is a
-simple one: classifying all representations of a given Lie algebra up to
-isomorphism. However, understanding the relationship between representations is
-also of huge importance. In other words, to understand the whole of
+The fundamental problem of representation theory is a simple one: classifying
+all representations of a given Lie algebra up to isomorphism. However,
+understanding the relationship between representations is also of huge
+importance. In other words, to understand the whole of
\(\mathfrak{g}\text{-}\mathbf{Mod}\) we need to study the collective behavior
-of representations -- as opposed to individual examples.
-
-To that end, we define\dots
+of representations -- as opposed to individual examples. To that end, we
+define\dots
\begin{definition}
Given a Lie algebra \(\mathfrak{g}\) and a representation \(V\) of
\(\mathfrak{g}\), a subspace \(W \subset V\) is called \emph{a
- subrepresentation} if it is stable under the action of \(\mathfrak{g}\) --
- i.e. \(X w \in W\) for all \(w \in W\) and \(X \in \mathfrak{g}\).
+ subrepresentation}, or \emph{a \(\mathfrak{g}\)-submodule}, if it is stable
+ under the action of \(\mathfrak{g}\) -- i.e. \(X w \in W\) for all \(w \in
+ W\) and \(X \in \mathfrak{g}\).
\end{definition}
\begin{example}\label{ex:sl2-polynomial-subrep}