# Zulip Chat Archive

## Stream: general

### Topic: mathlib algebra organisation

#### Kevin Buzzard (Nov 23 2020 at 09:38):

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 (Nov 23 2020 at 09:45):

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 (Nov 23 2020 at 09:45):

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

#### Johan Commelin (Nov 23 2020 at 09:47):

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

#### Eric Wieser (Nov 23 2020 at 09:48):

That difference suggests to me that `group_theory/group_action/defs.lean`

belongs under `algebra`

somewhere?

#### Reid Barton (Nov 23 2020 at 09:48):

This particular reorganization might be complicated by the fact that `data.nat.basic`

imports `algebra.group_power.basic`

#### Reid Barton (Nov 23 2020 at 09:49):

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 (Nov 23 2020 at 09:50):

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

#### Reid Barton (Nov 23 2020 at 09:52):

Perhaps the name `group_power`

should change to just `power`

#### Johan Commelin (Nov 23 2020 at 09:57):

Eric Wieser said:

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

Does `leanproject`

s import graph give you what you are looking for?

#### Johan Commelin (Nov 23 2020 at 09:57):

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 (Nov 23 2020 at 09:58):

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 (Nov 23 2020 at 09:59):

Maybe `data.nat.basic`

should be split?

#### Reid Barton (Nov 23 2020 at 10:00):

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 (Nov 23 2020 at 10:02):

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 (Nov 23 2020 at 10:08):

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 (Nov 23 2020 at 10:09):

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 (Nov 23 2020 at 10:10):

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

Last updated: May 14 2021 at 22:15 UTC