Engel's theorem?

Stream: maths

[Nicolás Ojeda Bär]

Hello, I want to get my feet wet with mathlib (have some experience with Coq and my background is PhD in number theory). I thought about tackling Engel's theorem since a lot of the background about Lie algebras seems to be in place. But I wanted to check beforehand, in case this is already done/someone is working on this/there is some blocking issue that is pending/etc... Comments appreciated, thanks!

[Oliver Nash]

This would be great!

[Oliver Nash]

I already have various bits and pieces of this formalised and was planning to get back to them for a final but I'd be delighted to see someone else do it instead. I enthusiastically encourage you to go ahead!

[Oliver Nash]

Note that we already have this bit which you'll need early on: https://github.com/leanprover-community/mathlib/blob/03ddb8dd343a0dca6cd66470eaf3f40ce933876b/src/algebra/lie/nilpotent.lean#L228

[Oliver Nash]

Also, note that Engel's theorem requires a finite dimensionality. So far in the Lie algebra theory, I've tried to avoid unnecessary assumptions on the coefficients but for Engel's theorem I think we should probably just start working over a field.

[Oliver Nash]

I tried to come up with an argument that worked with just Noetherian assumption but as far as I can see it's necessary to have the descending chain condition too (though I admit I haven't cooked up a counterexample). So it seems to me that the result needs both ACC and DCC.

[Oliver Nash]

Having both ACC and DCC is of course just the theory of finite-length modules but we do not have this and I couldn't motivate myself to develop this just so I can prove Engel more generally.

[Oliver Nash]

Finally you should note that we have the concept of nilpotency for Lie modules, not just Lie algebras. I think this will actually work out pretty neatly for Engel's theorem. The usual statement has two bits: one about algebras being nilpotent, and one about modules carries a non-zero vector that is killed by the action of the algebra. However I think the right statement is just that modules are nilpotent with this expanded definition that we have.

[Oliver Nash]

And then this covers nilpotency of algebras (since they are modules over themselves) and gives the non-zero simultaneous zero eigenvector bit for modules since the last non-zero term in the lower central series will consist of such vectors.

[Oliver Nash]

IMHO the next step could be any of:

• Develop theory of finite-length modules [or just ignore this and work over a field]
• Show that a nilpotent module always has a non-zero simultaneous zero eigenvector
• Show that central extensions of nilpotent modules are nilpotent

but feel free to do whatever you think is best.

[Johan Commelin]

@Nicolás Ojeda Bär Welcome! Sounds like an awesome project to me, if you already have some experience with ITP's

[Kevin Buzzard]

Hi @Nicolás Ojeda Bär ! If you want a starter problem you could formalise the theory of finite length modules over a ring :-) The key theorem we'll need is that if M is an R-module with a submodule N then the length of M equals the sum of the lengths of N and M/N.

[Nicolás Ojeda Bär]

Kevin Buzzard said:

Hi Nicolás Ojeda Bär ! If you want a starter problem you could formalise the theory of finite length modules over a ring :-) The key theorem we'll need is that if M is an R-module with a submodule N then the length of M equals the sum of the lengths of N and M/N.

This sounds like a neat and tidy chunk of work; I'll give it a shot. Thanks for all the background information, it is appreciated!

[Kevin Buzzard]

Feel free to ask me or Oliver if you have any questions -- Engel's theorem would be a really cool thing to work on and all the foundations are there.

[Johan Commelin]

Note that for the N -> M -> M/N stuff, it would be good to make this as general as possible. In other words, use an arbitrary short exact sequence, in stead of explicit submodules and quotients.

[Nicolás Ojeda Bär]

Johan Commelin said:

Note that for the N -> M -> M/N stuff, it would be good to make this as general as possible. In other words, use an arbitrary short exact sequence, in stead of explicit submodules and quotients.

But always working in the category of modules, right? Or do you have something more general in mind (abelian/exact categories)?

[Johan Commelin]

ooh, yes, I would do it with R-modules for now

[Johan Commelin]

open function

