feat(AlgebraicGeometry): The pushforward of a quasi-coherent sheaf between affines is quasi-coherent by Brian-Nugent · Pull Request #37189 · leanprover-community/mathlib4

Brian-Nugent · 2026-03-25T23:44:03Z

To be more precise, we show that if AlgebraicGeometry.Scheme.Modules.fromTildeΓ is an isomorphism then the same holds for the pushforward. This will show that being quasicoherent is stable under pushforward for affine morphisms once it is shown that AlgebraicGeometry.Scheme.Modules.fromTildeΓ being an isomorphism is equivalent to being quasicoherent.

github-actions · 2026-03-25T23:44:16Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-03-25T23:45:23Z

PR summary 2d59066e04

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.AlgebraicGeometry.Modules.Tilde	2339	2357	+18 (+0.77%)

Import changes for all files

Files	Import difference
`Mathlib.AlgebraicGeometry.Modules.Tilde`	18

Declarations diff

+ IsLocalizedModule.comp_iff_of_bijective_left
+ IsLocalizedModule.comp_iff_of_bijective_right
+ IsLocalizedModule.restrictScalars
+ IsLocalizedModule.restrictScalars_iff
+ IsLocalizedModule.restrictScalars_powers
+ IsLocalizing
+ instance : (modulesSpecToSheaf (R := R)).Faithful := SpecModulesToSheafFullyFaithful.faithful
+ instance : (modulesSpecToSheaf (R := R)).Full := SpecModulesToSheafFullyFaithful.full
+ isIso_fromTildeΓ_iff_isLocalizing
+ isIso_iff_isIso_basis
+ isIso_of_isLocalizedModule_comp
+ isLocalizing_iff_of_iso
+ isLocalizing_of_isIso_app_top
+ isLocalizing_of_iso
+ isLocalizing_pushforward_of_isLocalizing
+ isLocalizing_tilde
+ linearEquiv_of_isLocalizedModule_comp
+ pushforwardCompForgetToSheafModuleCat
+ pushforward_isIso_fromTildeΓ
+ pushforward_modulesSpecToSheaf_iso
+ sheafComposePushforwardComp

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
6176	1	backward.isDefEq.respectTransparency

Current commit 8797ae0185
Reference commit 2d59066e04

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

…lib4 into pushforward-qc

joelriou · 2026-04-06T15:56:20Z

