Experiments with algebra

Stream: mathlib4

[Julien Marquet]

Hello,
During the past few days, I have worked on some basic group theory in Lean 4, and since there is an open debate on how to port algebra to Lean 4, I thought that some things that I have done in my repo might be interesting. The main point is that I have tried a slightly different approach than that of mathlib 3, and I also used some of the new features of Lean 4 : improved coercion and notations.
All this is detailed in the _readme_ of my repo (which I don't paste right here to not flood the channel)

Hope you will find this interesting !

REPO : https://github.com/thejohncrafter/playlean4

[Kevin Buzzard]

So you have fully bundled groups? I think that there are some problems which the Coq people experience with this approach and which we don't have in Lean, but I don't know what these problems are.

[Julien Marquet]

I'm far from having group theory, but what I got looks promising to me (yet I don't believe it is mathlib-worthy for the moment, it is still possible that I hit a wall at some point). The main problem that I encountered as of now is the way Lean handles notation, and it can be solved with metaprogramming, but I didn't experiment enough to be sure my approach is viable.

---

Here's a more detail :

I have fairly complicated objects that I'm able to define easily enough, for instance cosets and canonical actions on cosets. This allows me to prove that a subgroup is normal iff it is the kernel of a morphism.
If you look at the code (by the way, according to the timestamps, you missed my latest commit where I entierely move the laws of groups outside of any typeclass), everything is pretty straightforward : no complicated management of instances/corecions/anything (that's mainly thanks to Lean 4 :tada:).
A great part of the code is actually just definitions of namespaces and instantiations of objects. Yet at the moment I have to perform hacks like here too often, which is a pain and means my approach is not "mathlib-worthy" for now, but this could easily be solved by metaprogramming, and maybe a hint of hacking in Lean (hopefully...).
There is one other problem that I can't avoid (and that may actually be structurally unavoidable) : I often have to refer explicitly to some instance of Group when I do things that are not obvious enough to Lean. See here, where I have to use explicitly grp.invertible instead of invertible. That is because (I guess) when I only use invertible Lean can't know which group law I want to refer to (even though, in this context, there obviously is only one possible law), so it asks for an explicit call.

[Eric Wieser]

Without having thought about it much, it seems odd to bundle 1 but not (*) into Group.

[Julien Marquet]

I do this because 1 is uniquely defined once we have a group law. Same for inverse, it is unique so I can just make Group give it to me once I give the law.
The other, more trivial benefit is that I do not need to add an argument like one : G each time I instantiate a group, but doing it wouldn't actually be a problem modulo metaprogramming.
But sure, this is a bit unnatural if we consider the full algebraic hierarchy : for instance we might want to specify the unit alongside the law when we're dealing with monoids :)