-
Notifications
You must be signed in to change notification settings - Fork 316
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): add LocalRing.not_mem_maximalIdeal and nilradmax_localization_IsSelf #17549
base: master
Are you sure you want to change the base?
Conversation
PR summary 3bf55718c2Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
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 |
There was a problem hiding this 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:
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`. | ||
-/ | ||
noncomputable def nilradmax_localization_IsSelf (h : (nilradical R).IsMaximal) (h' : (0 : R) ∉ M) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The naming convention requires def
s to be in lowerCamelCase
, i.e., nilradMaxLocalizationIsSelf
in this case.
An element `x` of a commutative local semiring is not contained in the maximal ideal | ||
iff it is a unit. | ||
-/ | ||
theorem LocalRing.not_mem_maximalIdeal [LocalRing R] (x : R) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think maybe this theorem should be moved to immediately follow the theorem mem_maximalIdeal
.
Co-authored-by: Yongle Hu <[email protected]>
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 semiringR
at a submonoidM
that does not contain 0. If the nilradical ofR
is maximal then there is a ring isomorphism betweenR
andS
.As discussed on Zulip here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/PR.20Permission/near/472582165