variables {R : Type*} [comm_ring]
variables {M M' M'' : Type*} [add_comm_group M] [add_comm_group M'] [add_comm_group M'']
variables [module R M] [module R M'] [module R M'']
variables (f : M' \rl[R] M) (g : M \rl[R] M'') (hf : injective f) (hg : surjective g)

include hf hg

[Johan Commelin]

Something like that. Where \rl expands to $\to_l$ in VScode.

[Nicolás Ojeda Bär]

Got it, thanks!

[Kevin Buzzard]

Actually this might be much thornier than I thought for a beginner because it involves developing an API for a definition (the length of a module) as opposed to just using it.

[Kevin Buzzard]

One is going to need the fact that all saturated chains have the same length which will be quite messy to do formally.

[Nicolás Ojeda Bär]

Kevin Buzzard said:

Actually this might be much thornier than I thought for a beginner because it involves developing an API for a definition (the length of a module) as opposed to just using it.

I assumed (didn't actually check it) that a similar "API" already exists for finite-dimensional vector spaces, so I was planning to imitate that...

[Nicolás Ojeda Bär]

Kevin Buzzard said:

One is going to need the fact that all saturated chains have the same length which will be quite messy to do formally.

I was planning to show as follows (I hope the argument is correct): given a saturated chain of length n in a module, every consecutive subquotient has length 1, and then use additivity of lengths to show that the i-th element of the chain has length i (and thus the chain itself has length equal to the length of the module). I was hoping that the fact that every subquotient has length 1 and the additivity of lengths would follow from the definitions and the basic properties of sub/quotient modules (but haven't checked).

[Patrick Massot]

The API for dimension of a vector space is not so easy to use because of the existence of both the cardinal and the natural number versions.

[Nicolás Ojeda Bär]

Ok, that doesn't yet make sense to me because I haven't looked at the details of the relevant definitions, but I keep it in mind.
On another subject: is there any existing work for filtrations in mathlib?

[Oliver Nash]

I'm
Nicolás Ojeda Bär said:

On another subject: is there any existing work for filtrations in mathlib?

I don't think so but I believe they are needed for the Liquid Tensor Experiment and might be en route to Mathlib from there: https://github.com/leanprover-community/lean-liquid/search?q=filtration

[Oliver Nash]

(Mind you I only follow LTE at a great distance so I'm not at all sure.)

[Johan Commelin]

The filtrations for LTE are of a different kind then the ones usually encountered in commutative algebra. We filter a group object by compact subspaces, where as usually one filteres by submodules.
The compact subspaces in LTE are not closed under addition.

[Johan Commelin]

@Nicolás Ojeda Bär I think it's also completely fine to follow Oliver's initial suggestion, and to just prove Engel's theorem over fields.

[Kevin Buzzard]

Yes, this was rather more of a complicated detour than I had imagined!

[Eric Wieser]

I made a half-hearted attempt at defining filtration here: https://github.com/pygae/lean-ga/blob/master/src/for_mathlib/algebra/filtration.lean

[Eric Wieser]

Looking at it again though, I think my map_add axiom might be too strong, and should be only ≤ not =

[Kevin Buzzard]

Yes, you want $R[T^2,T^3,T^4,\ldots]$ (polynomials with no degree 1 term) to be filtered by the naturals (by degree), but $F_1^2$ is smaller than $F_2$.

[Eric Wieser]

Somehow I was able to see that there could in principle be no degree-one terms without being able to make that obvious construction from polynomials - thanks!

[Kevin Buzzard]

It's not at all obvious that this gives a ring until someone points it out! I remember it weirding me out as an UG.

[Kevin Buzzard]

In fact this turns out to be some standard construction in algebraic geometry, e.g. the spectrum of the subring $\mathbb{C}[T^5,T^8]$ of $\mathbb{C}[T]$ is a model of a singularity which these people might want to study, and this has random missing parts of small degree but then becomes normal around T^28.

[Kevin Buzzard]

Note: @Chris Hughes might be developing a theory of finite length modules.

[Oliver Nash]

Cross-linking this project for anyone who finds this thread.

[Oliver Nash]

Oliver Nash said:

IMHO the next step could be any of:

• Develop theory of finite-length modules [or just ignore this and work over a field]
• Show that a nilpotent module always has a non-zero simultaneous zero eigenvector
• Show that central extensions of nilpotent modules are nilpotent

but feel free to do whatever you think is best.

I've just pushed #11422 addressing the third item above. If I have enough time over the weekend I might just prove the rest of the theorem.

[Oliver Nash]

I've just pushed #11515 addressing the second item above.

[Oliver Nash]

We now have a PR containing this result: #11922

I became slightly obsessed with proving it using only minimal assumptions so it was rather more work than it might have been. The PR above depends on all of #11515, #11625, #11819, #11820, #11822, #11823, #11826, #11828, #11831, #11852, #11853, #11854 (though not actually on #11422 because I did not use the standard argument).

[Patrick Massot]

Did you manage to find someone who could talk with you about this general setup?

[Patrick Massot]

Or is everyone around you knowing only the field case?

[Oliver Nash]

I didn't speak to anyone about it. (Edit: I did mention I was doing this to Kevin.)

[Oliver Nash]

I think the group theorists and non-associative algebra people like Zelmanov study Lie rings and work at this level of generality but I didn't make contact with anyone.

[Oliver Nash]

It was a fun little journey where I started out utterly unsure about how weak one could make the assumptions. It's all obvious to me now but several weeks ago it was not.

[Patrick Massot]

I think it would be good to talk to some expert about this.

[Oliver Nash]

Note that I did find this old paper of Zorn (referenced in the PR): https://projecteuclid.org/journals/bulletin-of-the-american-mathematical-society-new-series/volume-43/issue-6/On-a-theorem-of-Engel/bams/1183499839.full

[Oliver Nash]

Patrick Massot said:

I think it would be good to talk to some expert about this.

To make sure my doc string remarks are accurate? I'd be happy to ask someone. Any idea who?

[Johan Commelin]

I could chat about it with Wolfgang Soergel. He is in the office on the opposite side of the corridor to mine. And he seems to find Lean a fun experiment.

[Johan Commelin]

I'll see if he's around tomorrow, when I'm going to the institute again.