diff --git a/sections/complete-reducibility.tex b/sections/complete-reducibility.tex
@@ -249,17 +249,63 @@ is actually pretty simple. Namely, it suffices to note that the adjoint
representation \(\mathfrak{g}\) is the direct sum of irreducible
subrepresentations, which are all simple ideals of \(\mathfrak{g}\) -- so
\(\mathfrak{g}\) is the direct sum of simple Lie algebras. The proof of the
-converse is more nuanced, and this will be our next milestone. Before proceding
-to the proof of complete reducibility, however, we would like to review some
-basic tools which will come in handy later on, known as\dots
+converse is more nuanced, and this will be our next milestone.
+
+Before proceding to the proof of complete reducibility, however, we would like
+to introduce some basic tools which will come in handy later on, known as\dots
\section{Invariant Bilinear Forms}
-Another interesting characterization of semisimple Lie algebras, which will
-come in handy later on, is the following.
+\begin{definition}
+ A symmetric bilinear \(B : \mathfrak{g} \times \mathfrak{g} \to K\) is called
+ \emph{\(\mathfrak{g}\)-invariant} if the operator \(\operatorname{ad}(X) :
+ \mathfrak{g} \to \mathfrak{g}\) is antisymmetric with respect to \(B\) for
+ all \(X \in \mathfrak{g}\).
+ \[
+ B(\operatorname{ad}(X) Y, Z) + B(Y, \operatorname{ad}(Y) Z) = 0
+ \]
+\end{definition}
+
+\begin{note}
+ The etimology of the term \emph{invariant form} comes from group
+ representation theory. If \(G \subset \operatorname{GL}(V)\) is a group of
+ linear automorphisms of a \(K\)-vector space \(V\), a bilinear form \(B : V
+ \times V \to K\) is called \(G\)-invariant if each \(g \in G\) is an
+ orthogonal operator with respect to the form \(B\).
+\end{note}
+
+An interesting example of an invariant bilinear form is the so called
+\emph{Killing form}.
+
+\begin{definition}
+ Given a finite-dimensional Lie algebra \(\mathfrak{g}\), the symmetric
+ bilinear form
+ \begin{align*}
+ B : \mathfrak{g} \times \mathfrak{g} & \to K \\
+ (X, Y) &
+ \mapsto \operatorname{Tr}(\operatorname{ad}(X) \operatorname{ad}(Y))
+ \end{align*}
+ is called \emph{the Killing form of \(\mathfrak{g}\)}.
+\end{definition}
+
+The fact that the Killing form is an invariant form follows directly from the
+identity \(\operatorname{Tr}([X, Y] Z) = \operatorname{Tr}(X [Y, Z])\), \(X, Y,
+Z \in \mathfrak{gl}_n(K)\). In fact this same identity show\dots
+
+\begin{lemma}
+ Given a finite-dimensional representation \(V\) of \(\mathfrak{g}\), the
+ symmetric bilinear form
+ \begin{align*}
+ B_V : \mathfrak{g} \times \mathfrak{g} & \to K \\
+ (X, Y) & \mapsto \operatorname{Tr}(X\!\restriction_V \, Y\!\restriction_V)
+ \end{align*}
+ is \(\mathfrak{g}\)-invariant.
+\end{lemma}
+
+The reason why we are disccussing invariant bilinear forms is the following
+characterization of finite-dimensional semisimple Lie algebras.
-% TODO: Define the Killing form beforehand
-% TODO: Define invariant forms beforehand
+% TODO: Prove this
\begin{proposition}
Let \(\mathfrak{g}\) be a Lie algebra. The following statements are
equivalent.
@@ -280,7 +326,7 @@ come in handy later on, is the following.
\end{proposition}
We refer the reader for \cite[ch. 5]{humphreys} for a proof of this last
-result. Without further ado, we may proceed to a proof of\dots
+result. Without further ado, we may proceed to our\dots
\section{Proof of Complete Reducibility}