## Schur's recursive triangulation procedure

Given a linear endomorphism `f` on a non-trivial finite-dimensional vector space `E` over an
algebraically closed field `𝕜`, one can always pick an eigenvalue `μ` of `f` whose corresponding
eigenspace `V` is non-trivial. Given that `E` is also an inner product space, let `bV` and `bW` be
othonormal bases for `V` and `Vᗮ` respectively. Then, the collection of vectors in `bV` and `bW`
forms an othornomal basis `bE` for `E`, as the direct sum of `V` and `Vᗮ` is an internal
decomposition of `E`. The matrix representation of `f` with respect to `bE` satisfies
$$
\sideset{_\mathrm{bE}}{_\mathrm{bE}}{[f]} =
\begin{bmatrix}
\sideset{_\mathrm{bV}}{_\mathrm{bV}}{[f]} &
\sideset{_\mathrm{bW}}{_\mathrm{bV}}{[f]} \\
\sideset{_\mathrm{bV}}{_\mathrm{bW}}{[f]} &
\sideset{_\mathrm{bW}}{_\mathrm{bW}}{[f]}
\end{bmatrix} =
\begin{bmatrix} \mu I & □ \\ 0 & \sideset{_\mathrm{bW}}{_\mathrm{bW}}{[f]} \end{bmatrix},
$$
which is upper triangular as long as $\sideset{_\mathrm{bW}}{_\mathrm{bW}}{[f]}$ is. Finally, one
observes that the recursion from $\sideset{_\mathrm{bE}}{_\mathrm{bE}}{[f]}$ to
$\sideset{_\mathrm{bW}}{_\mathrm{bW}}{[f]}$ is well-founded, as the dimension of `bW` is smaller
than that of `bE` because `bV` is non-trivial.

However, in order to leverage `DirectSum.IsInternal.collectedOrthonormalBasis`, the type
`Σ b, cond b (Fin m) (Fin n)` has to be used instead of the more natural `Fin m ⊕ Fin n` while their
equivalence is propositionally established by `Equiv.sumEquivSigmalCond`.

## Showing `Lorentz.SL2C.toSelfAdjointMap` has determinant 1

Since `Lorentz.ℍ₂` as a real vector space has the 4 Pauli matrices as basis, we know that its vector
representation consists of 4 real components. This makes the matrix representation of
`toSelfAdjointMap M` a 4-by-4 real matrix `F`. To make the computation of `F.det` manageable, the
following basis is used instead of the Pauli matrices to induce as many zeros as possible in `F`:
$$
E_0 = \begin{bmatrix} 1 & 0 \\ 0 & 0 \end{bmatrix},
E_1 = \begin{bmatrix} 0 & 0 \\ 0 & 1 \end{bmatrix},
E_2 = \sigma_1 = \begin{bmatrix} 0 & 1 \\ 1 & 0 \end{bmatrix},
E_3 = -\sigma_2 = \begin{bmatrix} 0 & i \\ -i & 0 \end{bmatrix},
$$
Suppose that $M = \begin{bmatrix} x & □ \\ 0 & y \end{bmatrix}$ is upper triangular, the basis
$\{E_k\}_{k=0}^3$ induces the matrix representation
$$
F = \begin{bmatrix}
\lvert x\rvert^2 & □ & □ & □ \\
0 & \lvert y\rvert^2 & 0 & 0 \\
0 & □ & \operatorname{Re}(x\bar{y}) & -\operatorname{Im}(x\bar{y}) \\
0 & □ & \operatorname{Im}(x\bar{y}) & \operatorname{Re}(x\bar{y}) \\
\end{bmatrix}.
$$
If $xy = 1$, the Schur complement formula `Matrix.det_fromBlocks₂₂` yields
$$\begin{align}
\det F &=
\begin{vmatrix}
\operatorname{Re}(x\bar{y}) & -\operatorname{Im}(x\bar{y}) \\
\operatorname{Im}(x\bar{y}) & \operatorname{Re}(x\bar{y})
\end{vmatrix} \det\left(
\begin{bmatrix} \lvert x\rvert^2 & □ \\ 0 & \lvert y\rvert^2 \end{bmatrix} -
\begin{bmatrix} □ & □ \\ 0 & 0 \end{bmatrix}
\begin{bmatrix} □ & □ \\ □ & □ \end{bmatrix}
\begin{bmatrix} 0 & □ \\ 0 & □ \end{bmatrix}
\right) \\ &=
\lvert x\bar{y}\rvert^2 \lvert x\rvert^2 \lvert y\rvert^2 = \lvert xy\rvert^4 = 1.
\end{align}$$
This concludes `Lorentz.SL2C.toSelfAdjointMap_det_one'`. To get
`Lorentz.SL2C.toSelfAdjointMap_det_one`, triangulate the special linear matrix using
`Matrix.schur_triangulation`, and observe that `Matrix.schurTriangulation` preserves the determinant
which is 1.