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

feat(Algebra/Category/ModuleCat): pullback of presheaves of modules #17366

Open
wants to merge 64 commits into
base: master
Choose a base branch
from
Open

feat(Algebra/Category/ModuleCat): pullback of presheaves of modules #17366

wants to merge 64 commits into from
+307 −0

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented Oct 2, 2024 •
edited
Loading

@joelriou
refactoring ModuleCat.Presheaf
e3f0045
@joelriou
wip
00ead34
@joelriou
fixed Presheaf.Limits
39a0013
@joelriou
fix docstrings
458a34c
@joelriou
fixed Presheaf.Colimits
4986072
@joelriou
wip
2f85fa6
@joelriou
fixed ModuleCat.Sheaf
47b3337
@joelriou
fixed Sheaf.ChangeOfRings
bcb4088
@joelriou
fixed Presheaf.Sheafify
61d4ac8
@joelriou
wip
ae99ab9
@joelriou
fixed Presheaf.Sheafification
94eb640
@joelriou
fixed Differentials.Presheaf
ade38cf
@joelriou
feat(Algebra/Category/ModuleCat): the free presheaf of modules functor
919b915
@joelriou
AIM note
ab3f04b
@joelriou
fixing AG.Modules.Tilde
f7e9796
@joelriou
cleaning up
e0eccec
@joelriou
Merge remote-tracking branch 'origin/refactor-presheaf-of-modules' in…
aae13f3 
…to the-free-presheaf-of-modules-on-a-presheaf-of-sets
@joelriou
fixed GroupCohomology.Resolution
177dbdf
@joelriou
cleaning up
be238ef
@joelriou
cleaning up
e833541
@joelriou
Merge remote-tracking branch 'origin/refactor-presheaf-of-modules' in…
3c589a0 
…to the-free-presheaf-of-modules-on-a-presheaf-of-sets
@joelriou
added docstrings
1e15c86
@joelriou
Merge remote-tracking branch 'origin' into the-free-presheaf-of-modul…
b0edaa3 
…es-on-a-presheaf-of-sets
@joelriou
fixing the build
6b0c727
@joelriou
cleaning up
68d109c
@joelriou
coding style
f9171f7
@joelriou
typo
aab62c4
@joelriou
Merge remote-tracking branch 'origin' into the-free-presheaf-of-modul…
f168dc3 
…es-on-a-presheaf-of-sets
@joelriou
Merge remote-tracking branch 'origin' into the-free-presheaf-of-modul…
4fb41e7 
…es-on-a-presheaf-of-sets
@joelriou
Merge remote-tracking branch 'origin' into the-free-presheaf-of-modul…
8adc243 
…es-on-a-presheaf-of-sets
@joelriou joelriou mentioned this pull request Oct 4, 2024
Closed
1 task
This was referenced Oct 6, 2024
Open
Open
Open
Open
@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
@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 19, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 23, 2024
@joelriou
feat(CategoryTheory/Adjunction): the left partial adjoint (#17388)
c48f8a2 
Given a functor `F : D ⥤ C`, we define a functor`F.partialLeftAdjoint : F.PartialLeftAdjointSource ⥤ D` which is defined on a certain full subcategory of `C`. It satisfies similar properties to the left adjoint of `F` (if this existed). We show that the domain of definition of this partial left adjoint is stable under certain colimits.

This shall be used in #17366 in order to show the existence of the pullback functor on categories of presheaves of modules.
@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 23, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Oct 24, 2024
@mathlib4-dependent-issues-bot
Copy link
Collaborator

mathlib4-dependent-issues-bot commented Oct 24, 2024 •
edited
Loading

This PR/issue depends on:

@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 24, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Oct 24, 2024
@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 24, 2024
@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 24, 2024
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
blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-algebraic-geometry Algebraic geometry t-category-theory Category theory WIP Work in progress
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@joelriou @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant