Cyclic Groups need Ring

Stream: mathlib4

[Filippo A. E. Nuccio]

I am stumbling upon this error

import Mathlib.GroupTheory.SpecificGroups.Cyclic

assert_not_exists Ring -- Declaration Ring is not allowed to be imported by this file.

and I believe that there is something that should be done, no? Looking at the error, it seems that it comes from a path

Mathlib.Algebra.Ring.Hom.Defs,
which is imported by Mathlib.Data.Nat.Cast.Basic,
which is imported by Mathlib.Algebra.CharP.Defs,
which is imported by Mathlib.Algebra.CharP.Lemmas,
which is imported by Mathlib.Algebra.CharP.Two,
which is imported by Mathlib.Data.Nat.Totient,
which is imported by Mathlib.GroupTheory.SpecificGroups.Cyclic

and I kind of imagine that when speaking about cyclic groups we want to access the totient function, yet that to speak about cyclic groups we need rings seems problematic. Is it not?

[Yaël Dillies]

Agreed! I've been working on similar issues ("order of an element" needs rings), and it is never super easy to know what to do

[Filippo A. E. Nuccio]

Indeed I was typing @ Yaël...

[Yaël Dillies]

In that case, the suspicious import is Algebra.CharP.Two → Data.Nat.Totient IMO. Basic results about the totient function should need no algebra at all!

[Yaël Dillies]

Do you want to give it a go? Otherwise I have a freshly spun out gitpod and another 30min of sunlight before I can go to bed

[Filippo A. E. Nuccio]

For the context: I am trying to add some cyclicity properties to Mathlib.Algebra.GroupWithZero.Int.lean but it starts with a assert_not_import Ring and then it complains.

[Filippo A. E. Nuccio]

Yaël Dillies said:

Do you want to give it a go? Otherwise I have a freshly spun out gitpod and another 30min of sunlight before I can go to bed

Here sun is down, so if you want to go feel free! Otherwise I can try to do something (but picking up where you left it once you called it a night is also a nice option :angel: ).

[Filippo A. E. Nuccio]

Just tell me what you prefer.

[Yaël Dillies]

Filippo A. E. Nuccio said:

For the context: I am trying to add some cyclicity properties to Mathlib.Algebra.GroupWithZero.Int.lean but it starts with a assert_not_import Ring and then it complains.

This is a very good stress test of our import sanitisation whether we can do this or not. Right now I can tell you: it will be a solid amount of work

[Eric Wieser]

yet that to speak about cyclic groups we need rings seems problematic.

What's the argument here? Certainly the fact that groups are "simpler" than rings doesn't imply that all "$X groups" are simpler than "$Y rings". For cyclic groups, I would expect it to become handly to know that the integers and naturals form a (semi)ring.

[Filippo A. E. Nuccio]

(deleted)

[Filippo A. E. Nuccio]

Yaël Dillies said:

Filippo A. E. Nuccio said:

For the context: I am trying to add some cyclicity properties to Mathlib.Algebra.GroupWithZero.Int.lean but it starts with a assert_not_import Ring and then it complains.

This is a very good stress test of our import sanitisation whether we can do this or not. Right now I can tell you: it will be a solid amount of work

Yes, this I imagine.

[Yaël Dillies]

Eric, this reasoning is very dangerous, because empirically everyone says "Oh but to prove this why don't you that first? Makes the proof much easier", and soon enough you're stuck in a long chain of imports cycling through the same few folders in a seemingly random order

[Filippo A. E. Nuccio]

Eric Wieser said:

yet that to speak about cyclic groups we need rings seems problematic.

What's the argument here? Certainly the fact that groups are "simpler" than rings doesn't imply that all "$X groups" are simpler than "$Y rings". For cyclic groups, I would expect it to become handly to know that the integers and naturals form a (semi)ring.

I think that the argument is what Yael calls import sanitisation... at any rate, I believe that at least the basics about cyclic groups are really independent of any (semi)ring theory, I would have nothing against seeing them show up in e.g. classification theorems, but not below, no?

[Filippo A. E. Nuccio]

That being said: if anything interesting about cyclic groups needs ring, we should re-think the assert_not_exists Ring in the basics about GroupWithZero.Int: and there I perhaps agree with Eric that importing Ring when speaking about Int (or the WithZero-ification) is probably ok.

[Yaël Dillies]

Really, the group vs group with zero vs ring vs ... distinction I've been pushing for is kind of arbitrary, but the point is that:

1. It is easy for humans to evaluate where a result lies in the hierarchy
2. It is easy for Lean to yell at humans when they mess with the distinction, eg assert_not_exists or the forbidden folder imports linter
3. It at least somewhat matches the order in which things are taught to an undergrad. I myself sat through a course named "Groups, Rings and Modules", and the material was indeed covered in that precise order, with no back and forth

