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(RingTheory/GradedAlgebra/Noetherian): properties of a graded Noetherian ring #8187

Closed
wants to merge 49 commits into from
Closed

[Merged by Bors] - feat(RingTheory/GradedAlgebra/Noetherian): properties of a graded Noetherian ring #8187

wants to merge 49 commits into from

Conversation

FMLJohn
Copy link
Collaborator

@FMLJohn FMLJohn commented Nov 4, 2023

Open in Gitpod

@FMLJohn FMLJohn added awaiting-review t-algebraic-geometry Algebraic geometry t-algebra Algebra (groups, rings, fields, etc) labels Nov 4, 2023
@FMLJohn
Copy link
Collaborator Author

FMLJohn commented Nov 4, 2023

I have proved that for a Noetherian graded ring, its 0th grade is also a Noetherian ring.

@FMLJohn
Copy link
Collaborator Author

FMLJohn commented Nov 4, 2023

@kbuzzard @eric-wieser

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 6, 2023
eric-wieser
eric-wieser reviewed Nov 6, 2023
View reviewed changes
@FMLJohn FMLJohn closed this Nov 6, 2023
@FMLJohn FMLJohn deleted the HilbertSeries branch November 6, 2023 15:43
@eric-wieser eric-wieser restored the HilbertSeries branch November 6, 2023 16:18
@FMLJohn FMLJohn reopened this Nov 6, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 6, 2023
@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI and removed awaiting-review labels Nov 20, 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. (this label is managed by a bot) label Mar 1, 2024
@FMLJohn FMLJohn requested a review from kbuzzard May 16, 2024 11:46
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 16, 2024
@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 May 16, 2024
kbuzzard
kbuzzard reviewed May 19, 2024
View reviewed changes
Copy link
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

Modulo the grammar issue I just flagged, this looks good to me. @eric-wieser you wrote "I'm also happy with merging them as is, and revisiting it if/when we notice issues." last November -- do you still feel the same way?

@erdOne erdOne requested a review from eric-wieser May 31, 2024 09:15
@joneugster
Copy link
Collaborator

bench!

@joneugster
Copy link
Collaborator

This PR has approving reviews by both @eric-wieser and @kbuzzard, and superficially it seems to me that there's nothing speaking against a merge.

maintainer merge

@github-actions GitHub Actions
Copy link

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

@mattrobball
Copy link
Collaborator

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 1579883.
There were no significant changes against commit 730684c.

@mattrobball
Copy link
Collaborator

Let's merge master on this before sending it off at least.

@github-actions GitHub Actions
Copy link

PR summary 0d00dd9305

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.Algebra.GradedMonoid 402 407 +5 (+1.24%)

Declarations diff

+ GradeZero.isNoetherianRing
+ GradedRing.coe_projZeroRingHom'_apply
+ GradedRing.projZeroRingHom'
+ GradedRing.projZeroRingHom'_apply_coe
+ GradedRing.projZeroRingHom'_surjective
+ coe_algebraMap
+ coe_intCast
+ coe_mul
+ coe_natCast
+ coe_ofNat
+ coe_one
+ coe_pow
+ instAlgebra
+ instCommMonoid
+ instCommRing
+ instCommSemiring
+ instMonoid
+ instRing
+ instSemiring
+ subalgebra
+ submonoid
+ subring
+ subsemiring

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

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

@mattrobball
Copy link
Collaborator

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 0d00dd9.
There were significant changes against commit 9c4c6f7:

  Benchmark   Metric    Change
  ============================
- build       linting     5.1%

@mattrobball
Copy link
Collaborator

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 27, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 27, 2024
@FMLJohn @eric-wieser
@jjaassoonn @kbuzzard @mattrobball
feat(RingTheory/GradedAlgebra/Noetherian): properties of a graded Noe…
4daf382 
…therian ring (#8187)

Co-authored-by: Li <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Jujian Zhang <[email protected]>
Co-authored-by: Kevin Buzzard <[email protected]>
Co-authored-by: FMLJohn <[email protected]>
Co-authored-by: Matthew Ballard <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 27, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/GradedAlgebra/Noetherian): properties of a graded Noetherian ring [Merged by Bors] - feat(RingTheory/GradedAlgebra/Noetherian): properties of a graded Noetherian ring Jun 27, 2024
@mathlib-bors mathlib-bors bot closed this Jun 27, 2024
@mathlib-bors mathlib-bors bot deleted the HilbertSeries branch June 27, 2024 11:26
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@FMLJohn @eric-wieser
@jjaassoonn @kbuzzard @mattrobball @dagurtomas
feat(RingTheory/GradedAlgebra/Noetherian): properties of a graded Noe…
429f154 
…therian ring (#8187)

Co-authored-by: Li <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Jujian Zhang <[email protected]>
Co-authored-by: Kevin Buzzard <[email protected]>
Co-authored-by: FMLJohn <[email protected]>
Co-authored-by: Matthew Ballard <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Vierkantor Vierkantor Vierkantor left review comments

@kbuzzard kbuzzard kbuzzard left review comments

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

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

Assignees

@eric-wieser eric-wieser

Labels
maintainer-merge new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
9 participants
@FMLJohn @joneugster @mattrobball @leanprover-bot @eric-wieser @Vierkantor @kbuzzard @leanprover-community-mathlib4-bot @jjaassoonn