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(topology/sheaves): Locally surjective maps of presheaves #15398

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(topology/sheaves): Locally surjective maps of presheaves #15398

wants to merge 12 commits into from

Conversation

jakelev
Copy link
Collaborator

@jakelev jakelev commented Jul 15, 2022

For presheaves valued in a concrete category, we define locally surjective maps of presheaves and show that this condition is equivalent to all the induced maps of stalks being surjective.

We also introduce notation for the types of sections, germs and corresponding induced maps.

Co-authored by: Sam van Gool @samvang

We are unhappy with one line in each direction of the proof of equivalence:

  • On Line 119, we weren't able to rewrite with h_eq and/or (forget C).map_comp.
  • On Line 151, we weren't able to rewrite with (forget C).map_comp.

Open in Gitpod

erdOne
erdOne reviewed Jul 16, 2022
View reviewed changes
src/topology/sheaves/locally_surjective.lean Show resolved Hide resolved
src/topology/sheaves/locally_surjective.lean Outdated Show resolved Hide resolved
src/topology/sheaves/locally_surjective.lean Outdated Show resolved Hide resolved
src/topology/sheaves/locally_surjective.lean Show resolved Hide resolved
src/topology/sheaves/locally_surjective.lean Outdated Show resolved Hide resolved
@erdOne
Copy link
Member

erdOne commented Jul 16, 2022

Also, If you need help on some things in a PR, you could label the PR as help_wanted.

jakelev and others added 2 commits July 18, 2022 00:00
@jakelev @erdOne
Apply suggestions from code review
095ca41 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@jakelev
cleaner end of proof due to Adam Topaz
2b3730f
erdOne
erdOne approved these changes Jul 18, 2022
View reviewed changes
Copy link
Member

@erdOne erdOne left a comment

Choose a reason for hiding this comment

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

Some minor comments about styles, but LGTM otherwise.

src/topology/sheaves/locally_surjective.lean Outdated Show resolved Hide resolved
src/topology/sheaves/locally_surjective.lean Outdated Show resolved Hide resolved
src/topology/sheaves/locally_surjective.lean Outdated Show resolved Hide resolved
src/topology/sheaves/locally_surjective.lean Outdated Show resolved Hide resolved
src/topology/sheaves/locally_surjective.lean Outdated Show resolved Hide resolved
@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 18, 2022
jakelev and others added 2 commits July 18, 2022 14:27
@jakelev @erdOne
Apply suggestions from code review
beb8b3f 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@jakelev
added backticks around math notation in docstrings
0947215
@erdOne
Copy link
Member

erdOne commented Nov 2, 2022

Hi, are there still plans on getting this merged?

@erdOne erdOne 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 7, 2022
@semorrison
Copy link
Collaborator

Unless @erdOne says others, LGTM.

bors d+

@semorrison semorrison closed this Nov 9, 2022
@bors
Copy link

bors bot commented Nov 9, 2022

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

@semorrison semorrison reopened this Nov 9, 2022
@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 9, 2022
@semorrison
Copy link
Collaborator

(Sorry, hit the wrong button, didn't mean to close!!)

@erdOne
Copy link
Member

erdOne commented Nov 11, 2022

@semorrison It seems like the author is not working on this anymore; this has been "awaiting-author" for four months.
I think we should merge it right away?

@samvang
Copy link
Collaborator

samvang commented Nov 11, 2022

Hi, @jakelev and I did this work together during LFTCM’22, I for one would definitely be happy to see it merged. I imagine the same goes for Jake.
(I have a busy semester and not a lot of time to devote to Lean atm, so may have missed some Zulip messages on the topic, sorry!)
Thanks,
Sam

@semorrison
Copy link
Collaborator

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Nov 13, 2022
bors bot pushed a commit that referenced this pull request Nov 13, 2022
@jakelev @erdOne
feat(topology/sheaves): Locally surjective maps of presheaves (#15398)
fb7698e 
For presheaves valued in a concrete category, we define locally surjective maps of presheaves and show that this condition is equivalent to all the induced maps of stalks being surjective.

We also introduce notation for the types of sections, germs and corresponding induced maps.

Co-authored by: Sam van Gool @samvang 



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

bors bot commented Nov 13, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(topology/sheaves): Locally surjective maps of presheaves [Merged by Bors] - feat(topology/sheaves): Locally surjective maps of presheaves Nov 13, 2022
@bors bors bot closed this Nov 13, 2022
@bors bors bot deleted the locally_surjective_maps_of_presheaves branch November 13, 2022 16:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

@erdOne erdOne erdOne approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. 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.

None yet
4 participants
@jakelev @erdOne @semorrison @samvang