[Filippo A. E. Nuccio]

I basically agree, but allow me a slightly provocative question (I told you sun is down... :wine: :smirk: ): for 3., are you sure your teacher never multiplied two integers when discussing some nice properties of Int as a (cyclic) group?

[Filippo A. E. Nuccio]

(I am much older, so memory is probably not serving well, but concerning my GRF course I cannot swear that this has not been used).

[Yaël Dillies]

Sure they did! but they didn't need to appeal to the fact that the properties of multiplication over ℤ (and its interaction with addition) are more general phenomena pertaining to rings. Instead they wrote them down and went on with the course.

[Filippo A. E. Nuccio]

(And I am now frantically checking all the notes about my lectures to check what I did... :sweat_smile: :note: )

[Filippo A. E. Nuccio]

Yaël Dillies said:

Sure they did! but they didn't need to appeal to the fact that the properties of multiplication over ℤ (and its interaction with addition) are more general phenomena pertaining to rings. Instead they wrote them down and went on with the course.

But that becomes a nightmare, no? Are you suggesting that we prove stupid ring-theoretical results on Int without appealing to the Ring library to avoid the import?

[Yaël Dillies]

This is a useful attitude to adopt in the Lean ecosystem too because you don't want to be telling the computer scientists "Well you can't multiply together two indices without importing mathlib because hum well you know multiplication is mathematics"

[Filippo A. E. Nuccio]

(Just to be clear: I agree 100% that there is something to be done, just trying to understand what).

[Filippo A. E. Nuccio]

I know that this seems pure laziness: but is "just remove assert_not_exists Blah on the go, after informed discussions on Zulip" too easy? EDIT as @Eric Wieser rightly points out, this must go hand-in-hand with "and link to that discussion in the commit message"

[Filippo A. E. Nuccio]

It certainly has the terrible drawback of being basically irreversible

[Yaël Dillies]

Filippo A. E. Nuccio said:

But that becomes a nightmare, no? Are you suggesting that we prove stupid ring-theoretical results on Int without appealing to the Ring library to avoid the import?

If the result is truly ring-theoretical, then it is not basic. Of course, I am implying that one can and should draw a line between "basic algebra" and "ring theory". In practice, there seems to always be an obvious answer

[Yaël Dillies]

Filippo A. E. Nuccio said:

I know that this seems pure laziness: but is "just remove assert_not_exists Blah on the go, after informed discussions on Zulip" too easy?

Not sure what you mean exactly, but certainly one shouldn't remove assert_not_exists Ring from Algebra.GroupWithZero.Blah. Instead, one should move the relevant results to Algebra.Ring.Blah.

[Filippo A. E. Nuccio]

Yaël Dillies said:

Filippo A. E. Nuccio said:

I know that this seems pure laziness: but is "just remove assert_not_exists Blah on the go, after informed discussions on Zulip" too easy?

Not sure what you mean exactly, but certainly one shouldn't remove assert_not_exists Ring from Algebra.GroupWithZero.Blah. Instead, one should move the relevant results to Algebra.Ring.Blah.

Well, I dare to disagree. If the relevant results concern the GroupWithZero structure of Blah, the fact that somewhere uphill a Ring has been used should not make them fall in Ring.Blah.

[Filippo A. E. Nuccio]

Of course, changing the proof above so that it does not import Ring anymore is a good option; but then @Eric Wieser 's objection fires: if we're speaking about (cyclic) groups and we end up using, in an ancillary way, something about rings, it is perhaps safe to allow this import.

[Filippo A. E. Nuccio]

This is what I meant by "removing on the go": on a case-by-case analysis, say something like "to prove Y, although in principle we don't need X and we enforced a assert_not_exists X , it is actually handy to allow the X-theory: so let's remove the assert_not_exists."

[Eric Wieser]

Filippo A. E. Nuccio said:

I know that this seems pure laziness: but is "just remove assert_not_exists Blah on the go, after informed discussions on Zulip" too easy?

In general I think assert_not_exists is a mechanism to ensure discussion and thought happens; if they were meant to be hard rules, then they ought to require an explanation next to each one!

[Filippo A. E. Nuccio]

Excellent point

[Eric Wieser]

I think "and link to that discussion in the commit message" is another important part that you didn't mention

[Yaël Dillies]

They are meant as hard rules and registered as such centrally in Algebra/README.md

[Yaël Dillies]

(please read it!)

[Filippo A. E. Nuccio]

(I am reading it: but would it been accessible from the doc webpage?)

[Eric Wieser]

Yaël Dillies said:

They are meant as hard rules and registered as such centrally in Algebra/README.md

Either this should be in the docstring of assert_not_exists, or it should be a comment on each use in algebra

