Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 22 commits into
base: master
Choose a base branch
from

Conversation

maddycrim
Copy link
Collaborator

@maddycrim maddycrim commented Oct 8, 2024

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


Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Oct 8, 2024
Copy link

github-actions bot commented Oct 8, 2024

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.

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Oct 8, 2024
Copy link
Collaborator

@mbkybky mbkybky left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the contribution!
Some suggestions:

Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean Outdated Show resolved Hide resolved
@mbkybky mbkybky added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 9, 2024
@maddycrim maddycrim requested a review from mbkybky October 9, 2024 18:05
Copy link
Collaborator

@mbkybky mbkybky left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 maddycrim requested review from mbkybky and removed request for mbkybky October 10, 2024 02:56
@maddycrim maddycrim closed this Oct 10, 2024
@maddycrim maddycrim reopened this Oct 10, 2024
@maddycrim
Copy link
Collaborator Author

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
Copy link
Collaborator

mbkybky commented Oct 10, 2024

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 maddycrim added the help-wanted The author needs attention to resolve issues label Oct 10, 2024
@maddycrim
Copy link
Collaborator Author

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

@maddycrim maddycrim removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 10, 2024
@mbkybky
Copy link
Collaborator

mbkybky commented Oct 11, 2024

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

@maddycrim maddycrim removed the help-wanted The author needs attention to resolve issues label Oct 16, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 18, 2024
@AlexKontorovich AlexKontorovich removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 22, 2024
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean Outdated Show resolved Hide resolved
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 30, 2024
@maddycrim maddycrim removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 30, 2024
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

maintainer merge

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

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 `R`-algebra isomorphism between
`R` and `S`. -/
noncomputable def nilradmaxlocalizationIsSelf [h : (nilradical R).IsMaximal] (h' : (0 : R) ∉ M)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not super sure about this name

Copy link

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

variable {R : Type*} [CommSemiring R] {S : Type*} [CommSemiring S] [Algebra R S] {M : Submonoid R}

-- TODO: Make this an `instance`
theorem LocalRing.of_nilradical_isMaximal [h : (nilradical R).IsMaximal] :
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But it is always the Jacobson radical.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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 `R`-algebra isomorphism between
`R` and `S`. -/
noncomputable def nilradmaxlocalizationIsSelf [h : (nilradical R).IsMaximal] (h' : (0 : R) ∉ M)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm would something like localization_equiv_self_of_nilradical_isMaximal be better?...

@riccardobrasca
Copy link
Member

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

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Oct 31, 2024

✌️ 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 YaelDillies changed the title feat (LocalRing/MaximalIdeal/Basic): add LocalRing.not_mem_maximalIdeal and nilradmax_localization_IsSelf feat(LocalRing/MaximalIdeal/Basic): localization of a Krull dim zero ring Oct 31, 2024
@YaelDillies
Copy link
Collaborator

(I changed the title to something more memorable)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated maintainer-merge new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants