feat(AlgebraicGeometry): the pseudofunctor which sends a scheme to its category of sheaves of modules #30350

joelriou · 2025-10-08T21:27:21Z

We define Scheme.Modules.pseudofunctor : Pseudofunctor (LocallyDiscrete Schemeᵒᵖ) (Adj Cat) which sends a scheme X to the category X.Modules of sheaves of modules (not to be be confused with the full subcategory of quasi-coherent sheaves). The target bicategory is the bicategory of adjunctions in the bicategory of categories: this means that we formalise both the pushforward and the pullback of sheaves of modules over schemes.

depends on: [Merged by Bors] - feat(CategoryTheory/Adjunction): more mate compatibilities #30335
depends on: [Merged by Bors] - feat(Algebra/ModuleCat/Presheaf): composition of pushforwards and pullbacks and compatibilites #30318
depends on: [Merged by Bors] - feat(Algebra/Category/ModuleCat/Sheaf): compatibilities of pushforward and pullbacks on sheaves of modules #30342

…to the-free-presheaf-of-modules-on-a-presheaf-of-sets

…es-on-a-presheaf-of-sets

github-actions · 2025-10-08T21:28:35Z

PR summary 337d737cae

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Adjunction.toCat_id
+ Hom
+ Hom.toRingCatSheafHom
+ conjugateEquiv_eq_categoryTheoryConjugateEquiv
+ conjugateEquiv_leftAdjointCompIso_inv
+ conjugateEquiv_leftAdjointIdIso_hom
+ instance : Abelian X.Modules
+ instance : Category X.Modules
+ instance : Preadditive X.Modules
+ instance {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
+ mateEquiv_eq_categoryTheoryMateEquiv
+ ofCat
+ ofCat_toCat
+ pseudofunctor
+ pseudofunctor_associativity
+ pseudofunctor_left_unitality
+ pseudofunctor_right_unitality
+ pullback
+ pullbackComp
+ pullbackId
+ pullbackPushforwardAdjunction
+ pushforward
+ pushforwardComp
+ pushforwardId
+ toCat
+ toCat_comp_toCat
+ toCat_ofCat
++ conjugateEquiv_pullbackComp_inv
++ conjugateEquiv_pullbackId_hom
- instance : Abelian X.Modules := inferInstance
- instance : HasSheafify (Opens.grothendieckTopology X) AddCommGrpCat.{u}

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.

No changes to technical debt.

You can run this locally as

./scripts/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).

mathlib4-merge-conflict-bot · 2025-10-12T19:34:37Z

This pull request has conflicts, please merge master and resolve them.

…dofunctor

mathlib4-merge-conflict-bot · 2025-11-19T08:13:41Z

This pull request has conflicts, please merge master and resolve them.

mathlib4-dependent-issues-bot · 2025-11-20T13:50:47Z

This PR/issue depends on:

~~[Merged by Bors] - feat(CategoryTheory/Adjunction): more mate compatibilities #30335~~
~~[Merged by Bors] - feat(Algebra/ModuleCat/Presheaf): composition of pushforwards and pullbacks and compatibilites #30318~~
~~[Merged by Bors] - feat(Algebra/Category/ModuleCat/Sheaf): compatibilities of pushforward and pullbacks on sheaves of modules #30342~~
By Dependent Issues (🤖). Happy coding!

…dofunctor

erdOne · 2025-11-21T10:16:15Z

Mathlib/CategoryTheory/Bicategory/Adjunction/Cat.lean

+attribute [local simp] bicategoricalComp Cat.associator_hom_app Cat.associator_inv_app
+  Cat.leftUnitor_hom_app Cat.leftUnitor_inv_app Cat.rightUnitor_hom_app Cat.rightUnitor_inv_app
+  Functor.toCatHom


Should this be a simp set?

erdOne · 2025-11-21T10:17:33Z

Mathlib/CategoryTheory/Bicategory/Adjunction/Cat.lean

+abbrev toCat : Bicategory.Adjunction F.toCatHom G.toCatHom where
+  unit := adj.unit
+  counit := adj.counit
+
+/-- The adjunction of functors corresponding to an adjunction in the bicategory `Cat`. -/
+abbrev ofCat {C D : Cat} {F : C ⟶ D} {G : D ⟶ C}
+    (adj : Bicategory.Adjunction F G) :
+    Functor.ofCatHom F ⊣ Functor.ofCatHom G where
+  unit := adj.unit
+  counit := adj.counit
+  left_triangle_components X := by simpa using congr_app adj.left_triangle X
+  right_triangle_components X := by simpa using congr_app adj.right_triangle X


Why are these abbrevs?

erdOne · 2025-11-21T10:17:50Z

Mathlib/CategoryTheory/Bicategory/Adjunction/Cat.lean

+namespace Bicategory
+
+@[simp]
+lemma Adjunction.toCat_id (C : Cat.{v, u}) :


Suggested change

lemma Adjunction.toCat_id (C : Cat.{v, u}) :

lemma Adjunction.ofCat_id (C : Cat.{v, u}) :

erdOne · 2025-11-21T10:18:51Z

Mathlib/CategoryTheory/Adjunction/CompositionIso.lean

+and show that the left adjoint functors satisfies properties similar to the left/right
 unitality and the associativity of pseudofunctors if the right adjoint functors
-satisfy the corresponding properties.
+satisfies the corresponding properties.


I think satisfy was correct?

erdOne · 2025-11-21T10:19:40Z

Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

+attribute [simps! obj_obj map_l map_r map_adj] pseudofunctor
+attribute [simps! mapId_hom_τl mapId_hom_τr mapId_inv_τl mapId_inv_τr] pseudofunctor
+attribute [simps! mapComp_hom_τl mapComp_hom_τr] pseudofunctor
+attribute [simps! mapComp_inv_τl mapComp_inv_τr] pseudofunctor


