Skip to content

feat(Algebra/Category/ModuleCat/Presheaf): the colimit module of a presheaf of modules on a cofiltered category#37369

Open
joelriou wants to merge 1 commit intoleanprover-community:masterfrom
joelriou:modulecat-presheaf-colimitfunctor
Open

feat(Algebra/Category/ModuleCat/Presheaf): the colimit module of a presheaf of modules on a cofiltered category#37369
joelriou wants to merge 1 commit intoleanprover-community:masterfrom
joelriou:modulecat-presheaf-colimitfunctor

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Mar 30, 2026

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Mar 30, 2026
@joelriou joelriou mentioned this pull request Mar 30, 2026
Open
11 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 30, 2026

PR summary b84059846b

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Filtered.FinallySmall 1
Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (new file) 1285

Declarations diff

+ ModuleColimit
+ coconeSMul
+ colimitFunctor
+ comp_map
+ instance : AddCommGroup (ModuleColimit hcR hcM)
+ instance : Module cR.pt (ModuleColimit hcR hcM)
+ instance : SMul cR.pt (ModuleColimit hcR hcM)
+ jointly_surjective₂
+ jointly_surjective₃
+ jointly_surjective₃'
+ map
+ map_apply
+ map_id
+ preservesColimitsOfShape_of_isFiltered
+ smul_eq
+ ιM
+ ιM_jointly_surjective
+ ιM_jointly_surjective₂
+ ιM_jointly_surjective₃
+ ιR
+ ιR_jointly_surjective

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

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

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

Increase in tech debt: (relative, absolute) = (1.34, 0.00)
Current number Change Type
635 1 erw
6893 5 backward.isDefEq

Current commit 561064a9fa
Reference commit b84059846b

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

erdOne
erdOne reviewed Mar 31, 2026
View reviewed changes
Copy link
Copy Markdown
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.

I wonder if CategoryTheory.Limits.colimit.smul is useful here.

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Mar 31, 2026 •
edited
Loading

I wonder if CategoryTheory.Limits.colimit.smul is useful here.

This is essentially the same construction as in this file, but with the exact assumptions which allow to use the more general GrothendieckTopology.Point API. At some point, my intent would be to refactor the construction of stalks of (pre)sheaves of modules on topological spaces.

dagurtomas
dagurtomas reviewed Apr 2, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas left a comment

Choose a reason for hiding this comment

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

Thanks!

maintainer merge

Mathlib/Algebra/Category/ModuleCat/Presheaf/ColimitFunctor.lean
have h₂ := ConcreteCategory.congr_hom (hcM.fac c U) m
dsimp [c] at h₁ h₂ ⊢
rw [ModuleColimit.smul_eq]
erw [h₁, h₂, ModuleColimit.smul_eq, ← (f.app U).hom.map_smul]
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas Apr 2, 2026

Choose a reason for hiding this comment

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

I tried very hard to get rid of this erw, I thought it had something to do with the type synonym but I don't think that's the problem, it's probably more related to PresheafOfModules.presheaf API

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 2, 2026

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

@mathlib-triage mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 2, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dagurtomas dagurtomas dagurtomas left review comments

@erdOne erdOne erdOne left review comments

Assignees

@dagurtomas dagurtomas

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@joelriou @dagurtomas @erdOne