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
[Merged by Bors] - feat(RingTheory/Localization): add facts about localization at minimal prime ideals #11201
Conversation
first half of homogenitiy
It wouldn't take much effort to show that the prime spectrum of these rings is a single point but I'm not sure where this would fit exactly |
This reverts commit 3bdfc10.
I agree that this should be added, probably in |
Done. I think the |
Here is a slight refactor that introduces IsLocalization.AtPrime.orderIsoOfPrime and IsLocalization.AtPrime.prime_unique_of_minimal. Feel free to merge if it looks good. |
Apart from @alreadydone 's comment, the whole PR now LGTM. |
If you add docs to the |
I've now added a docstring, but this is something you could have done :) |
…_minimalPrime Jyxu/localization minimal prime
LGTM |
Thanks 🎉 |
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
Thanks! bors merge |
…l prime ideals (#11201) Show that localization at minimal primes results in rings with only a single prime ideal, implying that every non-unit element is nilpotent. Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: uniwuni <95649083+uniwuni@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…l prime ideals (#11201) Show that localization at minimal primes results in rings with only a single prime ideal, implying that every non-unit element is nilpotent. Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: uniwuni <95649083+uniwuni@users.noreply.github.com>
…l prime ideals (#11201) Show that localization at minimal primes results in rings with only a single prime ideal, implying that every non-unit element is nilpotent. Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: uniwuni <95649083+uniwuni@users.noreply.github.com>
…l prime ideals (#11201) Show that localization at minimal primes results in rings with only a single prime ideal, implying that every non-unit element is nilpotent. Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: uniwuni <95649083+uniwuni@users.noreply.github.com>
…l prime ideals (#11201) Show that localization at minimal primes results in rings with only a single prime ideal, implying that every non-unit element is nilpotent. Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: uniwuni <95649083+uniwuni@users.noreply.github.com>
…l prime ideals (#11201) Show that localization at minimal primes results in rings with only a single prime ideal, implying that every non-unit element is nilpotent. Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: uniwuni <95649083+uniwuni@users.noreply.github.com>
Show that localization at minimal primes results in rings with only a single prime ideal, implying that every non-unit element is nilpotent.
Co-authored-by: Junyan Xu junyanxumath@gmail.com