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 presheaves of modules has limits #12264

Closed
wants to merge 76 commits into from
Closed

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

wants to merge 76 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
@joelriou joelriou added the t-category-theory Category theory label Apr 19, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Apr 19, 2024
@joelriou joelriou mentioned this pull request Apr 19, 2024
Closed
2 tasks
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Apr 19, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@joelriou joelriou added awaiting-review The author would like community review of the PR awaiting-CI labels Apr 19, 2024
erdOne
erdOne reviewed Apr 20, 2024
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.

Otherwise LGTM

Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean Outdated Show resolved Hide resolved
@erdOne erdOne 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 20, 2024
@joelriou @erdOne
Update Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean
7c97704 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@joelriou joelriou 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 Apr 20, 2024
@erdOne
Copy link
Member

erdOne commented Apr 20, 2024

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by erdOne.

jcommelin
jcommelin reviewed Apr 20, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Apr 20, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 20, 2024
@joelriou @chrisflav
feat(Algebra/Category/ModuleCat): the category of presheaves of modul…
5d9cf93 
…es has limits (#12264)

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Christian Merten <christian@merten.dev>
@mathlib-bors
Copy link

mathlib-bors bot commented Apr 20, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Category/ModuleCat): the category of presheaves of modules has limits [Merged by Bors] - feat(Algebra/Category/ModuleCat): the category of presheaves of modules has limits Apr 20, 2024
@mathlib-bors mathlib-bors bot closed this Apr 20, 2024
@mathlib-bors mathlib-bors bot deleted the RingMod4 branch April 20, 2024 21:59
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@joelriou @chrisflav @callesonne
feat(Algebra/Category/ModuleCat): the category of presheaves of modul…
11418af 
…es has limits (#12264)

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Christian Merten <christian@merten.dev>
Jun2M pushed a commit that referenced this pull request Apr 24, 2024
@joelriou @chrisflav @Jun2M
feat(Algebra/Category/ModuleCat): the category of presheaves of modul…
4f570cc 
…es has limits (#12264)

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
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

@jcommelin jcommelin jcommelin left review comments

@erdOne erdOne erdOne left review comments

Assignees
No one assigned
Labels
maintainer-merge 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 @jcommelin @chrisflav