+def pushforward_modulesSpecToSheaf_iso :
+    Scheme.Modules.pushforward (Spec.map φ) ⋙ modulesSpecToSheaf ≅
+    modulesSpecToSheaf ⋙ TopCat.Sheaf.pushforward (ModuleCat S) (Spec.map φ).base ⋙
+    sheafCompose _ (ModuleCat.restrictScalars φ.hom) := eqToIso (by
+  conv_lhs =>


We probably want to have a better definition of this isomorphism.

Better in what way? Where the hom and inverse are specified to have some nice definitional properties?

Since this is an isomorphism of functors, a good start would be to use NatIso.ofComponents.

Would NatIso.ofComponents fun X => (eqToIso ...) be a good definition?

Or since the objects in this case are sheaves, maybe we'd want to put the eqToIso another step deeper?

We should not use eqToIso at all. Generally, the trick for this type of isomorphism is to just keep applying things like NatIso.ofComponents and use dsimp very liberally to simplify the situation (without breaking def-eqs). Then we usually already have the components somewhere. By following this strategy, you get this:

set_option backward.isDefEq.respectTransparency false in def _root_.SheafOfModules.pushforwardCompForgetToSheafModuleCat {C : Type*} [Category* C] {D : Type*} [Category* D] {J : GrothendieckTopology C} {K : GrothendieckTopology D} {F : C ⥤ D} {R : Sheaf K RingCat.{u}} {S : Sheaf J RingCat.{u}} [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat.{u} J K).obj R) (X : Cᵒᵖ) (hX : IsInitial X) (hX' : IsInitial (F.op.obj X)) : SheafOfModules.pushforward φ ⋙ SheafOfModules.forgetToSheafModuleCat _ X hX ≅ SheafOfModules.forgetToSheafModuleCat _ _ hX' ⋙ sheafCompose K (ModuleCat.restrictScalars <| (φ.hom.app _).hom) ⋙ F.sheafPushforwardContinuous _ J K := by refine NatIso.ofComponents (fun M ↦ ObjectProperty.isoMk _ ?_) ?_ · refine NatIso.ofComponents (fun U ↦ ?_) ?_ · refine (ModuleCat.restrictScalarsComp'App _ _ _ ?_ _).symm ≪≫ (ModuleCat.restrictScalarsComp _ _).app _ rw [← RingCat.hom_comp, ← RingCat.hom_comp, φ.hom.naturality] dsimp rw [hX'.hom_ext (hX'.to (op (F.obj (unop U)))) _] · cat_disch · cat_disch

The special case you have here you should be able to obtain easily from the general case.

Thank you for this! I've incorporated this but I think something still needs to be done to deal with the sheafCompose in the definition of modulesSpecToSheaf. My attempt at dealing with this is sheafComposePushforwardComp (see my comment below). I can make this more general but I first wanted to check to make sure this is reasonable and gives a good definition for pushforward_modulesSpecToSheaf_iso.

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

chrisflav · 2026-04-23T13:56:17Z

+def pushforward_modulesSpecToSheaf_iso :
+    Scheme.Modules.pushforward (Spec.map φ) ⋙ modulesSpecToSheaf ≅
+    modulesSpecToSheaf ⋙ TopCat.Sheaf.pushforward (ModuleCat S) (Spec.map φ).base ⋙
+    sheafCompose _ (ModuleCat.restrictScalars φ.hom) := eqToIso (by
+  conv_lhs =>


Since this is an isomorphism of functors, a good start would be to use NatIso.ofComponents.

chrisflav · 2026-05-01T20:51:43Z

+def pushforward_modulesSpecToSheaf_iso :
+    Scheme.Modules.pushforward (Spec.map φ) ⋙ modulesSpecToSheaf ≅
+    modulesSpecToSheaf ⋙ TopCat.Sheaf.pushforward (ModuleCat S) (Spec.map φ).base ⋙
+    sheafCompose _ (ModuleCat.restrictScalars φ.hom) := eqToIso (by
+  conv_lhs =>


We should not use eqToIso at all. Generally, the trick for this type of isomorphism is to just keep applying things like NatIso.ofComponents and use dsimp very liberally to simplify the situation (without breaking def-eqs). Then we usually already have the components somewhere. By following this strategy, you get this:

set_option backward.isDefEq.respectTransparency false in def _root_.SheafOfModules.pushforwardCompForgetToSheafModuleCat {C : Type*} [Category* C] {D : Type*} [Category* D] {J : GrothendieckTopology C} {K : GrothendieckTopology D} {F : C ⥤ D} {R : Sheaf K RingCat.{u}} {S : Sheaf J RingCat.{u}} [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat.{u} J K).obj R) (X : Cᵒᵖ) (hX : IsInitial X) (hX' : IsInitial (F.op.obj X)) : SheafOfModules.pushforward φ ⋙ SheafOfModules.forgetToSheafModuleCat _ X hX ≅ SheafOfModules.forgetToSheafModuleCat _ _ hX' ⋙ sheafCompose K (ModuleCat.restrictScalars <| (φ.hom.app _).hom) ⋙ F.sheafPushforwardContinuous _ J K := by refine NatIso.ofComponents (fun M ↦ ObjectProperty.isoMk _ ?_) ?_ · refine NatIso.ofComponents (fun U ↦ ?_) ?_ · refine (ModuleCat.restrictScalarsComp'App _ _ _ ?_ _).symm ≪≫ (ModuleCat.restrictScalarsComp _ _).app _ rw [← RingCat.hom_comp, ← RingCat.hom_comp, φ.hom.naturality] dsimp rw [hX'.hom_ext (hX'.to (op (F.obj (unop U)))) _] · cat_disch · cat_disch

The special case you have here you should be able to obtain easily from the general case.

Brian-Nugent · 2026-05-02T22:37:40Z

+/-- `sheafCompose` commutes with `pushforward` -/
+def sheafComposePushforwardComp :
+    sheafCompose (Opens.grothendieckTopology (Spec S))
+      (ModuleCat.restrictScalars (Spec.map φ).appTop.hom) ⋙
+    TopCat.Sheaf.pushforward _ (Spec.map φ).base ⋙
+    sheafCompose _ (ModuleCat.restrictScalars (Scheme.ΓSpecIso R).inv.hom) ≅
+    sheafCompose _ (ModuleCat.restrictScalars (Scheme.ΓSpecIso S).inv.hom) ⋙
+    TopCat.Sheaf.pushforward _ (Spec.map φ).base ⋙
+    sheafCompose _ (ModuleCat.restrictScalars φ.hom) := by
+  refine NatIso.ofComponents (fun M ↦ ObjectProperty.isoMk _ ?_) ?_
+  · refine NatIso.ofComponents (fun U ↦ ?_) ?_
+    · refine (ModuleCat.restrictScalarsComp'App _ _ _ ?_ _).symm ≪≫
+        (ModuleCat.restrictScalarsComp φ.hom ((Scheme.ΓSpecIso S).inv).hom).app _
+      rw [← CommRingCat.hom_comp, Scheme.ΓSpecIso_inv_naturality, CommRingCat.hom_comp]
+    · cat_disch
+  · cat_disch
+
+/-- `Scheme.Modules.pushforward` and `modulesSpecToSheaf` commute -/
+def pushforward_modulesSpecToSheaf_iso :
+    Scheme.Modules.pushforward (Spec.map φ) ⋙ modulesSpecToSheaf ≅
+    modulesSpecToSheaf ⋙ TopCat.Sheaf.pushforward (ModuleCat S) (Spec.map φ).base ⋙
+    sheafCompose _ (ModuleCat.restrictScalars φ.hom) :=
+  Functor.isoWhiskerRight (SheafOfModules.pushforwardCompForgetToSheafModuleCat
+    (Spec.map φ).toRingCatSheafHom _ _ _) (sheafCompose _ _) ≪≫
+  (Functor.isoWhiskerLeft (SheafOfModules.forgetToSheafModuleCat (Spec S).ringCatSheaf _
+    (initialOpOfTerminal isTerminalTop)) (sheafComposePushforwardComp φ))


I can make sheafComposePushforwardComp more general, but first I just want to make sure that this is a reasonable way of defining pushforward_modulesSpecToSheaf_iso

Brian-Nugent added 3 commits March 21, 2026 12:20

Commit

fc7d421

feat: Add IsLocalizing

22b2261

start cleanup

48e8689

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Mar 25, 2026

Remove Pushforward.lean

1e6244f

remove reflect iso instance

bec487b

github-actions 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 Mar 26, 2026

Brian-Nugent added 3 commits March 26, 2026 17:19

Moved instances

d2ec040

Moved Lemmas to IsLocalizedModule.Basic

fddbef3

Merge branch 'master' into pushforward-qc

ee4dc89

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 Mar 30, 2026

Brian-Nugent and others added 6 commits March 30, 2026 11:46

Added documentation

c031311

Merge branch 'pushforward-qc' of https://github.com/Brian-Nugent/math…

b07f1b2

…lib4 into pushforward-qc

add isIso_iff_isIso_basis

ce312d3

add TopCat.Sheaf.isIso_iff_isIso_basis

bdc64cc

[pre-commit.ci lite] apply automatic fixes

599da80

clean up Tilde.lean

3dfad3a

Brian-Nugent marked this pull request as ready for review March 30, 2026 22:14

Brian-Nugent requested review from chrisflav and erdOne March 30, 2026 22:14

Brian-Nugent added t-algebraic-geometry Algebraic geometry and removed new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! labels Mar 31, 2026

mathlib-triage Bot assigned adamtopaz Apr 1, 2026

joelriou reviewed Apr 1, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Module/LocalizedModule/Basic.lean Outdated

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 1, 2026

fix indentation

ba88ea7

Brian-Nugent removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 1, 2026

Merge branch 'master' into pushforward-qc

ba5d904

joelriou reviewed Apr 6, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicGeometry/Modules/Tilde.lean Outdated

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 6, 2026

Brian-Nugent and others added 2 commits April 6, 2026 11:08

Update Mathlib/AlgebraicGeometry/Modules/Tilde.lean

c81f038

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

Merge branch 'master' into pushforward-qc

37a4597

Brian-Nugent removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 6, 2026

chrisflav reviewed Apr 23, 2026

View reviewed changes

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 23, 2026

Brian-Nugent added 4 commits April 27, 2026 13:30

add IsLocalizedModule.restrictScalars_iff

edbeed1

Merge branch 'master' into pushforward-qc

1263fc6

move lemma

efbdf44

min_imports

e95533b

Brian-Nugent removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 28, 2026

chrisflav reviewed May 1, 2026

View reviewed changes

chrisflav added the awaiting-author A reviewer has asked the author a question or requested changes. label May 1, 2026

Brian-Nugent added 4 commits May 2, 2026 15:18

Fix definition of NatIso

e52350c

Move lemmas

66a9e30

-_root_

8bbe21c

Use Functor.IsCoverDense.iso_of_restrict_iso

fc89105

Brian-Nugent commented May 2, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicGeometry/Modules/Tilde.lean Outdated

Add documentation

8797ae0

Brian-Nugent commented May 2, 2026

View reviewed changes

Brian-Nugent removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 2, 2026

Conversation

Brian-Nugent commented Mar 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Mar 25, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Mar 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2d59066e04

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Brian-Nugent commented Mar 25, 2026 •

edited

Loading

github-actions Bot commented Mar 25, 2026 •

edited

Loading