mathlib algebra organisation

Stream: general

[Kevin Buzzard]

The innocuous-looking #5083 has now morphed into a suggestion that some material in algebra/group_power be reorganised. As a random example, all this stuff is about linearly ordered rings and semirings, so one might argue that algebra/group_power/basic.lean is perhaps not the right place for it any more (my memory of how this occurred was that a robust theory of powers was introduced after all the monoid/group/ring machinery was set up, and it was all thrown together in one file). Note also that algebra/group_power/basic imports deprecated.group and this might be a good chance to remove this import.

So I'm thinking about how this stuff could be redistributed. The first question which springs to my mind is "why the heck do we even have the directory algebra/group_power (containing basic.lean, a basic theory of $a^n$ for n : nat and a in a monoid, group, monoid with 0, ring, canonically ordered semiring, linear ordered semiring, and also $g^m$ for m : int in the special case where g is in a group, and identities.lean which contains no groups whatsoever)? Can this directory be nuked, and the files in it be broken up and placed in more appropriate places? The main reason I need to ask this is that I don't understand the import heirarchy, it's never something I've paid any attention to because I usually work at the "ends" of mathlib, e.g. writing MSc algebra which just imports everything. Why do we have no algebra/monoid? Why do we have algebra/group and also group_theory? Is this all to do with imports?

In short then, is the idea that algebra/group_power be nuked and the results moved to, say, algebra/group/power.lean and algebra/ring/power.lean a reasonable one? (or group_theory/power.lean?) Note that we have algebra/group_with_zero/power.lean which contains a ton of results about monoids with zero, objects which are more primitive than rings (indeed a ring, or even a semiring, is a monoid with zero).

[Johan Commelin]

The difference between algebra/group and group_theory is that everything in algebra/* should be the basic things that follow directly from the axioms and that typically don't get written down in maths books. (Apart from the definitions, and basic lemmas on the two pages after that)
So Sylow goes in group_theory, but the fact that (x * y) ^-1 = y^-1 * x ^-1 goes in algebra/group/*

[Johan Commelin]

That's my idealistic understanding of the separation. But this breaks down in 37 places (at least)

[Johan Commelin]

Your "nuke-the-powers" proposal sounds good to me.

[Eric Wieser]

That difference suggests to me that group_theory/group_action/defs.lean belongs under algebra somewhere?

[Reid Barton]

This particular reorganization might be complicated by the fact that data.nat.basic imports algebra.group_power.basic

[Reid Barton]

I made algebra.group_power.basic to be basically "stuff about $a^n$ and $g^m$ that can be done without importing data.nat.basic"

[Eric Wieser]

How hard would it be to get a visualization of the import heirarchy in the mathlib docs?

[Reid Barton]

Perhaps the name group_power should change to just power

[Johan Commelin]

Eric Wieser said:

How hard would it be to get a visualization of the import heirarchy in the mathlib docs?

Does leanprojects import graph give you what you are looking for?

[Johan Commelin]

The problem with rendering it in the docs, is that the full graph is huge. So it's better to pass some options on the command line, and get a manageable graph.

[Johan Commelin]

Eric Wieser said:

That difference suggests to me that group_theory/group_action/defs.lean belongs under algebra somewhere?

Probably yes. This must be one those 37 places where the ideal separation broke down :rofl:

[Johan Commelin]

Maybe data.nat.basic should be split?

[Reid Barton]

I guess this line of thought just seems like stirring up trouble to me unless there is some concrete goal in the end

[Eric Wieser]

The problem with rendering it in the docs, is that the full graph is huge

I think I got fed up of waiting last time I asked lean to produce the full graph for mathlib...

[Kevin Buzzard]

I linked to #5083 already, which is a clear indication that there is no concrete goal here. It was just an idle late-night suggestion by Sebastien, and the realisation that I didn't really know what I was doing when it came to implement it. I certainly don't want to plough in and make matters worse.

[Reid Barton]

Somehow the underlying problem is that we have to use files at all, which forces us to decide whether lemma zero_pow [monoid_with_zero R] : ∀ {n : ℕ}, 0 < n → (0 : R) ^ n = 0 is "about the power operation" or "about monoid_with_zero"

[Johan Commelin]

Brings me back to unisonweb.org and content addresable storage...