[Yaël Dillies]

I do think that's a made-up rule, Eric. Discussion on Zulip will point to the README, end of the story.

[Yaël Dillies]

Sadly it is currently not. I tried to ignite a discussion on making those README files be considered by doc-gen, but nothing came out of it

[Filippo A. E. Nuccio]

Yaël Dillies said:

They are meant as hard rules and registered as such centrally in Algebra/README.md

I have read it: and with all the due respect, I still believe that Eric has a point: these should not be hard rules (even if they've been written/suggested with a good idea in mind).

[Eric Wieser]

Yaël Dillies said:

That's a made-up rule, Eric.

I wasn't saying this was a rule, I was saying that if what you say really is a rule, surely we want to communicate it more directly than waiting for a human to point the reader to a per-folder readme file via Zulip?

[Jz Pan]

Yaël Dillies said:

Sadly it is currently not. I tried to ignite a discussion on making those README files be considered by doc-gen, but nothing came out of it

If you use README.lean instead, then it will be considered by doc-gen under current code framework without modifications

[Yaël Dillies]

Yes but then these files also need to:

1. Have a copyright header
2. Appear in Mathlib.lean
3. Import Mathlib.Init

and furthermore they could contain non-trivial Lean code. Bug or feature?

[Michael Rothgang]

4. be valid Lean files (as opposed to just markdown)

[Riccardo Brasca]

Well, it is surely strange that there is a file, Mathlib/Algebra/README.md, that basically nobody knows about and that contains an hard rule.

[Riccardo Brasca]

Honestly I've ignored it until now. This can very well be my fault, but I am pretty sure we never really discussed the rule itself.

[Filippo A. E. Nuccio]

I confess I had never heard/seen the REAMDE.md neither.

[Eric Wieser]

Quoting the readme:

The basic algebraic hierarchy is split across a series of subfolders that each depend on the
previous:

• Algebra.Notation for basic algebraic notation
• Algebra.Group for semigroups, monoids, groups
• Algebra.GroupWithZero for monoids with a zero adjoined, groups with a zero adjoined
• Algebra.Ring for semirings, rings
• Algebra.Field for semifields, fields

Files in earlier subfolders should not import files in later ones.

I think the tension here is whether the taxonomy of files is intended to help users or maintainers. I don't think users expect to find a result about cyclic groups in Algebra.Ring just because it happens to need some results from ring theory.

[Eric Wieser]

But if ultimately we just tell users to import Mathlib then indeed the taxonomy only really matters for maintainers.

[Filippo A. E. Nuccio]

Well, it actually also matters for contributors when they open a PR.

[Robin Carlier]

Maintainers and people wanting to contribute.

[Robin Carlier]

But ultimately, this is "development" documentation rather than "user documentation", so perhaps we could say "read the README.md of the relevant folders" in the contribution guidelines?

[Andrew Yang]

Maybe the answer is “cyclic groups shouldn’t be a part of the ‘basic algebraic hierarchy’ and should go in Mathlib/GroupTheory instead”?

[Filippo A. E. Nuccio]

I confess I also have some difficulties in understanding the difference between the GroupTheory folder and the Algebra.Group one. That being said, if we consider that importing something from ring theory for Algebra.Group is unreasonable, why would it be OK for Mathlib.GroupTheory?

[Yaël Dillies]

Precisely because it isn't basic anymore

[Yaël Dillies]

Andrew's viewpoint is exactly mine too

[Eric Wieser]

Can you expand the readme to explain that such "crossover" topics likely belong in the *Theory directories?

[Yaël Dillies]

Sure, PR incoming

[Filippo A. E. Nuccio]

It seems to me that there is no clear consensus and I feel that there are two main options around, so I'm proposing a poll and will try to advance according to the results.

[Filippo A. E. Nuccio]

/poll What should we do about cyclic groups (with zero) requiring Ring?
Remove assert_not_exists Ring from Mathlib.Group.GroupWithZero.Int
Move all results about cyclic groups (with zero) away from Mathlib.Algebra.Group to Mathlib.GroupTheory

[Yaël Dillies]

Is this poll about anything, really? Do we have examples of cyclic group results that genuinely require Ring?

[Filippo A. E. Nuccio]

I am running into problems with #24435, so " yes".

[Yaël Dillies]

Ah! That would have been good to mention from the start :smile:

[Yaël Dillies]

You have found results that currently import rings. It is not clear to me that they need rings

[Filippo A. E. Nuccio]

Filippo A. E. Nuccio said:

For the context: I am trying to add some cyclicity properties to Mathlib.Algebra.GroupWithZero.Int.lean but it starts with a assert_not_import Ring and then it complains.

[Yaël Dillies]

I didn't see the PR :see_no_evil: