diff --git a/sections/mathieu.tex b/sections/mathieu.tex
@@ -164,6 +164,7 @@ entire \(Q\)-coset it enhabits -- i.e.
\(\operatorname{supp}_{\operatorname{ess}} K[x, x^{-1}] = 2 \mathbb{Z}\). This
isn't always the case. Nevertheless, in general we find\dots
+% TODOO: Explain what we mean by Zariski topology in 𝔥*
\begin{proposition}
Let \(V\) be an infinite-dimensional admissible representation of
\(\mathfrak{g}\). The essential support
@@ -171,11 +172,13 @@ isn't always the case. Nevertheless, in general we find\dots
\(\mathfrak{h}^*\).
\end{proposition}
-Again, there is plenty of examples of completely reducible modules which are
-\emph{not} weight modules. Nevertheless, weight modules constitute a large
-class of representations and understanding them can give us a lot of insight
-into the general case. Our goal is now classifying all irreducible weight
-\(\mathfrak{g}\)-modules for some fixed reductive Lie algebra \(\mathfrak{g}\).
+This proof was deemed too technical to be included in here, but see proposition
+3.5 of \cite{mathieu}. Again, there is plenty of examples of completely
+reducible modules which are \emph{not} weight modules. Nevertheless, weight
+modules constitute a large class of representations and understanding them can
+give us a lot of insight into the general case. Our goal is now classifying all
+irreducible weight \(\mathfrak{g}\)-modules for some fixed reductive Lie
+algebra \(\mathfrak{g}\).
As a first approximation of a solution to our problem, we consider the
induction functors \(\operatorname{Ind}_{\mathfrak{p}}^{\mathfrak{g}} :
@@ -235,7 +238,7 @@ construction very similar to that of Verma modules.
that Verma modules are indeed generalized Verma modules.}.
\end{definition}
-\begin{proposition}
+\begin{proposition}\label{thm:generalized-verma-has-simple-quotient}
Given an irreducible \(\mathfrak{p}\)-module \(V\), the generalized Verma
module \(M_{\mathfrak{p}}(V)\) has a unique maximal subrepresentation
\(N_{\mathfrak{p}}(V)\) and a unique irreducible quotient
@@ -243,6 +246,8 @@ construction very similar to that of Verma modules.
The irreducible quotient \(L_{\mathfrak{p}}(V)\) is a weight module.
\end{proposition}
+The proof of proposition~\ref{thm:generalized-verma-has-simple-quotient} is
+entirely analogous to that of proposition~\ref{thm:max-verma-submod-is-weight}.
This leads us to the following definitions.
\begin{definition}
@@ -544,7 +549,7 @@ to a completely reducible coherent extension of \(V\).
% TODO: Note somewhere that M[mu] is a submodule
% Mathieu's proof of this is somewhat profane, I don't think it's worth
% including it in here
-\begin{lemma}
+\begin{lemma}\label{thm:component-coh-family-has-finite-length}
Given a coherent family \(\mathcal{M}\) and \(\lambda \in \mathfrak{h}^*\),
\(\mathcal{M}[\lambda]\) has finite length as a \(\mathfrak{g}\)-module.
\end{lemma}
@@ -647,7 +652,9 @@ to a completely reducible coherent extension of \(V\).
In addition, there is no canonical choice of composition series.
\end{note}
-As promised, if \(\mathcal{M}\) is a coherent extension of \(V\) then so is
+The proof of lemma~\ref{thm:component-coh-family-has-finite-length} is
+extremily technical and may be found in \cite{mathieu} -- see lemma 3.3. As
+promised, if \(\mathcal{M}\) is a coherent extension of \(V\) then so is
\(\mathcal{M}^{\operatorname{ss}}\).
\begin{proposition}
@@ -748,7 +755,9 @@ coherent family are cuspidal representations?
\(\mathcal{M}[\lambda] = V\) and \(\mathcal{M}[\lambda]\) is cuspidal.
\end{proof}
-To finish the proof, we now show\dots
+Once more, the proof of proposition~\ref{thm:centralizer-multiplicity} wasn't
+deemed informative enought to be included in here, but see the proof of lemma
+2.3 of \cite{mathieu}. To finish the proof, we now show\dots
\begin{lemma}
Let \(\mathcal{M}\) be a coherent family. The set \(U = \{\lambda \in
@@ -1042,8 +1051,10 @@ well-behaved. For example, we can show\dots
functoriality of our constructions.
\end{note}
-Since \(F_\alpha\) is locally \(\operatorname{ad}\)-nilpotent for all \(\alpha
-\in \Delta\), we can see\dots
+The proof of the previous lemma is quite techinical and was deemed too tedious
+to be included in here. See lemma 4.4 of \cite{mathieu} for a full proof. Since
+\(F_\alpha\) is locally \(\operatorname{ad}\)-nilpotent for all \(\alpha \in
+\Delta\), we can see\dots
\begin{corollary}
Let \(\Sigma\) be as in lemma~\ref{thm:nice-basis-for-inversion} and