pre-Lie algebras

Stream: new members

[Nikolas Tapia]

Hello! I'm Nikolas Tapia, postdoc at the Weierstrass Institute in Berlin. I work on rough paths and path signatures and became interested in Lean4 after hearing about it from a colleague in Oxford.

As a learning project I decided to try and implement pre-Lie algebras and prove a few facts about them.
I ended up mimicking Algebra.Lie and defined Lie-admissible rings as NonUnitalNonAssocRings such that their associator satisfies a certain identity (see e.g. [p. 587, MKL]), and showed that it implies that the canonical commutator yields a LieRing.
Then one can show that every PreLieRing is a LieAdmissibleRing and hence a LieRing. There are algebra versions of these facts as well.

I organised this in two files, which I plan to submit as two separate PRs.
Since I'm new to Lean4 I think some of the proofs can be improved or maybe even some of the conventions/definitions might not really fit the style.

In particular, I was unsure about whether it was sensible to define both left and right pre-Lie rings and show they are equivalent under op.

Thanks for such amazing software, I'm really loving it.

References
[MKL] Munthe-Kaas, H.Z., Lundervold, A. On Post-Lie Algebras, Lie–Butcher Series and Moving Frames. Found Comput Math 13, 583–613 (2013). https://doi.org/10.1007/s10208-013-9167-7

[Nikolas Tapia]

PR for pre-Lie algebras #28495

[Nikolas Tapia]

PR for Lie-admissible algebras #28496