preferred spelling of zero ideal

Stream: mathlib4

[Violeta Hernández]

In #18568, I experimented with adding a typeclass for 0 being a bottom element. This is meant to generalize lemmas like zero_le, pos_iff_ne_zero, etc. which currently take in assumptions that are too strong for e.g. Ordinal or Nimber, and which cause some duplication with other types like Nat or Multiset that need them before the relevant instance is built.

[Violeta Hernández]

I also made a simp lemma bot_eq_zero. The idea being, bot only has a handful of order properties which can all be taken care of by the instance, while 0 has lots of important algebraic properties depending on where it's found. So the latter form always conveys more information.

[Violeta Hernández]

So I was a bit surprised to learn that via docs#Submodule.zero_eq_bot, the simp-normal form for 0 on submodules and ideals is bot

[Ruben Van de Velde]

Sounds good, but less sure about the simp lemma

[Violeta Hernández]

This seems to be the only instance of breakage, though it is quite a major one

[Violeta Hernández]

So I'm wondering if it would make sense to instead spell the zero and one ideals as 0 and 1

[Eric Wieser]

My take on this is that neither should be declared the simp-normal form; if you want to do lattice theory then you probably want bot, but if you want to work with submodules as a semiring you probably want 0.

[Andrew Yang]

neither should be declared the simp-normal form

This sounds nice in theory but in practice we often need both structures and it is a pain to switch from one to another everytime.
And I'd say the lattice form is more useful because it can prove inequalities while zero can a priori only prove equalities. The only thing about bot being zero that we will need is docs#Ideal.bot_mul. And the preferred spelling of I + J is actually I ⊔ J because of basically the same reasons.
And for the unit ideal, most of the ideal API comes from Submodules where 1 and ⊤ are different things and usually we want the latter so 1 probably won't work.

But if your new typeclass can take care of the bot part seamlessly, then I don't object the change.

[Violeta Hernández]

Thinking about it, maybe it's simply cleaner to not have bot_eq_zero as a simp lemma, but instead implement it individually on the types where it makes sense

[Violeta Hernández]

Which is to say, basically everything besides ideals.

[Violeta Hernández]

Switching the notation for ideals over is something that can be done later if there's a need for it