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(category_theory/sites/*): Redefine the category of sheaves. #10678

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - refactor(category_theory/sites/*): Redefine the category of sheaves. #10678

wants to merge 19 commits into from

Conversation

adamtopaz
Copy link
Collaborator

This refactor redefines sheaves and morphisms of sheaves using bespoke structures.
This is an attempt to make automation more useful when dealing with categories of sheaves.

See the associated zulip discussion

Open in Gitpod

@adamtopaz adamtopaz added the RFC Request for comment label Dec 8, 2021
@adamtopaz adamtopaz mentioned this pull request Dec 8, 2021
Closed
semorrison
semorrison approved these changes Dec 11, 2021
View reviewed changes
Copy link
Collaborator

@semorrison semorrison left a comment

Choose a reason for hiding this comment

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

Looks great!

@adamtopaz adamtopaz added awaiting-review The author would like community review of the PR and removed RFC Request for comment labels Dec 11, 2021
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

bors bot pushed a commit that referenced this pull request Dec 16, 2021
@adamtopaz
refactor(category_theory/sites/*): Redefine the category of sheaves. (#…
9f9015c 
…10678)

This refactor redefines sheaves and morphisms of sheaves using bespoke structures.
This is an attempt to make automation more useful when dealing with categories of sheaves.

See the associated [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Redefining.20Sheaves/near/263308542)
@github-actions github-actions bot 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 Dec 16, 2021
@bors
Copy link

bors bot commented Dec 16, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(category_theory/sites/*): Redefine the category of sheaves. [Merged by Bors] - refactor(category_theory/sites/*): Redefine the category of sheaves. Dec 16, 2021
@bors bors bot closed this Dec 16, 2021
@bors bors bot deleted the sheaf_redef branch December 16, 2021 22:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison approved these changes

@erdOne erdOne Awaiting requested review from erdOne

Assignees
No one assigned
Labels
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
3 participants
@adamtopaz @jcommelin @semorrison