lie-semisimple-classification.lean

import algebra.lie.classical
import algebra.lie.cartan_matrix
import algebra.lie.semisimple
import algebra.lie.direct_sum
import field_theory.algebraic_closure
open lie_algebra
open_locale direct_sum
notation L₁ ` ≅ₗ⁅` K `⁆ `L₂ := nonempty (L₁ ≃ₗ⁅K⁆ L₂)
abbreviation sl (l : ℕ) (K : Type*) [field K] := special_linear.sl (fin l) K
abbreviation sp (l : ℕ) (K : Type*) [field K] := symplectic.sp (fin l) K
abbreviation so (l : ℕ) (K : Type*) [field K] := orthogonal.so (fin l) K

/-- Let `K` be an algebraically closed field of characteristic zero. -/
variables (K : Type*) [field K] [is_alg_closed K] [char_zero K]

/-- Let `L` be a finite-dimensional Lie algebra over `K`. -/
variables (L : Type*) [lie_ring L] [lie_algebra K L] [finite_dimensional K L]

theorem simple_classification :
  is_simple K L ↔
  ((L ≅ₗ⁅K⁆ g₂ K) ∨
   (L ≅ₗ⁅K⁆ f₄ K) ∨
   (L ≅ₗ⁅K⁆ e₆ K) ∨
   (L ≅ₗ⁅K⁆ e₇ K) ∨
   (L ≅ₗ⁅K⁆ e₈ K) ∨
   (∃ l, (L ≅ₗ⁅K⁆ sl l K) ∧ 1 < l) ∨
   (∃ l, (L ≅ₗ⁅K⁆ sp l K) ∧ 2 < l) ∨
   (∃ l, (L ≅ₗ⁅K⁆ so l K) ∧ 4 < l ∧ l ≠ 6)) := sorry

-- TODO (probably) connect with `direct_sum.lie_algebra_is_internal`.
theorem semisimple_classification :
  is_semisimple K L ↔
  ∃ n (I : fin n → lie_ideal K L), (L ≅ₗ⁅K⁆ (⨁ i, I i)) ∧ ∀ i, is_simple K (I i) := sorry

/- Note that the `simple_classification` contains several of the "exceptional isomorphisms". E.g.,
`so(6)` is simple so it must be isomorphic to one of the other algebras on the list. For
dimensional reasons, this has to be `sl(4)`. Likewise for the other cases excluded. -/

-- These are not too hard to close.
instance : finite_dimensional K (g₂ K) := sorry
instance : finite_dimensional K (so 5 K) := sorry

-- Sanity check:
example : is_simple K (g₂ K) :=
by { rw simple_classification, left, constructor, refl, }

-- Sanity check:
example : is_simple K (so 5 K) :=
by { rw simple_classification, repeat { right, }, use 5, refine ⟨_, by simp⟩, constructor, refl, }

/- Note that ultimately we will probably state `simple_classification` in terms of algebras
constructed from Cartan matrices of types `A, B, C, D`. A side effect of this is that the conditions
on `l` will then be slightly neater since they are more naturally:
 * `1 ≤ l` for `Aₗ`
 * `2 ≤ l` for `Bₗ`
 * `3 ≤ l` for `Cₗ`
 * `4 ≤ l` for `Dₗ`

Thus, to the extent that they exist, the following six cases are omitted: `B₁, C₁, C₂, D₁, D₂, D₃`.
This is because they are degenerate (consider their Dynkin diagrams) and also because:
 * `B₁ ≅ A₁`
 * `C₁ ≅ A₁`
 * `C₂ ≅ B₂`
 * `D₁` Abelian, thus not simple
 * `D₂ ≅ A₁ ⊕ A₁`, thus not simple
 * `D₃ ≅ A₃`

If we recall that:
 * `Aₗ ≅ sl(l+1)`,  with dimension `l(l+2)`
 * `Bₗ ≅ so(2l+1)`, with dimension `l(2l+1)`
 * `Cₗ ≅ sp(l)`,    with dimension `l(2l+1)`
 * `Dₗ ≅ so(2l)`,   with dimension `l(2l-1)`

Then we see the list is:
 * `A : sl(2),  sl(3),  sl(4), ...`, with dimensions: ` 3,  8, 15, ...`
 * `B : so(5),  so(7),  so(9), ...`, with dimensions: `10, 21, 36, ...`
 * `C : sp(3),  sp(4),  sp(5), ...`, with dimensions: `21, 36, 55, ...`
 * `D : so(8), so(10), so(12), ...`, with dimensions: `28, 45, 66, ...`
[Aside: extending we can see e₆ is the only exceptional Lie algebra not distinguished by dimension.]

And the six cases cases omitted are:
 * `so(3) ≅ sl(2)`
 * `sp(1) ≅ sl(2)`
 * `sp(2) ≅ so(5)`
 * `so(2)` Abelian, thus not simple
 * `so(4) ≅ so(3) ⊕ so(3)`, thus not simple
 * `so(6) ≅ sl(4)`

This explains the bounds on `l` in `simple_classification`. -/