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

feat(ring_theory/graded_algebra/homogeneous_ideal): homogenous ideals of a graded algebras #9717

Closed
wants to merge 326 commits into from
Closed

feat(ring_theory/graded_algebra/homogeneous_ideal): homogenous ideals of a graded algebras #9717

wants to merge 326 commits into from

Conversation

jjaassoonn
Copy link
Collaborator

@jjaassoonn jjaassoonn commented Oct 14, 2021 •
edited by github-actions bot
Loading

Define homogenous ideal of a graded algebras and some lemmas

Most noticeably:

  • Inf, Sup, product
  • radical
    of homogeneous ideals and when is a homogeneous ideal prime.

Once this pr stablises, this can be used in pr #9964 and #9919 (Construction of proj of graded algebra)

This pr is splitted into this one and #10784

Open in Gitpod

@jjaassoonn jjaassoonn changed the title first commit feat(homogenous-ideal-of-graded-ring) Oct 14, 2021
@jjaassoonn jjaassoonn added WIP Work in progress help-wanted The author needs attention to resolve issues labels Oct 14, 2021
eric-wieser
eric-wieser reviewed Oct 14, 2021
View reviewed changes
src/ring_theory/homogeneous_ideal.lean Outdated Show resolved Hide resolved
src/ring_theory/homogeneous_ideal.lean Outdated Show resolved Hide resolved
src/ring_theory/homogeneous_ideal.lean Outdated Show resolved Hide resolved
src/ring_theory/homogeneous_ideal.lean Outdated Show resolved Hide resolved
src/ring_theory/homogeneous_ideal.lean Outdated Show resolved Hide resolved
src/ring_theory/homogeneous_ideal.lean Outdated Show resolved Hide resolved
src/ring_theory/homogeneous_ideal.lean Outdated Show resolved Hide resolved
src/ring_theory/homogeneous_ideal.lean Outdated Show resolved Hide resolved
@eric-wieser eric-wieser changed the title feat(homogenous-ideal-of-graded-ring) feat(ring_theory/homogeneous_ideal): homogenous ideals of a graded rings Oct 14, 2021
@jjaassoonn
Copy link
Collaborator Author

Also, the linter says one instance is unused but if I comment it out, everything breaks.

@eric-wieser
Copy link
Member

It's telling you that it's unused by one particular lemma, not by everything in the file. You should remove it from variables and add it to the lemmas that need it.

@jjaassoonn
Copy link
Collaborator Author

It's telling you that it's unused by one particular lemma, not by everything in the file. You should remove it from variables and add it to the lemmas that need it.

Thank you.

@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 18, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 18, 2021
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 23, 2022
@leanprover-community leanprover-community deleted a comment from github-actions bot Feb 23, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 23, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 24, 2022
@eric-wieser
Copy link
Member

Would you mind discarding this PR and starting a new PR with the same changes? We're >300 commits and 66 comments in, and this is only just ready for review!

@jjaassoonn
Copy link
Collaborator Author

Would you mind discarding this PR and starting a new PR with the same changes? We're >300 commits and 66 comments in, and this is only just ready for review!

Sure, I was thinking that.

@jjaassoonn jjaassoonn closed this Feb 24, 2022
@jjaassoonn jjaassoonn mentioned this pull request Feb 24, 2022
Closed
@jjaassoonn jjaassoonn deleted the feat(homogenous-ideal-of-graded-ring) branch March 9, 2022 16:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@alexjbest alexjbest alexjbest left review comments

Assignees
No one assigned
Labels
awaiting-review The author would like community review of the PR RFC Request for comment
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@jjaassoonn @eric-wieser @leanprover-community-bot-assistant @alexjbest