lie-algebras-and-their-representations

diff --git a/sections/mathieu.tex b/sections/mathieu.tex
@@ -183,33 +183,45 @@
   \(\mathcal{M}[\lambda]\) has finite length as a \(\mathfrak{g}\)-module.
 \end{lemma}
 
-% TODO: Pose this more abstractly: the key property of the semisimplification
-% is the fact that it is semisimple and the composition series of M
-% TODO: From this we may conclude that any cuspidal submodule fits nicely in
-% the semisimplification of any of its coherent extensions
-% TODO: Note that the semisimplification is only defined up to isomorphism: the
-% isomorphism class is independant of the composition series because all
-% composition series are conjugate
-% TODO: Note that the semisimplification is independent of the choice of
-% representatives
+% TODO: From this we may conclude that any admissible submodule is a submodule
+% of the semisimplification of any of its coherent extensions
 \begin{corollary}
-  Let \(\{\lambda_i\}_i\) be a set of representatives of the \(Q\)-cosets of
-  \(\mathfrak{h}^*\). Given a coherent family \(\mathcal{M}\) of degree \(d\)
-  and composition series \(0 = \mathcal{M}_{i 0} \subset \mathcal{M}_{i 1}
-  \subset \cdots \subset \mathcal{M}_{i n_i} = \mathcal{M}[\lambda_i]\), the
-  \(\mathfrak{g}\)-module
+  Let \(\mathcal{M}\) be a coherent family of degree \(d\). There exists a
+  unique completely reducible coherent family
+  \(\mathcal{M}^{\operatorname{ss}}\) of degree \(d\) such that the composition
+  series of \(\mathcal{M}^{\operatorname{ss}}[\lambda]\) is the same as that of
+  \(\mathcal{M}[\lambda]\) for all \(\lambda \in \mathfrak{h}^*\), called
+  \emph{the semisimplification\footnote{Recall that a ``semisimple'' is a
+  synonim for ``completely reducible'' in the context of modules.} of
+  \(\mathcal{M}\)}.
+
+  Namely, if \(\{\lambda_i\}_i\) is a set of representatives of the
+  \(Q\)-cosets of \(\mathfrak{h}^*\) and \(0 = \mathcal{M}_{i 0} \subset
+  \mathcal{M}_{i 1} \subset \cdots \subset \mathcal{M}_{i n_i} =
+  \mathcal{M}[\lambda_i]\) is a composition series,
   \[
     \mathcal{M}^{\operatorname{ss}}
-    = \bigoplus_{i j}
-      \mfrac{\mathcal{M}_{i j + 1}}{\mathcal{M}_{i j}}
+    \cong \bigoplus_{i j} \mfrac{\mathcal{M}_{i j + 1}}{\mathcal{M}_{i j}}
   \]
-  is also a coherent family of degree \(d\), 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{proof}
+  % TODOOO: Note that any submodule of a semisimple module is semisimple
+  The uniqueness of \(\mathcal{M}^{\operatorname{ss}}\) should be clear:
+  since \(\mathcal{M}^{\operatorname{ss}}\) is completely reducible, so is
+  \(\mathcal{M}^{\operatorname{ss}}[\lambda_i]\). Hence
+  \[
+    \mathcal{M}^{\operatorname{ss}}[\lambda_i]
+    \cong \bigoplus_j \mfrac{\mathcal{M}_{i j + 1}}{\mathcal{M}_{i j}}
+  \]
+
+  As for the existence of the semisimplification, it suffices to show
+  \[
+    \mathcal{M}^{\operatorname{ss}}
+    = \bigoplus_{i j} \mfrac{\mathcal{M}_{i j + 1}}{\mathcal{M}_{i j}}
+  \]
+  is indeed a completely reducible coherent family of degree \(d\).
+
   We know from examples~\ref{ex:submod-is-weight-mod} and
   \ref{ex:quotient-is-weight-mod} that each quotient \(\mfrac{\mathcal{M}_{i j
   + 1}}{\mathcal{M}_{i j}}\) is a weight module. Hence
@@ -485,12 +497,14 @@
   \(\mathcal{M}\) be a coherent extension of \(V\) and take
   \(\operatorname{Ext}(V) = \mathcal{M}^{\operatorname{ss}}\) of \(V\).
 
+  % TODOOOOOO: Extract this to a general result: any admissible module is
+  % contained in the semisimplification of any of its coherent extensions
   We claim \(V\) is contained in \(\operatorname{Ext}(V)\). Indeed, if we fix
-  some composition series \(0 =
-  \mathcal{M}_0 \subset \mathcal{M}_1 \subset \cdots \subset \mathcal{M}_n =
-  \mathcal{M}[\lambda]\) of \(\mathcal{M}[\lambda]\) with
-  \(V \cong \mfrac{\mathcal{M}_{i + 1}}{\mathcal{M}_i}\), \(\lambda \in
-  \operatorname{supp} V\), there is a natural inclusion
+  some composition series \(0 = \mathcal{M}_0 \subset \mathcal{M}_1 \subset
+  \cdots \subset \mathcal{M}_n = \mathcal{M}[\lambda]\) of
+  \(\mathcal{M}[\lambda]\) with \(V \cong \mfrac{\mathcal{M}_{i +
+  1}}{\mathcal{M}_i}\), \(\lambda \in \operatorname{supp} V\), there is a
+  natural inclusion
   \[
     V
     \isoto \mfrac{\mathcal{M}_{i + 1}}{\mathcal{M}_i}