Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebra/homology/local_cohomology): just the definition #19061

Closed
wants to merge 30 commits into from
Closed

[Merged by Bors] - feat(algebra/homology/local_cohomology): just the definition #19061

wants to merge 30 commits into from

Conversation

emwitt
Copy link
Collaborator

@emwitt emwitt commented May 22, 2023

Open in Gitpod

@emwitt emwitt added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels May 22, 2023
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label May 22, 2023
kbuzzard
kbuzzard reviewed May 22, 2023
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.

This looks great! I've left some comments.

@kim-em kim-em added WIP Work in progress and removed awaiting-review The author would like community review of the PR labels May 23, 2023
@github-actions github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label May 23, 2023
jakelev and others added 14 commits May 23, 2023 11:29
@jakelev
fixed conventions about op and added the universal diagram for local …
7d2e9af 
…cohomology
@jakelev
fixed conventions about op and added the universal diagram for local …
8f022b0 
…cohomology
@jakelev
merge changes and destroy universes
7c1ed56
@jakelev
added authors to docstring
bc2a66d
@kim-em
universe polymorphism
debb577
@kim-em
Merge branch 'local_cohomology' of github.com:leanprover-community/ma…
a45dc29 
…thlib into local_cohomology
@kim-em
better handling of universes
71eae19
@jakelev
define local_cohomology_univ without auxiliary local_cohomology_univ_…
9f86af4 
…diagram step
@kim-em
some cleanup
5eda1e8
@jakelev
define local_cohomology_univ without auxiliary local_cohomology_univ_…
4d64fb3 
…diagram step
@jakelev
define local_cohomology_univ without auxiliary local_cohomology_univ_…
36b71d4 
…diagram step
@jakelev
add docstring and porting note to exists_pow_le_of_radical_le_of_fg
ff25d6a
@jakelev
coercion of powers of ideal into ideals with same radical
6c614e6
@jakelev
cleanup docstrings, remove incomplete bits
8ddb42f
@jakelev jakelev removed the WIP Work in progress label May 23, 2023
@kbuzzard kbuzzard added the awaiting-author A reviewer has asked the author a question or requested changes label May 24, 2023
@jakelev jakelev 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 May 24, 2023
@kbuzzard
Copy link
Member

This looks fine to me now -- I'm happy to maintainer-merge if nobody else has anything to say.

Note the forward-port requirement: in a couple of days you'll have to make a short PR to mathlib4. This is only happening because we're in this transition period.

@riccardobrasca
Copy link
Member

There is a new file that's empty...

jcommelin
jcommelin approved these changes May 24, 2023
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-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 24, 2023
@riccardobrasca
Copy link
Member

I see in the diff an empty file algebra.homology.koszul_homology. If this is not my fault and the file is really there, @emwitt can you please remove it before merging the PR?

bors r-

@bors
Copy link

bors bot commented May 24, 2023

Canceled.

@riccardobrasca
Copy link
Member

bors d+

@bors
Copy link

bors bot commented May 24, 2023

✌️ emwitt can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added the delegated The PR author may merge after reviewing final suggestions. label May 24, 2023
@jakelev
Copy link
Collaborator

jakelev commented May 24, 2023

I see in the diff an empty file algebra.homology.koszul_homology. If this is not my fault and the file is really there, @emwitt can you please remove it before merging the PR?

bors r-

That's my fault, I merged it by mistake in the last commit. Fixed now.

@emwitt
Copy link
Collaborator Author

emwitt commented May 25, 2023

bors merge

bors bot pushed a commit that referenced this pull request May 25, 2023
@emwitt @jakelev @kim-em
feat(algebra/homology/local_cohomology): just the definition (#19061)
5a684ce 


Co-authored-by: Emily Witt <emwitt@gmail.com>
Co-authored-by: Jake Levinson <levinson.jake@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented May 25, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat(algebra/homology/local_cohomology): just the definition [Merged by Bors] - feat(algebra/homology/local_cohomology): just the definition May 25, 2023
@bors bors bot closed this May 25, 2023
@bors bors bot deleted the local_cohomology branch May 25, 2023 21:34
@kim-em kim-em mentioned this pull request Jun 6, 2023
Merged
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

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

@adamtopaz adamtopaz adamtopaz left review comments

@jakelev jakelev jakelev left review comments

@kbuzzard kbuzzard kbuzzard left review comments

@riccardobrasca riccardobrasca riccardobrasca left review comments

@joelriou joelriou joelriou left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
10 participants
@emwitt @kbuzzard @riccardobrasca @jakelev @eric-wieser @adamtopaz @jcommelin @joelriou @kim-em @leanprover-community-bot-assistant