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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat : generalize PrimeSpectrum from Ring to Semiring #8763

Closed
wants to merge 26 commits into from
Closed

[Merged by Bors] - feat : generalize PrimeSpectrum from Ring to Semiring #8763

wants to merge 26 commits into from

Conversation

XavierXarles
Copy link
Collaborator

Some results of PrimeSpectrum generalized from CommRing to CommSemiring.

@XavierXarles XavierXarles added the help-wanted The author needs attention to resolve issues label Dec 1, 2023
@XavierXarles
Update Properties.lean
26a9d9d 
Changed proof to avoid a deterministic timeout
@XavierXarles @github-actions
Update Mathlib/AlgebraicGeometry/Properties.lean
3122986 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@XavierXarles XavierXarles added awaiting-review The author would like community review of the PR t-algebraic-geometry Algebraic geometry labels Dec 2, 2023
@jcommelin
Copy link
Member

Out of curiosity: Would you mind commenting a bit on the motivation for this PR?

@XavierXarles
Copy link
Collaborator Author

Out of curiosity: Would you mind commenting a bit on the motivation for this PR?

There are some papers about how the whole construction of Schemes work for general commutative semirings. In that papers, most of the details are omitted. I am trying to see if the proofs are more or less the same. As the changes in this case are minimum (just some results true for CommRing are not true for CommSemiring), I thought it would be nice to have it in mathlib4. The change in the AlgebraicGeometry.Properties is due to what it seems some inference (?) did not work.

@jcommelin
Copy link
Member

@XavierXarles Nice, that seems like an interesting project!

Can you please update the PR title according to the guidelines?

And I think it would be nice if you can debug a bit further why some proofs become longer. Is there a mathematical reason, or is it because some API for semirings is under developed?

@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 4, 2023
@XavierXarles XavierXarles changed the title Generalize PrimeSpectrum from Ring to Semiring feat: generalize PrimeSpectrum from Ring to Semiring Dec 5, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 5, 2023
@XavierXarles
Copy link
Collaborator Author

And I think it would be nice if you can debug a bit further why some proofs become longer. Is there a mathematical reason, or is it because some API for semirings is under developed?

I am not sure to what proofs you refer as being longer. Do you mean the proof in AlgebraicGeometry.Properties of the instance?

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 5, 2023
XavierXarles and others added 2 commits December 15, 2023 20:40
@XavierXarles
Update Basic.lean
ad076c5
@XavierXarles @github-actions
Apply suggestions from code review
56b655a 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@XavierXarles XavierXarles requested review from eric-wieser and removed request for jcommelin and MichaelStollBayreuth December 15, 2023 21:37
@XavierXarles XavierXarles changed the title feat: generalize PrimeSpectrum from Ring to Semiring feat (RingTheory/Localization/LocalizationLocalization): generalize PrimeSpectrum from Ring to Semiring Dec 16, 2023
@XavierXarles XavierXarles changed the title feat (RingTheory/Localization/LocalizationLocalization): generalize PrimeSpectrum from Ring to Semiring feat : generalize PrimeSpectrum from Ring to Semiring Dec 16, 2023
@XavierXarles XavierXarles added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 28, 2023
@XavierXarles XavierXarles requested review from eric-wieser and removed request for eric-wieser December 28, 2023 00:16
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jan 1, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jan 7, 2024
@XavierXarles @github-actions
Spaces
ded64f5 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
alreadydone
alreadydone reviewed Jan 7, 2024
View reviewed changes
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean Outdated Show resolved Hide resolved
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean Outdated Show resolved Hide resolved
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean Outdated Show resolved Hide resolved
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean Outdated Show resolved Hide resolved
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean Outdated Show resolved Hide resolved
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean Outdated Show resolved Hide resolved
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
(x : PrimeSpectrum S) (hx : IsClosed ({x} : Set (PrimeSpectrum S))) :
IsClosed ({comap f x} : Set (PrimeSpectrum R)) :=
haveI : x.asIdeal.IsMaximal := (isClosed_singleton_iff_isMaximal x).1 hx
(isClosed_singleton_iff_isMaximal _).2 (Ideal.comap_isMaximal_of_surjective f hf)
Copy link
Contributor

Choose a reason for hiding this comment

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

Once you generalize Ideal.comap_isMaximal_of_surjective you can probably generalize all results in this section that assumes surjectivity (not sure about IsIntegral). For surjectivity it should still be true for Semirings that there is an OrderIso between ideals in R containing the kernel and all ideals in S.

@XavierXarles @alreadydone
Apply suggestions from code review
c65ec9d 
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
jcommelin
jcommelin approved these changes Jan 8, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jan 8, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 8, 2024
@XavierXarles
feat : generalize PrimeSpectrum from Ring to Semiring (#8763)
3b80012 
Some results of PrimeSpectrum generalized from CommRing to CommSemiring. 



Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Jan 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat : generalize PrimeSpectrum from Ring to Semiring [Merged by Bors] - feat : generalize PrimeSpectrum from Ring to Semiring Jan 8, 2024
@mathlib-bors mathlib-bors bot closed this Jan 8, 2024
@mathlib-bors mathlib-bors bot deleted the PrimeSpectrum branch January 8, 2024 14:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alreadydone alreadydone alreadydone left review comments

@github-actions github-actions[bot] github-actions left review comments

@jcommelin jcommelin jcommelin approved these changes

@erdOne erdOne Awaiting requested review from erdOne

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-algebraic-geometry Algebraic geometry
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@XavierXarles @jcommelin @eric-wieser @alreadydone @leanprover-community-mathlib4-bot