lie-algebras-and-their-representations

diff --git a/sections/semisimple-algebras.tex b/sections/semisimple-algebras.tex
@@ -643,21 +643,45 @@ words\dots
   of \(\mathfrak{g}\)}.
 \end{definition}
 
-% TODO: Point out this is known as "the highest weight theorem"
 \begin{theorem}\label{thm:dominant-weight-theo}
   For each dominant integral \(\lambda \in P\) there exists precisely one
   irreducible finite-dimensional representation \(V\) of \(\mathfrak{g}\) whose
   highest weight is \(\lambda\).
 \end{theorem}
 
-Fix some dominant integral \(\lambda \in P\). The ``uniqueness'' part of the
-theorem follows at once from the argument used for \(\mathfrak{sl}_3(K)\). The
-``existence'' part is more nuanced. Our first instinct is, of course, to try to
-generalize the proof used for \(\mathfrak{sl}_3(K)\). The issue is that our
-proof relied heavily on our knowledge of the roots of \(\mathfrak{sl}_3(K)\).
-Instead, we need a new strategy for the general setting. To that end, we
-introduce a special class of \(\mathfrak{g}\)-modules, known as \emph{Verma
-modules}.
+This is known as \emph{the highest weight theorem}, and its proof is the focus
+of this section. The ``uniqueness'' part of the theorem follows at once from
+the argument used for \(\mathfrak{sl}_3(K)\). Namely\dots
+
+\begin{proposition}\label{thm:irr-subrep-generated-by-vec}
+  Let \(V\) be a finite-dimensional representation of \(\mathfrak{g}\) and \(v
+  \in V\) be a highest weight vector. Then the subrepresentation
+  \(\mathcal{U}(\mathfrak{g}) \cdot v \subset V\) generated by \(v\) is
+  irreducible.
+\end{proposition}
+
+\begin{corollary}
+  Let \(V\) and \(W\) be finite-dimensional irreducible
+  \(\mathfrak{g}\)-modules with highest weight given by some common \(\lambda
+  \in P\). Then \(V \cong W\).
+\end{corollary}
+
+\begin{proof}
+  Let \(v \in V\) and \(w \in W\) be highest weight vectors and \(U =
+  \mathcal{U}(\mathfrak{g}) \cdot v + w \subset V \oplus W\). It is clear that
+  \(v + w\) is a highest weight vector of \(V \oplus W\). Hence by
+  proposition~\ref{thm:irr-subrep-generated-by-vec} \(U\) is irreducible. The
+  projections \(\pi_1 : U \to V\) and \(\pi_2 : U \to W\) are thus nonzero
+  intertwiners between irreducible representations of \(\mathfrak{g}\) and are
+  therefore isomorphisms. Hence \(V \cong U \cong W\).
+\end{proof}
+
+The ``existence'' part is more nuanced. Our first instinct is, of course, to
+try to generalize the proof used for \(\mathfrak{sl}_3(K)\). The issue is that
+our proof relied heavily on our knowledge of the roots of
+\(\mathfrak{sl}_3(K)\). Instead, we need a new strategy for the general
+setting. To that end, we introduce a special class of \(\mathfrak{g}\)-modules,
+known as \emph{Verma modules}.
 
 \begin{definition}\label{def:verma}
   The \(\mathfrak{g}\)-module \(M(\lambda) =

diff --git a/sections/sl2-sl3.tex b/sections/sl2-sl3.tex
@@ -997,7 +997,7 @@ images of a highest weight vector under successive applications of \(E_{2 1}\),
 \(\mathfrak{sl}_3(K)\) -- please refer to \cite{fulton-harris} for further
 details. The same argument also goes to show\dots
 
-\begin{corollary}
+\begin{corollary}\label{thm:irr-component-of-high-vec}
   Given a representation \(V\) of \(\mathfrak{sl}_3(K)\) with highest weight
   \(\lambda\) and \(v \in V_\lambda\), the subspace spanned by successive
   applications of \(E_{2 1}\), \(E_{3 1}\) and \(E_{3 2}\) to \(v\) is an
@@ -1099,11 +1099,13 @@ simpler than that.
   Hence the highest weight of \(V \oplus W\) is \(\lambda\) -- with highest
   weight vectors given by the sum of highest weight vectors of \(V\) and \(W\).
 
-  % TODO: Define the irreducible component of a vector
+  % TODO: Define the subrepresentation generated by a vector
   Fix some \(v \in V_\lambda\) and \(w \in W_\lambda\) and consider the
-  irreducible representation \(U = \mathfrak{sl}_3(K) \cdot v + w\) generated
-  by \(v + w\). The projection maps \(\pi_1 : U \to V\), \(\pi_2 : U \to W\),
-  being non-zero homomorphism between irreducible representations of
+  subrepresentation \(U = \mathcal{U}(\mathfrak{sl}_3(K)) \cdot v + w \subset V
+  \oplus W\) generated by \(v + w\). Since \(v + w\) is a highest weight of \(V
+  \oplus W\), it follows from corollary~\ref{thm:irr-component-of-high-vec}
+  that \(U\) is irreducible. The projection maps \(\pi_1 : U \to V\), \(\pi_2 :
+  U \to W\), being non-zero homomorphism between irreducible representations of
   \(\mathfrak{sl}_3(K)\) must be isomorphism. Finally,
   \[
     V \cong U \cong W