The classification of Lie algebras

Stream: mathlib4

[Oliver Nash]

I'd like to invite people to consider helping add the classification of semisimple Lie algberas to Mathlib. I think this is a very useful result with many applications and adding it to Mathlib would open up future formalisation prospects as well as exercise parts of our algebra library in a non-trivial way.

[Oliver Nash]

A few years ago I put some of the basics of Lie algebra theory in place and in recent months I took up the theory again. I'd guess that maybe six months of single-person effort remains to finish the result.

[Oliver Nash]

To give a sense of where we are, I have created a project here: https://github.com/orgs/leanprover-community/projects/17/views/1?pane=info

Most of the items in this project are fairly non-trivial but some are probably only a few days of work (modulo time to familiarise with this corner of the library). For example: https://github.com/leanprover-community/mathlib4/issues/10073 should be easy enough.

Anyone should feel free to break down these tasks or add new items.

[Johan Commelin]

In my procrastination time, I've shown that regular elements exist in free Lie algebras of rank $n$ over domains with at least $n$ elements. From there it is a little computation to get the existence of Cartan subalgebras in those same Lie algebras. Should probably be done a few days from now. (Depending on the amount of procrastination time that I get.)

[Oliver Nash]

I managed to get docs#Module.End.exists_isNilpotent_isSemisimple into master today which I expect to need for #10064

[Oliver Nash]

Sooner or later I will probably also need this result:

import Mathlib.LinearAlgebra.Semisimple
import Mathlib.FieldTheory.Perfect

variable {K M : Type*} [Field K] [AddCommGroup M] [Module K M] {f g : Module.End K M}

theorem Module.End.isSemisimple_add_of_commute [PerfectField K] [FiniteDimensional K M]
    (comm : Commute f g)
    (hf : f.IsSemisimple)
    (hg : g.IsSemisimple) :
    (f + g).IsSemisimple := by
  -- Your proof here!
  sorry

so if somebody wants to take that on, I'd be very grateful :-)

[Eric Rodriguez]

What's the maths proof?

[Oliver Nash]

I haven't decided!

[Oliver Nash]

The obvious route is to prove that for semisimple endomorphisms docs#Module.End.generalizedEigenspace and docs#Module.End.eigenspace coincide, pass to the algebraic closure, invoke docs#Module.End.iSup_generalizedEigenspace_eq_top to see that semisimple means diagonalisable in this case, observe that this is an iff, and then argue that commuting diagonalisable endomorphisms are simultaneously diagonalisable.

[Oliver Nash]

I think to get back from the algebraic closure to the original coefficients, you'll need to use that the field is perfect and possibly prove the converse of docs#isSemisimple_of_squarefree_aeval_eq_zero

[Oliver Nash]

There might also be a slick proof!

[Oliver Nash]

Also, even just filling in any of the gaps in our eigenspace theory indicated above would be very helpful!

[Oliver Nash]

I'm going to try experimenting in this thread by dropping in formal statements of non-trivial gaps in the library which it would be useful to get filled. Here's one that would really help:

import Mathlib.LinearAlgebra.JordanChevalley
import Mathlib.Algebra.Lie.Killing

namespace LieAlgebra

variable (K L : Type*) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L]
  [CharZero K] [IsSemisimple K L] -- Or maybe just `[PerfectField K] [IsKilling K L]` suffices?

-- Bourbaki Chap. I, §6.3, Proposition 3 (page 52)
-- See also Fulton & Harris, Proposition C.17 (page 482)
theorem exists_isNilpotent_isSemisimple (x : L) :
    ∃ n s : L,
      _root_.IsNilpotent (ad K L n) ∧
      Module.End.IsSemisimple (ad K L s) ∧
      ⁅n, s⁆ = 0 ∧
      (∀ y : L, ⁅y, x⁆ = 0 → ⁅y, n⁆ = 0) ∧
      (∀ y : L, ⁅y, x⁆ = 0 → ⁅y, s⁆ = 0) ∧
      x = n + s := by
  sorry

end LieAlgebra

[Johan Commelin]

I have formalized a proof of the existence of Cartan subalgebras. More precisely: let L be a finite-dimensional Lie algebra over a field K. If K has more elements than the dimension of L, then L has a Cartan subalgebra.
(In general it is an open problem in Lie theory whether large Lie algebras over small fields have Cartan subalgebras.)

The proof needs

lemma finrank_maximalGeneralizedEigenspace :
    finrank K (φ.maximalGeneralizedEigenspace 0) = natTrailingDegree (φ.charpoly) := by

