Maximal Ideals

[tirix]

Definition and theorems about maximal ideals ported from Jeff Madsen's mathbox.
I also added a chapter about the sumset of two sets, which is useful for dealing with operations on ideals.

[savask]

Great work! I'm especially happy to see some theorems on sumsets. I think the theory of sumsets is very worth formalizing in set.mm (after agreeing on definitions, see my comment on LSSum). It would be great to see some results from additive combinatorics formalized, like Ruzsa's triangle inequality.

[tirix]

I'm converting this PR to draft until it is reworked using LSSum, then I will ask for a review again.
In the mean time it's Ok if other PR like e.g. #3789 are merged, I can adapt (this happened before).

[savask]

Nice changes, as always! The definition of a spectrum makes me wonder if you have an eye on algebraic geometry.

I think it's also worth mentioning that some earlier theorems in your pull request, like lsmidllsp, work for Rng-s (non-unital rings). The benefit here is that ideals in an Rng are Rng-s themselves, and that simplifies arguments in some cases.

[tirix]

Nice changes, as always! The definition of a spectrum makes me wonder if you have an eye on algebraic geometry.

Thanks! Yes, I had been looking a some algebraic geometry at the time I originally wrote this PR (in January), and I thought that the spectrum of a ring was a relatively low-hanging fruit to pick.

I think it's also worth mentioning that some earlier theorems in your pull request, like lsmidllsp, work for Rng-s (non-unital rings). The benefit here is that ideals in an Rng are Rng-s themselves, and that simplifies arguments in some cases.

Indeed. Since this PR has been pending for a long time, maybe it's better to just merge as-is, and refine later?