Prime ideals for semigroups/monoids

Stream: Is there code for X?

[Xavier Xarles]

I think it would be a good idea to define ideals for semigroups/monoids, and then define also such prime ideals. Of course, an ideal for a Monoid M is just SubMulAction M M, but there are some results that are just for ideals, and not general SubMulAction M N. My question is about the name, since I have not find another name in the literature, and I guess we don't want to be called just Ideals. How about MonoidIdeals or any other similar option?

[Kevin Buzzard]

LeftIdeal :-)

[Kevin Buzzard]

Actually I guess ideal shouldn't be mentioned at all because in my head at least it implies closed under addition

[Antoine Chambert-Loir]

Nevertheless, it seems to be customary, in the theory of monoids, to speak of ideals.

That poses again the question of having a reverse documentation of mathlib: given a mathematical topic, how is it addressed in mathlib, or how should it be? (Example: limits are addressed from filters, vector spaces from modules, etc.)
If you already know a bit of the relevant part of mathlib, you can guess what file to open and study its documentation, otherwise, nope…

[Eric Wieser]

How about Monoid.Ideal?

[Kevin Buzzard]

But am I right in thinking that it's only closed under multiplication on one side? Is Monoid.LeftIdeal more appropriate?

[Patrick Massot]

Antoine Chambert-Loir said:

That poses again the question of having a reverse documentation of mathlib: given a mathematical topic, how is it addressed in mathlib, or how should it be?

The Mathlib overview and #mil are meant to do that. But of course they are very incomplete. Contributing to the overview is very easy, you only have to edit a file. Each item is only a link to a declaration but then the module docstring is meant to give a lot more information. Contributing to these docstrings is also a very valuable kind of contribution.

[Xavier Xarles]

In fact, Idealis technically also a left ideal, as it is defined as Submodule R R. So my proposal is to follow the same type of construction.