and I bashed through a proof with the available tools. But it seems that there are gaps in our Eigenspace library that could easily house the NSA parking lot. However, I didn't have the time and energy to fill those gaps as prerequisite for this result in Lie theory, so I took the shortest path to my end goal.

[Damiano Testa]

What are the assumptions on K?

[Johan Commelin]

In the lemma that I quote, K is a field, and \phi is an endomorphism of a findim VS over K.

[Damiano Testa]

Ok, I still think that your "weaker" version is likely true, but I have not thought of a fully-formed proof yet.

[Damiano Testa]

Btw, any reason for the parentheses around φ.charpoly?

[Damiano Testa]

(also, sorry for not reading the text before the statement of the lemma, where you had already explained that K was a field)

[Johan Commelin]

Damiano Testa said:

Btw, any reason for the parentheses around φ.charpoly?

No! Just copypasta

[Antoine Chambert-Loir]

I feel we should take the time to formalize all of basic linear algebra before embarking in this (more exciting) world…

[Kevin Buzzard]

@Johan Commelin can you formalise the statements of what is missing, or even approximations to the statements?

[Johan Commelin]

Well... for starters there is the lemma that I mentioned above.

[Johan Commelin]

There is basically very little connection between the characteristic polynomial and eigenvectors/spaces.

[Johan Commelin]

But it's a bit hard to describe the gap precisely. It's just that there's a lot of API missing.

[Johan Commelin]

For things like this, it would be good if we had json files that told us which statements from standard reference texts are done, and which ones are missing.

[Antoine Chambert-Loir]

Indeed, it would be interesting, and probably instructive, to have Rudin/Lang/Matsumura/Bourbaki projects that formalize every statement of the book within mathlib's language. (No real proof should be added, only invocations of mathlib's proofs. And if proofs are needed, their adequate version should be added to mathlib.)

[Johan Commelin]

Anyway, while I agree that we should definitely work on this, I think there is also some momentum for the Lie theory project at the moment. And I don't think that should necessarily be postponed until LA is done.

[Kevin Buzzard]

I've said this to people offline but just to say it publically -- Tom Hales was very excited a few years ago that Oliver had even stated the classification, because he already felt that this was important. The proof will be a real milestone.

[Xela]

The relevant mathematics I know only deals with the complex lie algebra case, and I don't know what generalizes and what doesn't. I am interested in (eventually - I'm still learning the basics of Lean) working on the root system theory part, https://github.com/leanprover-community/mathlib4/issues/10067. Is it still true that over any field of char=0 that the root systems are classified by Dynkin Diagrams?

[Oliver Nash]

Yes I believe this is true because a root system induces a Q-structure and because they behave well with respect to base change.

[Oliver Nash]

I'm not expert though and we have some here. Perhaps @Scott Carnahan could comment?

[Scott Carnahan]

Over any field of characteristic zero, the finite crystallographic root systems are classified by finite type Dynkin diagrams.

[Oliver Nash]

You've convinced me @Scott Carnahan : would you be interested in convincing Lean?

[Scott Carnahan]

Absolutely. Sorry I haven't made much progress on Lie algebras recently - I've been distracted by Hahn series.

[Johan Commelin]

No need to apologize! We're all crazy busy. And having a smooth Hahn series PR is also great!

[Johan Commelin]

feat(Algebra/Lie): existence of Cartan subalgebras #12297

This PR contains a thoroughly documented 200-line monster proof that leads to a 10-line corollary proving the existence of Cartan subalgebras.

lemma exists_IsCartanSubalgebra_of_finrank_le_card (h : finrank K L ≤ #K) :
    ∃ H : LieSubalgebra K L, IsCartanSubalgebra H := by ...

[Johan Commelin]

I would be very happy to have some reviews of the monster proof. I don't think there are many reusable components. And extracting local definitions let into stand-alone definitions means that they will depend on parameters which makes their use in the monster proof awkard.
Things like

  let χ : Polynomial (K[X]) := lieCharpoly K E x u
  let ψ : Polynomial (K[X]) := lieCharpoly K Q x u

would no longer be χ and ψ whenever used, but would be χ K E x y and ψ K E x y all over the place. Which I think is not an improvement.

[Riccardo Brasca]

Having a look.

[Riccardo Brasca]

If you really want to split you can extract the case r = finrank K L and maybe one or two suffices, like suffices χ = X ^ r, but it is a bit strange. The proof is very fast on my computer, so I don't think it is a real problem to keep it.

[Johan Commelin]

Thanks for the review!

[Kevin Buzzard]

"Dimension of L is at most cardinality of K??" That's my review

[Richard Copley]

The condition that F has at least dim L elements cannot be omitted from
theorem 1, as is shown by the following example. [...]

Donald W. Barnes - On Cartan subalgebras of Lie algebras (1967)

I'm probably misunderstanding everything, but maybe the first theorem is "just a stepping stone" for the second.

[Kevin Buzzard]

It's very cool that we're proving everything in the right generality here. I know that this has been one of Oliver's design decisions in setting up the theory all the way through, even when it's made some proofs far more work.

[Johan Commelin]

Kevin Buzzard said:

"Dimension of L is at most cardinality of K??" That's my review

Sorry, I'm being obtuse... am I missing a typo?

[Riccardo Brasca]

The condition is rather surprising, I almost commented "there must be a typo" before checking that this is the actual statement.

[Kevin Buzzard]

Probably it's less surprising if you've just proved the theorem :-)

[Patrick Massot]

Johan Commelin said:

I would be very happy to have some reviews of the monster proof. I don't think there are many reusable components. And extracting local definitions let into stand-alone definitions means that they will depend on parameters which makes their use in the monster proof awkard.
Things like

  let χ : Polynomial (K[X]) := lieCharpoly K E x u
  let ψ : Polynomial (K[X]) := lieCharpoly K Q x u

would no longer be χ and ψ whenever used, but would be χ K E x y and ψ K E x y all over the place. Which I think is not an improvement.

I want to strongly refute this message, although I have no strong opinion about what we should do with this proof. It is definitely possible to split this monster proof into lemmas with almost no impact on the existing proof, and certainly none of what Johan described above. This is something we learned from large scale project (specifically sphere eversion here). I created a branch with this commit. The only change is the proof scripts are adding the line setup_notation at the beginning of most lemmas and three extra change lines because omega was confused. Otherwise each proof is copy-pasted from the original proof. The lemma statements have a couple of extra P..

The main trick is to introduce a ad-hoc structure holding the assumptions of the monster proof, and then some abbrev replace the definitions. Again I don’t strongly claim that we should merge this commit into Johan’s branch and finish the factoring out job (at some point I got too hungry to continue). I do claim that such a split is possible. One could argue that Sebastian’s work on incremental compilation will soon make that knowledge obsolete, but right now this is nice to know IMHO.

[Patrick Massot]

There is a little lie in my message: the new proofs also delete a couple of explicit unfoldings that are no longer necessary.

[Patrick Massot]

@Johan Commelin

[Johan Commelin]

Aah, very nice!

[Johan Commelin]

That setup_notation macro is great. Do we have similar examples in mathlib already?

[Patrick Massot]

The line length linter doesn’t think this macro is great. But this is only because I can never remember how to write a macro that produces a quoted tacticSeq.

[Patrick Massot]

I don’t think we use this kind of splitting methodology in Mathlib. We certainly use it a lot in sphere eversion.

[Patrick Massot]

And now I really need to find food.

[Patrick Massot]

@Ruben Van de Velde I wish I could find a baguette, but I’m in the USA this year… This is great, but there are some tradeoffs.

[Adam Topaz]

Johan Commelin said:

That setup_notation macro is great. Do we have similar examples in mathlib already?

I think that some generalization of this should indeed be added to mathlib. I'm envisioning some new commands that create the structure along with the setup_notation macro automatically.

[Patrick Massot]

Note that my example does more than creating lets for the fields, it also does it for some later definitions.

[Adam Topaz]

It's a bit hard to read the diff on github with the link to the commit above due to all of the CI errors being placed inline in the diff. Does anyone know how to temporarily turn off those error messages?

[Patrick Massot]

Oh indeed. It wasn’t like that in the beginning, the linter kicked off later.

[Antoine Chambert-Loir]

Kevin Buzzard said:

Probably it's less surprising if you've just proved the theorem :-)

There is a classic proof of the Nullstellensatz for uncountable fields that builds on the same idea: a finitely (countably would work) generated (associative and commutative) K-algebra is algebraic.

[Johan Commelin]

@Vincent Beffara Btw, see the message about custom notation for long proofs that Patrick wrote above. It is relevant to our breakfast discussion at CIRM last month.

[Antoine Chambert-Loir]

