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(Algebra/Category/ModuleCat): the category of sheaves of modules has limits #12269

Closed
wants to merge 82 commits into from
Closed

[Merged by Bors] - feat(Algebra/Category/ModuleCat): the category of sheaves of modules has limits #12269

wants to merge 82 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented Apr 19, 2024 •
edited

@joelriou
feat: construction of a presheaf of modules from a family of modules …
4edf7bc 
…over various rings
@joelriou
better docstring
e86e60e
@joelriou
Merge remote-tracking branch 'origin' into RingMod4
5ddace8
@joelriou
mostly done a draft of PresheafOfModules.evaluationJointlyReflectsLimits
c1c955f
@joelriou
some progress
5681094
@joelriou
some progress
6424f53
@joelriou
most done the construction of limits
3db3da4
@joelriou
code cleaning
95f6113
@joelriou
oops it is already in mathlib
cbff82d
@joelriou
code cleaning
effae41
@joelriou
feat(Algebra/Category/ModuleCat): composition of restriction of scala…
6e8802e 
…r functors
@joelriou
Merge remote-tracking branch 'origin/restrictScalarsComp' into RingMod4
9c5cda0
@joelriou
s/CategoryTheory.ModuleCat/ModuleCat/
f472969
@joelriou
Merge remote-tracking branch 'origin/restrictScalarsComp' into RingMod4
fa27667
@joelriou
merging with restrictScalarsComp
4ebce35
@joelriou
Merge remote-tracking branch 'origin/restrictScalarsComp' into RingMod3
1ad3404
@joelriou
tidied the code
ebeeeb4
@joelriou
add constructors
9653459
@joelriou
pleasing lint
69ed435
@joelriou
Merge remote-tracking branch 'origin/restrictScalarsComp' into RingMod3
5f73d69
@joelriou
better docstring
3b5368e
@joelriou
removed unnecessary def
7790048
@joelriou
more coherent coding style
4beea94
@joelriou
Merge remote-tracking branch 'origin/restrictScalarsComp' into RingMod3
69eebe1
@joelriou
Merge remote-tracking branch 'origin/RingMod3' into RingMod4
5d2f1ff
@joelriou
finished the construction of limits in the category of presheaves of …
1d4a34f 
…modules
@joelriou
mostly done the colimits in the category of presheaves of modules
2188a8a
@joelriou
Merge remote-tracking branch 'origin' into restrictScalarsComp
b39aa9d
@joelriou
Merge remote-tracking branch 'origin/restrictScalarsComp' into RingMod3
c006048
@joelriou
Merge remote-tracking branch 'origin/RingMod3' into RingMod4
924d55c
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 20, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 20, 2024
@joelriou joelriou added the awaiting-review The author would like community review of the PR label Apr 21, 2024
@joelriou joelriou 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 Apr 23, 2024
@joelriou joelriou added awaiting-review The author would like community review of the PR awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 25, 2024
@erdOne
Copy link
Member

erdOne commented Apr 27, 2024

Thanks!
maintainer merge

@riccardobrasca
Copy link
Member

Thanks!

bors d+

@mathlib-bors
Copy link

mathlib-bors bot commented Apr 30, 2024

✌️ 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 and removed awaiting-review The author would like community review of the PR labels Apr 30, 2024
@joelriou
Copy link
Collaborator Author

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Apr 30, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
@joelriou @chrisflav
feat(Algebra/Category/ModuleCat): the category of sheaves of modules …
fbdfab9 
…has limits (#12269)

Co-authored-by: Christian Merten <christian@merten.dev>
@mathlib-bors
Copy link

mathlib-bors bot commented Apr 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Category/ModuleCat): the category of sheaves of modules has limits [Merged by Bors] - feat(Algebra/Category/ModuleCat): the category of sheaves of modules has limits Apr 30, 2024
@mathlib-bors mathlib-bors bot closed this Apr 30, 2024
@mathlib-bors mathlib-bors bot deleted the RingMod5 branch April 30, 2024 16:16
apnelson1 pushed a commit that referenced this pull request May 12, 2024
@joelriou @chrisflav @apnelson1
feat(Algebra/Category/ModuleCat): the category of sheaves of modules …
31aec71 
…has limits (#12269)

Co-authored-by: Christian Merten <christian@merten.dev>
callesonne pushed a commit that referenced this pull request May 16, 2024
@joelriou @chrisflav @callesonne
feat(Algebra/Category/ModuleCat): the category of sheaves of modules …
a7918f1 
…has limits (#12269)

Co-authored-by: Christian Merten <christian@merten.dev>
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 ready-to-merge This PR has been sent to bors. t-category-theory Category theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@joelriou @leanprover-community-mathlib4-bot @erdOne @riccardobrasca @chrisflav