Skip to content

[Merged by Bors] - feat(Algebra/Category/ModuleCat): the free presheaf of modules on a presheaf of sets#16755

Closed
joelriou wants to merge 37 commits intomasterfrom
the-free-presheaf-of-modules-on-a-presheaf-of-sets
Closed

[Merged by Bors] - feat(Algebra/Category/ModuleCat): the free presheaf of modules on a presheaf of sets#16755
joelriou wants to merge 37 commits intomasterfrom
the-free-presheaf-of-modules-on-a-presheaf-of-sets

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Sep 13, 2024 •
edited by alreadydone
Loading

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Co-authored-by: Johan Commelin johan@commelin.net

Thanks to the refactor #16667, this is a better attempt as compared to #14245.

Open in Gitpod

@joelriou joelriou added WIP Work in progress workshop-AIM-AG-2024 This PR is associated with the 2024 AIM workshop on formalization of algebraic geometry labels Sep 13, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 13, 2024 •
edited
Loading

PR summary a64fc64f3c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Algebra.Category.ModuleCat.Presheaf.Free 1235

Declarations diff

+ adj_homEquiv
+ free
+ freeAdjunction
+ freeAdjunctionUnit
+ freeAdjunction_homEquiv
+ freeAdjunction_unit_app
+ freeDesc
+ freeDesc_apply
+ freeMk
+ freeObj
+ freeObjDesc
+ free_map_apply
+ sheafificationAdjunction_homEquiv_apply
++ freeHomEquiv
++ free_hom_ext
- sheaififcationAdjunction_homEquiv_apply

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@joelriou joelriou mentioned this pull request Sep 13, 2024
Closed
@joelriou joelriou mentioned this pull request Sep 13, 2024
Closed
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 13, 2024
@joelriou joelriou mentioned this pull request Sep 13, 2024
Closed
@joelriou joelriou changed the title The free presheaf of modules on a presheaf of sets feat(Algebra/Category/ModulaCat): the free presheaf of modules on a presheaf of sets Sep 13, 2024
@joelriou joelriou mentioned this pull request Oct 2, 2024
Closed
5 tasks
jcommelin
jcommelin approved these changes Oct 4, 2024
View reviewed changes
Copy link
Copy Markdown
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.

LGTM, but I was involved in writing parts of this.

This was referenced Oct 6, 2024
Open
Open
Closed
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 14, 2024
chrisflav
chrisflav reviewed Oct 15, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@chrisflav chrisflav left a comment

Choose a reason for hiding this comment

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

This looks good to me. You need to merge master and I left some small comments.

joelriou and others added 4 commits October 16, 2024 23:01
@joelriou @chrisflav
Update Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean
57e0f82 
Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
@joelriou @chrisflav
Update Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean
ef7b629 
Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
@joelriou @chrisflav
Update Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean
da136e0 
Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>
@joelriou
Merge remote-tracking branch 'origin' into the-free-presheaf-of-modul…
0d8e10b 
…es-on-a-presheaf-of-sets
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Oct 16, 2024

Thanks @chrisflav for your suggestions!

@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 16, 2024
@jcommelin jcommelin changed the title feat(Algebra/Category/ModulaCat): the free presheaf of modules on a presheaf of sets feat(Algebra/Category/ModuleCat): the free presheaf of modules on a presheaf of sets Oct 17, 2024
chrisflav
chrisflav approved these changes Oct 17, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@chrisflav chrisflav left a comment

Choose a reason for hiding this comment

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

Thanks, LGTM!

erdOne
erdOne reviewed Oct 17, 2024
View reviewed changes
erdOne
erdOne reviewed Oct 17, 2024
View reviewed changes
jcommelin and others added 3 commits October 17, 2024 13:23
@jcommelin @erdOne
Apply suggestions from code review
fc1e0b7 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@joelriou @github-actions
Update Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean
96dbd10 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@joelriou
Merge remote-tracking branch 'origin' into the-free-presheaf-of-modul…
a64fc64 
…es-on-a-presheaf-of-sets
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Oct 19, 2024

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 19, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 19, 2024
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Oct 24, 2024

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 24, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 24, 2024
@joelriou @jcommelin
feat(Algebra/Category/ModuleCat): the free presheaf of modules on a p…
893b3a8 
…resheaf of sets (#16755)


This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Co-authored-by: Johan Commelin <johan@commelin.net>



Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Johan Commelin <johan@commelin.net>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 24, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Algebra/Category/ModuleCat): the free presheaf of modules on a presheaf of sets [Merged by Bors] - feat(Algebra/Category/ModuleCat): the free presheaf of modules on a presheaf of sets Oct 24, 2024
@mathlib-bors mathlib-bors bot closed this Oct 24, 2024
@mathlib-bors mathlib-bors bot deleted the the-free-presheaf-of-modules-on-a-presheaf-of-sets branch October 24, 2024 07:32
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

@jcommelin jcommelin jcommelin approved these changes

@chrisflav chrisflav chrisflav approved these changes

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) workshop-AIM-AG-2024 This PR is associated with the 2024 AIM workshop on formalization of algebraic geometry

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@joelriou @mathlib4-dependent-issues-bot @erdOne @riccardobrasca @jcommelin @chrisflav @leanprover-community-bot-assistant