Universal algebra

Stream: new members

[Hamza Maimoune]

Hello!
I would like to know if universal algebra would be interesting for Lean? It could factorize a lot of definitions such as closure, stability, morphisms and other stuff.
Kindly

[Mario Carneiro]

Universal algebra would be interesting to investigate, but I would put a big warning if you are investigating this for refactoring purposes, because there is a much higher bar for usability in this case. Just because something is a special case of something else in maths doesn't mean it is actually useful as a generalization in formal maths

[Mario Carneiro]

It doesn't hurt to formalize the general theory and look into applications when it is already mostly fully formed, though. What is the actual scope of theorems that can be proven in this context?

[Hamza Maimoune]

What do you mean by higher bar of usability?

[Mario Carneiro]

I mean that it shouldn't be harder to apply the general theorem in the specific instance than it is to prove the theorem directly in the specific instance

[Mario Carneiro]

the shallower the theorems and the more convoluted the generalization the harder it gets to meet this criterion

[Mario Carneiro]

The best generalizations are those where the application overhead is minimal and there are still nontrivial theorems to be had. Things like the elementary theory of rings and groups are good examples of this

[Johan Commelin]

@Hamza Maimoune As a crazy example: in Lean we have the notion of group and add_group. And we automatically duplicate all theorems about groups to theorems about additive groups.
The only difference: notation

[Hamza Maimoune]

Did you copy paste the theorems?

[Mario Carneiro]

Basically (in an automated way)

[Mario Carneiro]

This is done in order to minimize application overhead

[Mario Carneiro]

Even though the theories of multiplicative and additive groups are obviously isomorphic, the application overhead of using an additive theorem on a multiplicative group via a translation is sufficiently high that it is easier to just prepare all the theorems in both contexts

[Hamza Maimoune]

Therefore, universal algebra would induce a lot of application overhead? If we would implement it, we wouldn't use it to deduce properties on specific algebras, right?

[Mario Carneiro]

I'm not saying it necessarily would, only that if you are seriously targeting using it to generalize existing theorems you have to pay very close attention to application overhead and do everything you can to keep it reasonable

[Mario Carneiro]

You don't necessarily have to worry about this for the first pass, though. When setting up the initial theory, just do things in the mathematically natural way, and leave application to specific algebras until later

[Mario Carneiro]

But easy application to diverse fields is certainly not something that happens for free unless you prepared everything with this in mind beforehand

[Hamza Maimoune]

Okay thank you for your answer

[Hamza Maimoune]

I'll try to dive into this to see if there is anything useful

[Patrick Massot]

@Hamza Maimoune there are two subtly different things here.

In the real world, almost no mathematicians knows anything about universal algebras, because they are not useful for real world mathematics: the benefits are not worth the effort. This fact is not necessarily relevant to formal mathematics. In the real world almost nobody knows about filters. The benefits are not worth the efforts because mathematicians in the real world have no trouble at all saying that everything they prove for limits of sequences hold, mutatis mutandis, for limits of functions etc. But in the formal mathematics world, filters are definitely worth the effort. So it could be that universal algebras are worth the effort in formal mathematics.

But now comes the second aspect of the discussion. Formalized mathematics happen in a formal context, here a flavor of dependent type theory, and in a given software, say Lean but the same would apply elsewhere. Hence there are usability issues, coming from flaws in the foundational theory or in the software. And this has to be weighted against the theoretical benefits. For filters everything is very usable. They blend easily into type theory, and translating back and forth between filters and epsilons is very easy. Hence they are everywhere in formalized maths. Proving theorems about limits of sequences of real numbers as special cases of super abstract theorems about filters is very easy.

Now consider abstract category theory. It's mostly useless in the real world of course (but nice to play with!). In mathlib we have a huge library of category theory, which comes with an gigantic usability barrier. As far as I know, we still have a total of zero specific lemma proved using a general theorem from the category theory library.