The plan for PBW theorem

Stream: mathlib4

[Wang Jingting]

Hi! We have been thinking about the formalization of Poincare-Birkhoff-Witt theorem for a while, and some preparations on Filtered ring/algebra and associated graded ring/algebra are recently being PRed to mathlib and is still under review.

But there are several questions that still confuse me while we prepare for the formalization, and I would really like to get some suggestions from here.

1. How general should we attempt to state the result, and what proof should we follow? Some of the proofs we've been looking at are: (1) the classical proof from Humphrey's book about Lie Algebra, which proves the theorem when the coefficient ring R is a field; (2)A later proof by P.J Higgins, which showed that the result holds when R is a Dedekind domain or the lie algebra is a free module and several other cases... (I came across this proof on MathOverflow)
   Both proofs are not very easy to formalize as they involve a lot of concrete calculations, the second one is a longer proof and introduces some algebraic structures that I'm not sure whether we want that.

2. Are there any general suggestions on how we can decompose the task to collaborate better? It sure seems like (to me) a relatively large thing to formalize, so I think smoother collaboration will be very helpful to the project.

Thanks for your suggestions in advance!

[Johan Commelin]

On MO I found a link to https://arxiv.org/pdf/1804.06485 which deals with a very abstract setup. The application to Lie algebras is maybe not completely straightforward, but I think it might be interesting to spend a few minutes considering it.

[Oliver Nash]

Regarding your question 1, even PBW with just field coefficients would be great, and a very welcome addition to the library.

Regarding how generally to work the following are the factors that I tend to bear in mind:

• Applications of the result. What generality do you need to cover them all? Even if they are covered, can you make life easier for downstream users by weakening / dropping an assumption? (E.g., we proved Engel's theorem quite generally and this obviates the need to assume field coefficients for a host of downstream results.)
• Ancillary benefits to Mathlib. Will the extra work require developing theory which will be valuable its own right. (E.g., we have some results for Lie modules under some Artinian + Noetherian assumptions. This is quite ridiculous from the POV of Lie theory but did force us to fill in some API for Artinian / Noetherian modules which should benefit people doing commutative algebra.)
• Personal appetite / curiosity. Sometimes one is just curious about generality.
• Effort required. Often I'm happy to do maybe 2x or 3x the work even for a smallish win in terms of generality but I'd need a big win to justify 10x or more.

It's always a bit of a guess though: for PBW I can't really give great answers to these so I'll just repeat my remark that even just field coefficients would be great.

[Oliver Nash]

Regarding your question 2, the gold standard is setting up a Blueprint using @Patrick Massot 's software. Making a good blueprint is a huge amount of work though.

There is also the possibility to use a GitHub Project. Again making a good project is a huge amount of work but even a very tiny one can be valuable. E.g., before I got pulled into other work, I spent about two hours setting one up last year and it has certainly paid me back multiples of the time I took to create it in terms of contributors.

[Wang Jingting]

Thanks for the suggestions! I've been trying to set up a blueprint and hopefully it will work. I didn't really get what the abstract setup is about, so we'll probably still stick to the concrete version anyway. By the way, our professor also suggested a proof by Braverman and Gaitstory, which seems to prove something similar with a generalization to Weyl and Clifford algebra.

[Oliver Nash]

Formalising this paper would be awesome, especially as it would bring many benefits to the library beyond the PBW theorem itself.

You should be aware it would also be quite a non-trivial undertaking. E.g., it casually uses Hochschild cohomology: setting this up would be a sizeable project in its own right.

[Scott Carnahan]

You may be interested in Bergman's "The diamond lemma for ring theory", which gives a proof of PBW in terms of reduction rules - one finds that the Jacobi identity is equivalent to the vanishing of reduction ambiguities.