feat(LocalRing/MaximalIdeal/Basic): localization of a Krull dim zero ring

[maddycrim]

For theorem LocalRing.not_mem_maximalIdeal: An element x of a commutative local semiring is not contained in the maximal ideal if and only if it is a unit.

For noncomputable def nilradmax_localization_IsSelf: Let S be the localization of a commutative semiring R at a submonoid M that does not contain 0. If the nilradical of R is maximal then there is a ring isomorphism between R and S.

As discussed on Zulip here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/PR.20Permission/near/472582165

---

[github-actions]

PR summary c6c8da1b16

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ LocalRing.of_nilradical_isMaximal
+ nilradmaxlocalizationIsSelf
+ not_mem_maximalIdeal

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mbkybky]

Thanks for the contribution!
Some suggestions:

[mbkybky]

Do you think the conclusion that R is LocalRing if nilradical of R is maximal will be used afterwards? If you think it will be useful ‌in future, you can extract it and write it as a separate instance.

[maddycrim]

Do you think the conclusion that R is LocalRing if nilradical of R is maximal will be used afterwards? If you think it will be useful ‌in future, you can extract it and write it as a separate instance.

I don't plan on using it for what I'm currently doing. However, I imagine it could be helpful to others. I will submit another pull request with this instance.

[mbkybky]

Do you think the conclusion that R is LocalRing if nilradical of R is maximal will be used afterwards? If you think it will be useful ‌in future, you can extract it and write it as a separate instance.

I don't plan on using it for what I'm currently doing. However, I imagine it could be helpful to others. I will submit another pull request with this instance.

I think you can just add the instance in this PR and then use it to prove your main theorem. If you prefer to open a new PR, you need to make this PR depend on your new PR.

[maddycrim]

I'm getting a strange linter error in an unrelated file. Can someone please help me figure this out?

[mbkybky]

I also have no idea how to solve this problem. You could post this problem on Zulip for help.

[YaelDillies]

Thanks for the PR! I think we are pretty close to merging.

[YaelDillies]

Thanks!

maintainer merge

Algebraists, please check if you agree with the new def's name

[YaelDillies]

I'm not super sure about this name

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[erdOne]

We should add one for Jacobson radical, and this should be an iff.

[maddycrim]

I don't think a Local ring always has that the nilradical is the unique maximal ideal. I believe we need krull dimension 0 as well.

[erdOne]

But it is always the Jacobson radical.

[maddycrim]

Oh I see what you mean now. Yes, I agree.

[erdOne]

I think the more common spelling of "nilradical is maximal" for commutative rings is "artinian local ring".

[maddycrim]

I see that artinian local ring has the nilradical is maximal. However, I don't see the reverse implication. What about R=F[x2,x3,...]/(x_2^2,x_3^3,..)? I am assuming here that F is a field and that we have countably many x_i. I believe we have a local ring with the nilradical is maximal but the ring is not Artinian.

[erdOne]

Okay sorry it's Krull dim = 0 instead.
But we don't have such a class in mathlib :(

[AlexKontorovich]

Hmm would something like localization_equiv_self_of_nilradical_isMaximal be better?...

[riccardobrasca]

It seems there is still a comment about a name, but otherwise LGTM, thanks!

bors d+

[mathlib-bors]

✌️ maddycrim can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

(I changed the title to something more memorable)