In the ongoing proof of Sion/von Neumann minimax theorem (with @Anatole Dedecker ) we have similar constructions, we took them out of the proof using ‘private‘ definitions and lemmas, but a more systematic way would be simpler!

[Ralf Stephan]

Adam Topaz said:

It's a bit hard to read the diff on github with the link to the commit above due to all of the CI errors being placed inline in the diff. Does anyone know how to temporarily turn off those error messages?

For any PR or commit, just add ".diff" to the URL, like:
https://patch-diff.githubusercontent.com/raw/leanprover-community/mathlib4/pull/12297.diff
https://github.com/leanprover-community/mathlib4/commit/f0faf4e74da9efc027be869a8f130cb98c52e572.diff

[Oliver Nash]

Unexpected career changes have meant that I've spent very little time working on Mathlib's Lie theory in recent months. Nevertheless some progress has been made, e.g., we now know root spaces are 1-dimensional docs#LieAlgebra.IsKilling.finrank_rootSpace_eq_one.

[Oliver Nash]

We are also tantalisingly close to the really nice result that the roots of a Lie algebra are a docs#RootSystem. To be precise, the following two sorrys capture exactly what remains to be done:

import Mathlib.Algebra.Lie.Weights.Killing
import Mathlib.LinearAlgebra.RootSystem.Basic

noncomputable section

namespace LieAlgebra.IsKilling

open LieModule Module

