Skip to content

[Merged by Bors] - feat: port CategoryTheory.Sites.Sheaf#3244

Closed
joelriou wants to merge 9 commits intomasterfrom
port/CategoryTheory.Sites.Sheaf
Closed

[Merged by Bors] - feat: port CategoryTheory.Sites.Sheaf#3244
joelriou wants to merge 9 commits intomasterfrom
port/CategoryTheory.Sites.Sheaf

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Apr 3, 2023

Open in Gitpod

joelriou added 3 commits April 3, 2023 17:12
@joelriou
feat: port CategoryTheory.Sites.Sheaf
ce53c85
@joelriou
Initial file copy from mathport
0563c6e
@joelriou
automated fixes
63ee893 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@joelriou joelriou added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 3, 2023
@joelriou joelriou removed the WIP Work in progress label Apr 4, 2023
@kim-em kim-em mentioned this pull request Apr 5, 2023
Closed
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 5, 2023

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Apr 5, 2023

✌️ joelriou 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 This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Apr 5, 2023
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Apr 5, 2023 •
edited
Loading

Actually, the proof of Preadditive (Sheaf J A) is now very fast with your change @semorrison . It is the previous definition Sheaf.Hom.addCommGroup which is taking some time.

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Apr 5, 2023

bord r+

@Parcly-Taxel
Copy link
Copy Markdown
Collaborator

Parcly-Taxel commented Apr 5, 2023 •
edited
Loading

@joelriou You made a typo with the command there...

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Apr 5, 2023

bors r+

bors bot pushed a commit that referenced this pull request Apr 5, 2023
@joelriou @kim-em
feat: port CategoryTheory.Sites.Sheaf (#3244)
50dc55d 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Apr 5, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port CategoryTheory.Sites.Sheaf [Merged by Bors] - feat: port CategoryTheory.Sites.Sheaf Apr 5, 2023
@bors bors bot closed this Apr 5, 2023
@bors bors bot deleted the port/CategoryTheory.Sites.Sheaf branch April 5, 2023 13:52
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Apr 8, 2023
@kim-em
chore(category_theory): simps should not add hom lemmas (#18742)
2efd242 
`@[simps]` should not be used to simplify the `hom` field of a category instance.

Very little needs to be changed when removing it.

However the problem in leanprover-community/mathlib4#3244 with a proof by `simp` failing seems to be implicated by this problem. If we remove the `@[simps]` generated lemma for `Hom` there, the original proof works (although is extremely slow).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
MonadMaverick pushed a commit that referenced this pull request Apr 9, 2023
@joelriou @kim-em @MonadMaverick
feat: port CategoryTheory.Sites.Sheaf (#3244)
e189d82 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
MonadMaverick pushed a commit to MonadMaverick/mathlib4 that referenced this pull request Apr 9, 2023
@joelriou @kim-em @MonadMaverick
feat: port CategoryTheory.Sites.Sheaf (leanprover-community#3244)
001afdf 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). mathlib-port This is a port of a theory file from mathlib.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@joelriou @kim-em @Parcly-Taxel