Why are these done separately? Is it because it times out otherwise?

erdOne · 2025-11-22T12:15:21Z

Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

+/-- The morphism of sheaves of rings corresponding to a morphism of schemes. -/
+def Hom.toRingCatSheafHom (f : X ⟶ Y) :
+    Y.ringCatSheaf ⟶ ((TopologicalSpace.Opens.map f.base).sheafPushforwardContinuous
+      _ _ _).obj X.ringCatSheaf where
+  val := Functor.whiskerRight f.c _


I think this should go near Scheme.ringCatSheaf

joelriou added 30 commits September 10, 2024 15:27

refactoring ModuleCat.Presheaf

e3f0045

wip

00ead34

fixed Presheaf.Limits

39a0013

fix docstrings

458a34c

fixed Presheaf.Colimits

4986072

wip

2f85fa6

fixed ModuleCat.Sheaf

47b3337

fixed Sheaf.ChangeOfRings

bcb4088

fixed Presheaf.Sheafify

61d4ac8

wip

ae99ab9

fixed Presheaf.Sheafification

94eb640

fixed Differentials.Presheaf

ade38cf

feat(Algebra/Category/ModuleCat): the free presheaf of modules functor

919b915

AIM note

ab3f04b

fixing AG.Modules.Tilde

f7e9796

cleaning up

e0eccec

Merge remote-tracking branch 'origin/refactor-presheaf-of-modules' in…

aae13f3

…to the-free-presheaf-of-modules-on-a-presheaf-of-sets

fixed GroupCohomology.Resolution

177dbdf

cleaning up

be238ef

cleaning up

e833541

Merge remote-tracking branch 'origin/refactor-presheaf-of-modules' in…

3c589a0

…to the-free-presheaf-of-modules-on-a-presheaf-of-sets

added docstrings

1e15c86

Merge remote-tracking branch 'origin' into the-free-presheaf-of-modul…

b0edaa3

…es-on-a-presheaf-of-sets

fixing the build

6b0c727

cleaning up

68d109c

coding style

f9171f7

typo

aab62c4

Merge remote-tracking branch 'origin' into the-free-presheaf-of-modul…

f168dc3

…es-on-a-presheaf-of-sets

Merge remote-tracking branch 'origin' into the-free-presheaf-of-modul…

4fb41e7

…es-on-a-presheaf-of-sets

Merge remote-tracking branch 'origin' into the-free-presheaf-of-modul…

8adc243

…es-on-a-presheaf-of-sets

better instances

daabf75

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 Oct 8, 2025

joelriou added 3 commits October 9, 2025 10:03

sorry free

e931f34

cleaning up

823ecd4

docstrings

31e9b54

mathlib4-merge-conflict-bot 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 12, 2025

Merge remote-tracking branch 'origin/master' into scheme-modules-pseu…

fa58352

…dofunctor

github-actions bot 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 30, 2025

joelriou mentioned this pull request Nov 18, 2025

[Merged by Bors] - feat(CategoryTheory/Sites): descent data #30189

Closed

3 tasks

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 20, 2025

joelriou added the WIP Work in progress label Nov 20, 2025

Merge remote-tracking branch 'origin/master' into scheme-modules-pseu…

8789b59

…dofunctor

github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Nov 20, 2025

joelriou mentioned this pull request Nov 20, 2025

chore(AlgebraicGeometry): API for 𝒪ₓ-modules #31854

Open

joelriou added 3 commits November 20, 2025 17:51

wip

54fd231

Merge remote-tracking branch 'origin/master' into scheme-modules-pseu…

4b0cc0f

…dofunctor

clean up

f596d5d

joelriou removed the WIP Work in progress label Nov 21, 2025

joelriou added 3 commits November 21, 2025 08:43

better def

eae0291

better syntax

f58746b

better syntax

09de33f

erdOne reviewed Nov 21, 2025

View reviewed changes

erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 21, 2025

erdOne reviewed Nov 22, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(AlgebraicGeometry): the pseudofunctor which sends a scheme to its category of sheaves of modules #30350

feat(AlgebraicGeometry): the pseudofunctor which sends a scheme to its category of sheaves of modules #30350

joelriou commented Oct 8, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Oct 8, 2025 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Oct 12, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Nov 20, 2025

Uh oh!

erdOne Nov 21, 2025

Uh oh!

erdOne Nov 21, 2025

Uh oh!

erdOne Nov 21, 2025

Uh oh!

erdOne Nov 21, 2025

Uh oh!

erdOne Nov 21, 2025

Uh oh!

erdOne Nov 22, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

	lemma Adjunction.toCat_id (C : Cat.{v, u}) :
	lemma Adjunction.ofCat_id (C : Cat.{v, u}) :

feat(AlgebraicGeometry): the pseudofunctor which sends a scheme to its category of sheaves of modules #30350

Are you sure you want to change the base?

feat(AlgebraicGeometry): the pseudofunctor which sends a scheme to its category of sheaves of modules #30350

Conversation

joelriou commented Oct 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 337d737cae

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Oct 12, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Nov 20, 2025

Uh oh!

erdOne Nov 21, 2025

Choose a reason for hiding this comment

Uh oh!

erdOne Nov 21, 2025

Choose a reason for hiding this comment

Uh oh!

erdOne Nov 21, 2025

Choose a reason for hiding this comment

Uh oh!

erdOne Nov 21, 2025

Choose a reason for hiding this comment

Uh oh!

erdOne Nov 21, 2025

Choose a reason for hiding this comment

Uh oh!

erdOne Nov 22, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

joelriou commented Oct 8, 2025 •

edited

Loading

github-actions bot commented Oct 8, 2025 •

edited

Loading