variable {K L : Type*} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L]
  [IsKilling K L] [FiniteDimensional K L]
  {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [IsTriangularizable K H L]

def reflectRoot
    {α β : Weight K H L} (hα : α.IsNonZero) (hβ : β.IsNonZero) : Weight K H L where
  toFun := β - β (coroot α) • α
  weightSpace_ne_bot' := by
    /- Several proofs of this. Probably best (though not shortest) is
      Bourbaki, Ch. VIII §2.2 Lemma 1 (page 80 of English translation, 88 of PDF)

      Approximate plan:
        1. define exponential of nilpotent things (independent of Lie theory)
        2. prove exponential of element with nilpotent adjoint endomorphism gives `LieEquiv`
           (slightly more is true: exponential of any nilpotent `LieDerivation` gives `LieEquiv`)
        3. prove adjoint endomorphism of element of rootspace is nilpotent
        4. establish the identities in Bourbaki lemma 1 for `θ := exp e * exp (- f) * exp e`
           where `e` and `f` belong to an `sl₂` triple associated to `α` provided by
           `exists_isSl2Triple_of_weight_isNonZero`.
    -/
    sorry

lemma reflectRoot_ne_zero
    {α β : Weight K H L} (hα : α.IsNonZero) (hβ : β.IsNonZero) :
    (reflectRoot hα hβ).IsNonZero := by
  sorry

variable (H)

/-- The root system of a finite-dimensional Lie algebra with non-degenerate Killing form over a
field of characteristic zero, relative to a splitting Cartan subalgebra. -/
def rootSystem :
    RootSystem {α : Weight K H L // α.IsNonZero} K (Dual K H) H :=
  RootSystem.mk'
    IsReflexive.toPerfectPairingDual
    { toFun := (↑)
      inj' := by
        intro α β h; ext x; simpa using LinearMap.congr_fun h x  }
    { toFun := coroot ∘ (↑)
      inj' := by rintro ⟨α, hα⟩ ⟨β, hβ⟩ h; simpa using h }
    (fun α ↦ by simpa using root_apply_coroot α.property)
    (by
      rintro ⟨α, hα⟩ - ⟨⟨β, hβ⟩, rfl⟩
      simp only [Function.Embedding.coeFn_mk, IsReflexive.toPerfectPairingDual_toLin,
        Function.comp_apply, Set.mem_range, Subtype.exists, exists_prop]
      exact ⟨reflectRoot hα hβ, reflectRoot_ne_zero hα hβ, rfl⟩)
    (by convert span_weight_isNonZero_eq_top K L H; ext; simp)

end LieAlgebra.IsKilling

[Oliver Nash]

All the technology exists to close these sorries (I've even sketched an approach in a code comment) so I'm posting this here in case somebody fancies being the first person to formalise a really nice result.

[Johan Commelin]

This is really great!

[Johan Commelin]

For everybody interested, let me advertise the Github project that is tracking progress towards the classification of semisimple Lie algebras: https://github.com/orgs/leanprover-community/projects/17

[Andrew Yang]

I filled the second sorry just for fun

lemma reflectRoot_ne_zero
    {α β : Weight K H L} (hα : α.IsNonZero) (hβ : β.IsNonZero) :
    (reflectRoot hα hβ).IsNonZero := by
  intro e
  have : β (coroot α) = 0 := by
    apply add_left_injective (β (coroot α))
    simpa [root_apply_coroot hα, mul_two] using congr_fun (sub_eq_zero.mp e) (coroot α)
  have : reflectRoot hα hβ = β := by ext; simp [reflectRoot, this]
  exact hβ (this ▸ e)

[Andrew Yang]

Okay I have RootSystem {α : Weight K H L // α.IsNonZero} K (Dual K H) H and (rootSystem H).IsCrystallographic and (rootSystem H).IsReduced sorry free here and I can finally start doing what I should have been working on today.

[Oliver Nash]

No way, that's amazing! Not for the first time what I thought was a 100:1 shot at nerd-sniping worked. Thanks so much.

[Oliver Nash]

Of course now you must PR it :)

[Oliver Nash]

Incidentally your lemma coroot_injective essentially exists as coroot_eq_iff (this was only added to master yesterday so maybe you hadn't picked it up).

[Oliver Nash]

Anyway thanks again, this is marvellous and you've even established reduced and crystallographic which I hadn't asked for because I felt it would be too much.

[Johan Commelin]

Very cool!

[Andrew Yang]

First batch of PRs: #13258 #13259 #13260 #13261

[Johan Commelin]

#13265 proves that Lie algebras with non-degenerate Killing form are semisimple.

[Johan Commelin]

@Andrew Yang I kicked the middle two on the queue, and reviewed the 4th.

[Andrew Yang]

New PR: #13298

[Andrew Yang]

Final PR: #13307

[Johan Commelin]

Kudos to @Andrew Yang !

[Yaël Dillies]

Get it in in time for the Month in Mathlib!

[Johan Commelin]

There are two more subprojects of https://github.com/orgs/leanprover-community/projects/17/views/1 in progress. And they might land soon!

[Oliver Nash]

Thanks to Johan and Andrew's recent work we can now do things like this:

import Mathlib.Algebra.Lie.Weights.RootSystem
import Mathlib.Algebra.Lie.CartanMatrix
import Mathlib.Algebra.Lie.CartanExists

open LieAlgebra LieSubalgebra IsKilling

variable (k : Type*) [Field k] [IsAlgClosed k] [CharZero k]

-- These are admittedly non-trivial. Closing them would go a long way to removing any slight doubts
-- about the correctness of our `Matrix.ToLieAlgebra` definition.
instance : FiniteDimensional k (e₈ k) := sorry
instance : IsKilling k (e₈ k) := sorry

instance : IsCartanSubalgebra <| engel k <|
    Classical.choose <| exists_isCartanSubalgebra_engel k (e₈ k) :=
  Classical.choose_spec <| exists_isCartanSubalgebra_engel k (e₈ k)

-- Construct `e₈`, take a Cartan subalgebra, take the roots, and prove they are a root system.
#check rootSystem (engel k <| Classical.choose <| exists_isCartanSubalgebra_engel k (e₈ k))

which I think is quite satisfying.

[Junyan Xu]

I think @Mitchell Lee's work on Coxeter groups will allow the construction of a root system over an arbitrary field (if you have it over ℤ the you have it over any commutative ring) associated to a Coxeter matrix, e.g. CoxeterMatrix.E₈. We can then aim to show that both root systems are isomorphic. The faitufulness of the geometric representation would show every Weyl group is isomorphic to a Coxeter group.

[Johan Commelin]

Yes, I think we're on a roll!

[Johan Commelin]

feat(Algebra/Lie): Killing Lie algebras are semisimple #13265

[Johan Commelin]

This is now merged. Thanks @Oliver Nash for the reviews!

[Johan Commelin]

We do not yet have the notion of a base of a root system (simple roots) and the corresponding Cartan matrix, do we? Or maybe I missed something...

[Scott Carnahan]

We do not have the notion yet. I got a bit stuck here, because when you split an infinite root system into positive and negative cones, you can have a system of simple roots ("simple root" meaning a positive root that is not a nontrivial sum of positive roots) that is not linearly independent. Perhaps "base" should be reserved for the linearly independent case.

[Johan Commelin]

Aha! Thanks for illuminating the subtleties of the infinite-dimensional case

[Scott Carnahan]

I will try to spend more time on roots, since the rest of the classification seems to be progressing rapidly.