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] - refactor(topology/sheaf_condition): remove has_products for restriction to open subspace #17361

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - refactor(topology/sheaf_condition): remove has_products for restriction to open subspace #17361

wants to merge 11 commits into from

Conversation

alreadydone
Copy link
Collaborator

@alreadydone alreadydone commented Nov 5, 2022 •
edited by erdOne
Loading

@alreadydone alreadydone 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. t-algebraic-geometry Algebraic geometry labels Nov 5, 2022
@alreadydone alreadydone requested a review from a team as a code owner November 5, 2022 02:53
@alreadydone alreadydone 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 Nov 5, 2022
@alreadydone alreadydone changed the title chore(algebraic_geometry/sheafed_space): partially remove has_products refactor(topology/sheaf_condition): remove has_products for restriction to open subspace Nov 5, 2022
@alreadydone alreadydone 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 Nov 5, 2022
@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 Nov 5, 2022
@jcommelin
Copy link
Member

bors d=erdOne

@bors
Copy link

bors bot commented Nov 5, 2022

✌️ erdOne 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 delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Nov 5, 2022
@alreadydone alreadydone requested a review from a team as a code owner November 6, 2022 04:29
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added 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 Nov 6, 2022
@alreadydone alreadydone mentioned this pull request Nov 6, 2022
Closed
1 task
@alreadydone
Copy link
Collaborator Author

@erdOne CI has passed. Could you please merge this? Thanks!

@erdOne
Copy link
Member

erdOne commented Nov 8, 2022

bors merge

@bors
Copy link

bors bot commented Nov 8, 2022

👎 Rejected by label

@erdOne erdOne 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 Nov 8, 2022
@erdOne
Copy link
Member

erdOne commented Nov 8, 2022

bors merge

@erdOne erdOne mentioned this pull request Nov 8, 2022
Closed
bors bot pushed a commit that referenced this pull request Nov 8, 2022
@alreadydone @erdOne
refactor(topology/sheaf_condition): remove has_products for restricti…
f384f5d 
…on to open subspace (#17361)

Co-authored-by: erd1 <the.erd.one@gmail.com>
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@bors
Copy link

bors bot commented Nov 8, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(topology/sheaf_condition): remove has_products for restriction to open subspace [Merged by Bors] - refactor(topology/sheaf_condition): remove has_products for restriction to open subspace Nov 8, 2022
@bors bors bot closed this Nov 8, 2022
@bors bors bot deleted the SheafedSpace_without_products branch November 8, 2022 03:51
bors bot pushed a commit that referenced this pull request Nov 9, 2022
@alreadydone @erdOne
refactor(topology/sheaf_condition): remove redundant constructions (#…
85d6221 
…17378)

The constructions used to prove `is_sheaf_iff_is_sheaf_equalizer_products` in *sites.lean* is redundant because the equivalence can now be achieved via `is_sheaf` (site version) ↔ opens_le_cover ↔ pairwise_intersections ↔ equalizer_products. Refactoring the proof of this equivalence after removal of these constructions, however, requires rearranging the import chain and moving things around, explaining the large diff.

The author @justus-springer of the constructions has previously [approved the removal](#11706 (comment)) in #11706.

The universe levels in *equalizer_products.lean* are also fixed and generalized (a cover of a space should be indexed by a type in the same universe), leading to the addition of a few universe ascriptions.

- [x] depends on: #17361 



Co-authored-by: erd1 <the.erd.one@gmail.com>
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@erdOne erdOne erdOne left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. t-algebraic-geometry Algebraic geometry
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@alreadydone @jcommelin @erdOne @mathlib-dependent-issues-bot