move p-adics

Stream: general

[Scott Morrison]

@Johan Commelin, @Rob Lewis, I was thinking about trying to move some of the less data like subdirectories out of data. padics seems a great candidate to move wholesale. But where exactly does it go? algebra? ring_theory?

[Johan Commelin]

I would vote for ring_theory. In my mind algebra is mostly for axiomatic typeclasses and their basic API.

[Adam Topaz]

We need a number theory folder

[Eric Wieser]

Should we be using default.lean to document what the subdirectories are for?

[Mario Carneiro]

I prefer readme.md in the directories, because those show up on github

[Eric Wieser]

I'm not sure that's all that useful; I'd expect most github viewers to jump to doc-gen for much beyond background information

[Scott Morrison]

Could we just incorporate README.md files into doc-gen? Seems an easy way to have best of both worlds.

[Scott Morrison]

I agree a number theory folder is a good idea, and padics could live there.

[Scott Morrison]

Another directory we could consider adding is commutative_algebra.

At the moment algebra/ring_theory/linear_algebra is pretty incoherent. I think we already have the right idea about what these should be:

• algebra: try to be nothing more than the typeclasses and immediate consequences of definitions (e.g. no "structure theory")
• ring_theory: everything beyond that about rings that is not already in a more specific category
• linear_algebra: everything about modules over fields/division rings

I think we could happily add commutative_algebra as a top-level directory, so that anything in ring_theory that is specifically about comm_ring goes in there?

Something I'm not sure about is where modules over rings that are not division rings naturally belong. Perhaps just under ring_theory.module and commutative_algebra.module? Currently everything there is stuffed into algebra, but I'd propose that only the definition and basic lemmas belong there.

[Johan Commelin]

"commutative algebra" is a well-established name, but is there a practical need to split between comm_alg and ring_theory?

[Scott Morrison]

Not necessarily. I've recently been doing some stuff on invariant basis number and the (strong) rank condition, mostly following Lam's book "Rings and Modules". Is this stuff commutative algebra or ring theory (or even representation theory)?

[Scott Morrison]

I guess the whole theory of noetherianity has to go under comm_alg, just because that's what the class/book is called when people learn it, even though much of it doesn't care about commutativity of the ring.

[Scott Morrison]

Another related question is where do polynomials belong? Certainly not in data. But perhaps not even in algebra, if we want to keep that to "axiomatics".

[Damiano Testa]

In my mind, seeing ring_theory and commutative_algebra, makes me think that the rings in ring_theory may not be commutative.

[Scott Morrison]

Yes, that would be my distinction --- I'd put all the stuff that works for noncommutive rings in ring_theory, and nothing that only works for commutative rings.

[Scott Morrison]

Perhaps polynomials even live in ring_theory?? Seems a bit weird.

[Damiano Testa]

I like the idea of polynomials in ring_theory, although several results about polynomials will (inevitably?) assume commutativity.

[Damiano Testa]

I think that there will have to be a non-commutative and a commutative part to polynomial rings. But this already will happen for rings, so that is probably ok, right?

[Johan Commelin]

I get the impression that in real life people reluctantly and lazily allow some non-commutative stuff to slip in under the comm_alg header.

[Johan Commelin]

Brauer group of a field... needs central simple algebras. They are so well-behaved that it's almost comm_alg, right?

[Damiano Testa]

Maybe people should think of defining a brauer group for division rings instead. :upside_down: That would definitely not go in commutative_algebra!

[Patrick Massot]

I fear this conversation will converge to "let's have a math folder". Things are simply too interleaved.

[Gabriel Ebner]

I think the only way to entangle this is to split up the folders, like ring_theory_0, ring_theory_1, etc.

[Johan Commelin]

ring_theory_37 is for the really advanced stuff :rofl:

[Damiano Testa]

Maybe we could have a regular "remove-a-commutative-assumption day", to get stuff about commutative slowly merge into not-necessarily commutative.

[Stu B22]

I don't wish to disrupt the discussion, but perhaps someday it will be worth considering a mapping relationship between mathlib folders and the "Mathematics Subject Classification" taxonomy
https://en.wikipedia.org/wiki/Mathematics_Subject_Classification.
Example of the MSC2020 taxonomy in use: https://www.zbmath.org/classification/
The mapping could be external to mathlib proper, e.g. a single external file that aligns mathlib elements with the MSC taxons.
But in cases where we have trouble deciding how to structure mathlib, perhaps it wouldn't be crazy to say "just follow MSC2020", at least structurally (not necessarily embedding the MSC alphanumeric coding into mathlib).

[Adam Topaz]

We could certainly add MSC identifiers in the module doc string, for example, and add some functionality in the doc generator to account for that

[Kevin Buzzard]

I think that an interface with MSC would be a valuable addition to Lean's maths library.

[Patrick Massot]

I have serious question. Is there any mathematician here who ever used the MSC taxanomy? It don't mean copy-pasting the codes from your previous paper (recursiverly going all the way back to your PhD advisor papers MSC codes that you copied in the first place) because journals ask for it. I've been doing that for 15 years and I still don't know the point.

[Mario Carneiro]

I usually find wikipedia links to be significantly more helpful than MSC codes

[Adam Topaz]

I think they're important for things like mathscinet, but, yes, I always copy/paste from somewhere else

[Patrick Massot]

Adam, do you use those codes when you use mathscinet?

[Patrick Massot]

I'm honestly curious. Maybe they are super useful and nobody ever taught me about it.

[Adam Topaz]

Nope! What I mean is that I think they use the codes to assign reviewers

[Patrick Massot]

Oh, that sounds plausible indeed.

[Adam Topaz]

I think some journals use these codes for the same reason as well...

[Sebastien Gouezel]

I never used these either.

[Sebastien Gouezel]

Fun fact: a few years ago, I was part of the creation of a new math journal. With the other founding editors, we decided that in our format we would request MSC numbers from the authors. I still don't know why, but since then we've been bugging all our authors with this :-)

[Patrick Massot]

I think we really shouldn't put any efforts into writing those codes in mathlib. If anyone has documentation energy we still have dozens (hundreds?) of files without any module docstrings.

[Scott Morrison]

I've proposed moving padics in #7771. (to number_theory/)

[Scott Morrison]

/poll Where should polynomial and mv_polynomial go?

[Scott Morrison]

Relatedly, I propose moving zmod and zsqrtd out of data; likely to the same place as polynomial.

[Adam Topaz]

Since we will soon have a number_theory folder, presumably they can go both in there?

[Scott Morrison]

My argument for ring_theory would be: polynomial is not just about the axiomatic consequences of the algebraic hierarchy, so doesn't belong in algebra, but they only care very mildly about commutativity (i.e. nothing "structural") so they don't belong in commutative_algebra.

[Scott Morrison]

We've actually had a number_theory folder for quite some time.

I agree zsqrtd belongs there! Less sure about zmod.

[Adam Topaz]

number_theory/elementary/zmod.lean?

[Scott Morrison]

I'd hate to have to draw the line between elementary and non-elementary number theory. :-)