diff --git a/sections/coherent-families.tex b/sections/coherent-families.tex
@@ -1,7 +1,6 @@
\chapter{Classification of Coherent Families}
% TODOOO: Is this decomposition unique??
-% TODOO: Prove this
\begin{proposition}
Suppose \(\mathfrak{g} = \mathfrak{s}_1 \oplus \cdots \oplus \mathfrak{s}_r\)
and let \(\mathcal{M}\) be a semisimple irreducible coherent
@@ -12,6 +11,90 @@
\]
\end{proposition}
+\begin{proof}
+ Suppose \(\mathfrak{h}_i \subset \mathfrak{s}_i\) are Cartan subalgebras,
+ \(\mathfrak{h} = \mathfrak{h}_1 \oplus \cdots \oplus \mathfrak{h}_r\) and \(d
+ = \deg \mathcal{M}\). Let \(M \subset \mathcal{M}\) be any
+ infinite-dimensional simple submodule, so that \(\mathcal{M}\) is a
+ semisimple coherent extension of \(M\). By
+ Example~\ref{thm:simple-weight-mod-is-tensor-prod}, there exists (unique)
+ simple weight \(\mathfrak{s}_i\)-modules \(M_i\) such that \(M \cong M_1
+ \otimes \cdots \otimes M_r\). Take \(\mathcal{M}_i = \mExt(M_i)\). We will
+ show that \(\mathcal{M}_1 \otimes \cdots \mathcal{M}_r\) is a coherent
+ extension of \(M\).
+
+ It is clear that \(\mathcal{M}_1 \otimes \cdots \otimes \mathcal{M}_r\) is a
+ degree \(d\) bounded \(\mathfrak{g}\)-module containing \(M\) as a submodule.
+ It thus suffices to show that \(\mathcal{M}\) is a coherent family. By
+ Example~\ref{ex:supp-ess-of-tensor-is-product},
+ \(\operatorname{supp}_{\operatorname{ess}} (\mathcal{M}_1 \otimes \cdots
+ \otimes \mathcal{M}_r) = \mathfrak{h}^*\). To see that the map
+ \begin{align*}
+ \mathfrak{h}^* & \to K \\
+ \lambda & \mapsto
+ \operatorname{Tr}
+ (
+ u\! \restriction_{(\mathcal{M}_1 \otimes \cdots \otimes \mathcal{M}_r)_\lambda}
+ )
+ \end{align*}
+ is polynomial, notice that the natural isomorphism of algebras
+ \begin{align*}
+ f : \mathcal{U}(\mathfrak{s}_1) \otimes \cdots \mathcal{U}(\mathfrak{s}_1)
+ & \isoto \mathcal{U}(\mathfrak{g}) \\
+ u_1 \otimes \cdots \otimes u_r & \mapsto u_1 \cdots u_r
+ \end{align*}
+ described in Example~\ref{ex:univ-enveloping-of-sum-is-tensor} is a
+ \(\mathfrak{g}\)-homomorphism between the tensor product of the adjoint
+ \(\mathfrak{s}_i\)-modules \(\mathcal{U}(\mathfrak{s}_i)\) and the adjoint
+ \(\mathfrak{g}\)-module \(\mathcal{U}(\mathfrak{g})\).
+
+ Indeed, given \(X = X_1 + \cdots + X_r \in \mathfrak{g}\) with \(X_i \in
+ \mathfrak{s}_i\) and \(u_i \in \mathcal{U}(\mathfrak{s}_i)\),
+ \[
+ \begin{split}
+ f(X \cdot (u_1 \otimes \cdots \otimes u_r))
+ & = f([X_1, u_1] \otimes u_2 \otimes \cdots \otimes u_r)
+ + \cdots
+ + f(u_1 \otimes \cdots \otimes u_{r-1} \otimes [X_r, u_r]) \\
+ & = [X_1, u_1] u_2 \cdots u_r + \cdots + u_1 \cdots u_{r-1} [X_r, u_r] \\
+ \text{(\([X_i, u_j] = 0\) for \(i \ne j\))}
+ & = [X_1, u_1u_2 \cdots u_r] + \cdots + [X_r, u_1 \cdots u_{r-1}u_r] \\
+ & = [X, f(u_1 \otimes \cdots \otimes u_r)]
+ \end{split}
+ \]
+
+ Hence by Example~\ref{ex:adjoint-action-in-universal-enveloping-is-weight}
+ \(f\) restricts to an isomorphism of algebras \(\mathcal{U}(\mathfrak{s}_1)_0
+ \otimes \cdots \otimes \mathcal{U}(\mathfrak{s}_r)_0 \isoto
+ \mathcal{U}(\mathfrak{g})_0\) with image \(\mathcal{U}(\mathfrak{g})_0 =
+ \mathcal{U}(\mathfrak{s}_1)_0 \cdots \mathcal{U}(\mathfrak{s}_r)_0\). More
+ importantly, if we write \(\lambda = \lambda_1 + \cdots + \lambda_r\) for
+ \(\lambda_i \in \mathfrak{h}_i^*\) it is clear from
+ Example~\ref{ex:tensor-prod-of-weight-is-weight} that the
+ \(\mathcal{U}(\mathfrak{g})_0\)-module \((\mathcal{M}_1 \otimes \cdots
+ \otimes \mathcal{M}_r)_\lambda\) corresponds to exactly the
+ \(\mathcal{U}(\mathfrak{s}_1)_0 \otimes \cdots \otimes
+ \mathcal{U}(\mathfrak{s}_r)_0\)-module \((\mathcal{M}_1)_{\lambda_1} \otimes
+ \cdots \otimes (\mathcal{M}_r)_{\lambda_r}\), so we can see that the value
+ \[
+ \operatorname{Tr}
+ (
+ u_1 \cdots u_r \!\restriction_{(\mathcal{M}_1 \otimes \cdots \otimes \mathcal{M}_r)_\lambda}
+ )
+ = \operatorname{Tr}(u_1\!\restriction_{(\mathcal{M}_1)_{\lambda_1}})
+ \cdots
+ \operatorname{Tr}(u_r\!\restriction_{(\mathcal{M}_r)_{\lambda_r}})
+ \]
+ varies polynomially with \(\lambda \in \mathfrak{h}^*\) for all \(u_i \in
+ \mathcal{U}(\mathfrak{s}_i)_0\).
+
+ Finally, \(\mathcal{M}_1 \otimes \cdots \otimes \mathcal{M}_r\) is a coherent
+ extension of \(M\). Since the \(\mathcal{M}_i = \mExt(M_i)\) are semisimple,
+ so is \(\mathcal{M}_1 \otimes \cdots \otimes \mathcal{M}_r\). It thus
+ follows from the uniqueness of semisimple coherent extensions that
+ \(\mathcal{M} \cong \mathcal{M}_1 \otimes \cdots \otimes \mathcal{M}_r\).
+\end{proof}
+
% TODO: Rework this
In addition, it turns out that very few simple Lie algebras admit cuspidal
modules at all. Specifically\dots