lie-algebras-and-their-representations

diff --git a/sections/mathieu.tex b/sections/mathieu.tex
@@ -22,6 +22,7 @@
 \end{example}
 
 % TODO: Is every quotient of a weight module a weight module too?
+% TODO: I think so!
 \begin{example}
   Proposition~\ref{thm:verma-is-weight-mod} and
   proposition~\ref{thm:max-verma-submod-is-weight} imply that the Verma module
@@ -120,6 +121,10 @@
   \end{enumerate}
 \end{definition}
 
+% TODOO: Add a discussion on how this may sound unintuitive, but the motivation
+% comes from the relationship between highest weight modules and coherent
+% families
+
 \begin{definition}
   A coherent family \(\mathcal{M}\) called \emph{irreducible} if
   \(\mathcal{M}_\lambda\) is a simple
@@ -133,7 +138,27 @@
   \(V\) as a subquotient.
 \end{definition}
 
-% TODO: Define the semisimplification of a coherent family
+% Mathieu's proof of this is somewhat profane, I don't think it's worth
+% including it in here
+\begin{proposition}
+  Any coherent family \(\mathcal{M}\) has finite length as a
+  \(\mathfrak{g}\)-module. 
+\end{proposition}
+
+% TODO: Add a proof!
+\begin{corollary}
+  Given a coherent family \(\mathcal{M}\) and a composition series \(0 =
+  \mathcal{M}_0 \subset \mathcal{M}_1 \subset \cdots \subset \mathcal{M}_n =
+  \mathcal{M}\), the \(\mathfrak{g}\)-module
+  \[
+    \mathcal{M}^{\operatorname{ss}}
+    = \bigoplus_i \mfrac{\mathcal{M}_{i + 1}}{\mathcal{M}_i}
+  \]
+  is also a coherent family, called \emph{the semisimplification\footnote{This
+  name is due to the fact that $\mathcal{M}^{\operatorname{ss}}$ is the direct
+  sum of irreducible $\mathfrak{g}$-modules} of \(\mathcal{M}\)}.
+\end{corollary}
+
 \begin{theorem}[Mathieu]
   Let \(V\) be an infinite-dimensional admissible irreducible
   \(\mathfrak{g}\)-module of degree \(d\). There exists a unique semisimple
@@ -161,7 +186,7 @@
   \[
     \operatorname{Ext}(V) 
     \cong \mathcal{M}^{\operatorname{ss}}
-    = \bigoplus_j \mfrac{\mathcal{M}_{j + 1}}{\mathcal{M}_j},
+    = \bigoplus_i \mfrac{\mathcal{M}_{i + 1}}{\mathcal{M}_i},
   \]
   so that \(V\) is contained in \(\operatorname{Ext}(V)\).