feat(AlgebraicGeometry): The pushforward of a quasi-coherent sheaf between affines is quasi-coherent (#37189)

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.

Co-authored-by: Brian-Nugent <bnugent@uw.edu>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: Brian-Nugent

Mathlib/Algebra/Category/ModuleCat/Localization.lean

@@ -101,4 +101,12 @@ instance [Small.{v} R] (S : Submonoid R) :
   have := ((Functor.exact_tfae _).out 1 3).mp (ModuleCat.localizedModuleFunctor_map_exact S)
   exact this.2
 
+lemma isIso_of_isLocalizedModule_comp {S : Submonoid R} {M₁ M₂ M₃ : ModuleCat R} {f₁ : M₁ ⟶ M₂}
+    {f₂ : M₂ ⟶ M₃} (h₁ : IsLocalizedModule S f₁.hom) (h₂ : IsLocalizedModule S (f₁ ≫ f₂).hom) :
+    IsIso f₂ := by
+  have : Function.Bijective f₂.hom := by
+    rw [← IsLocalizedModule.linearEquiv_of_isLocalizedModule_comp S f₁.hom f₂.hom]
+    exact (IsLocalizedModule.linearEquiv ..).bijective
+  simpa [ConcreteCategory.isIso_iff_bijective]
+
 end ModuleCat

Mathlib/Algebra/Category/ModuleCat/Sheaf.lean

@@ -103,6 +103,20 @@ noncomputable def forgetToSheafModuleCat
       (forget₂ (ModuleCat.{w} (R.1.obj X)) AddCommGrpCat.{w}) M.isSheaf⟩
   map f := { hom := (PresheafOfModules.forgetToPresheafModuleCat X hX).map f.1 }
 
+set_option backward.defeqAttrib.useBackward true in
+/-- Isomorphism on `forgetToSheafModuleCat` when given isomorphic initial objects. -/
+noncomputable def forgetToSheafModuleCatOfIso (X Y : Cᵒᵖ) (hX : Limits.IsInitial X)
+    (hY : Limits.IsInitial Y) (φ : X ≅ Y) :
+    forgetToSheafModuleCat R X hX ≅ forgetToSheafModuleCat R Y hY ⋙
+      sheafCompose J (ModuleCat.restrictScalars (R.obj.map φ.hom).hom) := by
+  refine NatIso.ofComponents (fun M ↦ ObjectProperty.isoMk _ ?_) ?_
+  · refine NatIso.ofComponents (fun U ↦ ?_) ?_
+    · dsimp [PresheafOfModules.forgetToPresheafModuleCatObjObj]
+      refine ModuleCat.restrictScalarsComp'App _ _ _ ?_ _
+      simpa using congr((R.obj.map $(hX.hom_ext (hX.to U) (φ.hom ≫ hY.to U))).hom)
+    cat_disch
+  cat_disch
+
 /-- The canonical isomorphism between
 `SheafOfModules.toSheaf R ⋙ sheafToPresheaf J AddCommGrpCat.{v}`
 and `SheafOfModules.forget R ⋙ PresheafOfModules.toPresheaf R.val`. -/

Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean

@@ -330,4 +330,23 @@ lemma pushforwardPushforwardEquivalence_counit_app_val_app (M U x) :
 
 end Equivalence
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+/-- Pushforward commutes with `SheafOfModules.forgetToSheafModuleCat` -/
+noncomputable def pushforwardCompForgetToSheafModuleCat
+    (X : Cᵒᵖ) (hX : Limits.IsInitial X) (hX' : Limits.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 (Opposite.op (F.obj (Opposite.unop U)))) _]
+    · cat_disch
+  · cat_disch
+
 end SheafOfModules

Mathlib/Algebra/Module/LocalizedModule/Basic.lean

@@ -569,6 +569,22 @@ instance IsLocalizedModule.of_linearEquiv_right (e : M'' ≃ₗ[R] M) [hf : IsLo
     exact ⟨c, by simpa only [Submonoid.smul_def, map_smul, e.symm_apply_apply]
       using congr(e.symm $hc)⟩
 
+lemma IsLocalizedModule.comp_iff_of_bijective_left {f : M →ₗ[R] M'} (e : M' →ₗ[R] M'')
+    (he : Function.Bijective e) :
+    IsLocalizedModule S (e ∘ₗ f) ↔ IsLocalizedModule S f := by
+  refine ⟨fun h ↦ ?_, fun h ↦ .of_linearEquiv _ _ (.ofBijective _ he)⟩
+  have : (LinearEquiv.ofBijective _ he).symm.toLinearMap ∘ₗ e ∘ₗ f = f := by ext; simp
+  rw [← this]
+  exact .of_linearEquiv _ _ _
+
+lemma IsLocalizedModule.comp_iff_of_bijective_right (e : M →ₗ[R] M') {f : M' →ₗ[R] M''}
+    (he : Function.Bijective e) :
+    IsLocalizedModule S (f ∘ₗ e) ↔ IsLocalizedModule S f := by
+  refine ⟨fun h ↦ ?_, fun h ↦ .of_linearEquiv_right _ _ (.ofBijective _ he)⟩
+  have : (f ∘ₗ e) ∘ₗ (LinearEquiv.ofBijective _ he).symm.toLinearMap = f := by ext; simp
+  rw [← this]
+  exact .of_linearEquiv_right _ _ _
+
 variable (M) in
 lemma isLocalizedModule_id (R') [CommSemiring R'] [Algebra R R'] [IsLocalization S R'] [Module R' M]
     [IsScalarTower R R' M] : IsLocalizedModule S (.id : M →ₗ[R] M) where
@@ -699,6 +715,30 @@ instance localizedModuleIsLocalizedModule :
         ← Submonoid.smul_def, LocalizedModule.mk_cancel t]
   exists_of_eq eq1 := by simpa only [eq_comm, one_smul] using LocalizedModule.mk_eq.mp eq1
 
+lemma IsLocalizedModule.restrictScalars (S : Submonoid R) [Module A M]
+    {N : Type*} [AddCommMonoid N] [Module R N] [Module A N]
+    [IsScalarTower R A M] [IsScalarTower R A N]
+    (f : M →ₗ[A] N) [h : IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f] :
+    IsLocalizedModule S (f.restrictScalars R) where
+  map_units s := by
+    have := h.1 ⟨algebraMap R A s, Algebra.mem_algebraMapSubmonoid_of_mem s⟩
+    simp only [← IsScalarTower.algebraMap_apply, Module.End.isUnit_iff] at this ⊢
+    exact this
+  surj y := by
+    obtain ⟨⟨x, ⟨_, ⟨r, ⟨hr₁, rfl⟩⟩⟩⟩, hx⟩ := h.2 y
+    exact ⟨⟨x, ⟨r, hr₁⟩⟩, by simpa [Submonoid.smul_def] using hx⟩
+  exists_of_eq {x₁ x₂} e := by
+    obtain ⟨⟨_, ⟨r, ⟨hr, rfl⟩⟩⟩, hc⟩ := h.3 e
+    exact ⟨⟨r, hr⟩, by simpa [Submonoid.smul_def] using hc⟩
+
+lemma IsLocalizedModule.restrictScalars_powers [Module A M]
+    {N : Type*} [AddCommMonoid N] [Module R N] [Module A N]
+    [IsScalarTower R A M] [IsScalarTower R A N]
+    (r : R) (f : M →ₗ[A] N) [h : IsLocalizedModule (.powers (algebraMap R A r)) f] :
+    IsLocalizedModule (.powers r) (f.restrictScalars R) := by
+  rw [← Algebra.algebraMapSubmonoid_powers] at h
+  exact IsLocalizedModule.restrictScalars _ f
+
 lemma IsLocalizedModule.of_restrictScalars (S : Submonoid R)
     {N : Type*} [AddCommMonoid N] [Module R N] [Module A M] [Module A N]
     [IsScalarTower R A M] [IsScalarTower R A N]
@@ -716,6 +756,13 @@ lemma IsLocalizedModule.of_restrictScalars (S : Submonoid R)
     obtain ⟨c, hc⟩ := IsLocalizedModule.exists_of_eq (S := S) (f := f.restrictScalars R) e
     refine ⟨⟨_, c, c.2, rfl⟩, by simpa [Submonoid.smul_def]⟩
 
+lemma IsLocalizedModule.restrictScalars_iff (S : Submonoid R)
+    {N : Type*} [AddCommMonoid N] [Module R N] [Module A M] [Module A N]
+    [IsScalarTower R A M] [IsScalarTower R A N] (f : M →ₗ[A] N) :
+    IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f ↔
+    IsLocalizedModule S (f.restrictScalars R) :=
+  ⟨fun _ => restrictScalars _ _, fun _ => of_restrictScalars _ _⟩
+
 lemma IsLocalizedModule.of_exists_mul_mem {N : Type*} [AddCommMonoid N] [Module R N]
     (S T : Submonoid R) (h : S ≤ T) (h' : ∀ x : T, ∃ m : R, m * x ∈ S)
     (f : M →ₗ[R] N) [IsLocalizedModule S f] :
@@ -933,6 +980,12 @@ lemma linearEquiv_symm_apply [IsLocalizedModule S g] (x : M) :
     (linearEquiv S f g).symm (g x) = f x := by
   simp [linearEquiv]
 
+lemma linearEquiv_of_isLocalizedModule_comp (g : M' →ₗ[R] M'') [IsLocalizedModule S (g ∘ₗ f)] :
+    linearEquiv S f (g ∘ₗ f) = g  := by
+  refine ext S f (IsLocalizedModule.map_units (g ∘ₗ f)) ?_
+  ext
+  simp
+
 variable {S}
 
 include f in

Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

@@ -456,4 +456,21 @@ lemma germ_restrictStalkNatIso_inv_app (x : X) (M : Y.Modules) (hxU : x ∈ U) :
 
 end Restriction
 
+/-- `sheafCompose` commutes with `pushforward` -/
+noncomputable def sheafComposePushforwardComp {R S : CommRingCat.{u}} (φ : R ⟶ S) :
+    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
+
 end AlgebraicGeometry.Scheme.Modules

Mathlib/AlgebraicGeometry/Modules/Tilde.lean

@@ -2,16 +2,14 @@
 Copyright (c) 2024 Weihong Xu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Johan Commelin, Amelia Livingston, Sophie Morel, Jujian Zhang, Weihong Xu,
-  Andrew Yang
+  Andrew Yang, Brian Nugent
 -/
 module
 
-public import Mathlib.Algebra.Module.LocalizedModule.Basic
+public import Mathlib.Algebra.Category.ModuleCat.Localization
+public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
 public import Mathlib.AlgebraicGeometry.AffineScheme
 public import Mathlib.AlgebraicGeometry.Modules.Sheaf
-public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
-public import Mathlib.Algebra.Category.ModuleCat.FilteredColimits
-public import Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures
 
 /-!
 
@@ -43,7 +41,7 @@ def modulesSpecToSheaf :
     (Spec R).Modules ⥤ TopCat.Sheaf (ModuleCat R) (Spec R) :=
   SheafOfModules.forgetToSheafModuleCat (Spec R).ringCatSheaf (.op ⊤)
     (Limits.initialOpOfTerminal Limits.isTerminalTop) ⋙
-  sheafCompose _ (ModuleCat.restrictScalars (StructureSheaf.globalSectionsIso R).hom.hom)
+  sheafCompose _ (ModuleCat.restrictScalars (Scheme.ΓSpecIso R).inv.hom)
 
 /-- The global section functor for `𝒪_{Spec R}` modules -/
 noncomputable
@@ -81,6 +79,10 @@ def SpecModulesToSheafFullyFaithful : (modulesSpecToSheaf (R := R)).FullyFaithfu
   map_preimage f := rfl
   preimage_map f := rfl
 
+instance : (modulesSpecToSheaf (R := R)).Faithful := SpecModulesToSheafFullyFaithful.faithful
+
+instance : (modulesSpecToSheaf (R := R)).Full := SpecModulesToSheafFullyFaithful.full
+
 /--
 `M^~` as a sheaf of `𝒪_{Spec R}`-modules
 -/
@@ -410,6 +412,96 @@ lemma isIso_fromTildeΓ_of_presentation (M : (Spec R).Modules) (P : M.Presentati
   exact ⟨cokernel g, ⟨PreservesCokernel.iso (tilde.functor R) g ≪≫ iso ≪≫
     IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) P.isColimit⟩⟩
 
+section IsLocalizing
+
+variable (M : (Spec R).Modules) (f : R) {S : CommRingCat.{u}} (φ : R ⟶ S)
+
+open TopologicalSpace
+
+/-- A sheaf `M` of `R-modules` is localizing if for all `f` in `R`, the restriction map
+from `M(⊤)` to `M(D(f))` is localization with respect to `f`. -/
+abbrev IsLocalizing (M : TopCat.Sheaf (ModuleCat R) (Spec R)) : Prop :=
+  ∀ f : R, IsLocalizedModule (.powers f) (M.obj.map (basicOpen f).leTop.op).hom
+
+theorem isLocalizing_of_iso {M N : TopCat.Sheaf (ModuleCat R) (Spec R)} (φ : M ≅ N)
+    (hM : IsLocalizing M) :
+    IsLocalizing N := by
+  intro f
+  rw [← IsLocalizedModule.comp_iff_of_bijective_left _ _ <|
+    ConcreteCategory.bijective_of_isIso (φ.inv.hom.app (op (basicOpen f))), ← ModuleCat.hom_comp,
+    φ.inv.hom.naturality (basicOpen f).leTop.op, ModuleCat.hom_comp,
+    IsLocalizedModule.comp_iff_of_bijective_right _ _ <| ConcreteCategory.bijective_of_isIso _]
+  exact hM f
+
+theorem isLocalizing_iff_of_iso {M N : TopCat.Sheaf (ModuleCat R) (Spec R)} (φ : M ≅ N) :
+    IsLocalizing M ↔ IsLocalizing N :=
+  ⟨fun h => isLocalizing_of_iso φ h, fun h => isLocalizing_of_iso φ.symm h⟩
+
+theorem isLocalizing_of_isIso_app_top {M N : TopCat.Sheaf (ModuleCat.{u} R) (Spec R)} {φ : M ⟶ N}
+    (h : IsIso (φ.hom.app (op ⊤))) (hM : IsLocalizing M) (hN : IsLocalizing N) :
+    IsIso φ := by
+  refine TopCat.Sheaf.isIso_iff_isIso_basis (φ := φ) isBasis_basic_opens (fun f => ?_)
+  refine ModuleCat.isIso_of_isLocalizedModule_comp (hM f) ?_
+  rw [φ.hom.naturality]
+  exact IsLocalizedModule.of_linearEquiv_right _ _ (asIso (φ.hom.app (op ⊤))).toLinearEquiv
+
+theorem isLocalizing_tilde (M : ModuleCat R) :
+    IsLocalizing (modulesSpecToSheaf.obj (tilde M)) := by
+  intro f
+  -- We can't rewrite with `tilde.toOpen_res` below, because of def-eq abuse between
+  -- `Spec R` and `PrimeSpectrum R`.
+  have heq : tilde.toOpen M ⊤ ≫ (modulesSpecToSheaf.obj (tilde M)).obj.map (basicOpen f).leTop.op =
+      tilde.toOpen M (basicOpen f) :=
+    tilde.toOpen_res _ _ _ _
+  rw [← IsLocalizedModule.comp_iff_of_bijective_right _ _ <|
+    ConcreteCategory.bijective_of_isIso (tilde.toOpen M ⊤), ← ModuleCat.hom_comp, heq]
+  infer_instance
+
+/-- An `𝓞_Spec R` module `M` is isomorphic to `Γ(M)^~` if and only if it is localizing
+as a sheaf of `R` modules -/
+theorem isIso_fromTildeΓ_iff_isLocalizing (M : (Spec R).Modules) :
+    IsIso M.fromTildeΓ ↔ IsLocalizing (modulesSpecToSheaf.obj M) := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · rw [← isLocalizing_iff_of_iso (modulesSpecToSheaf.mapIso (asIso M.fromTildeΓ))]
+    exact isLocalizing_tilde _
+  · rw [← isIso_iff_of_reflects_iso _ modulesSpecToSheaf]
+    refine isLocalizing_of_isIso_app_top ?_ (isLocalizing_tilde _) h
+    rw [← isIso_comp_left_iff (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) ⊤),
+      Scheme.Modules.toOpen_fromTildeΓ_app]
+    simpa using IsIso.id _
+
+/-- `Scheme.Modules.pushforward` and `modulesSpecToSheaf` commute -/
+def pushforwardCompModulesSpecToSheafIso :
+    Scheme.Modules.pushforward (Spec.map φ) ⋙ modulesSpecToSheaf ≅
+      modulesSpecToSheaf ⋙ TopCat.Sheaf.pushforward (ModuleCat S) (Spec.map φ).base ⋙
+      sheafCompose _ (ModuleCat.restrictScalars φ.hom) :=
+  (Functor.associator _ _ _).symm ≪≫
+    Functor.isoWhiskerRight (SheafOfModules.pushforwardCompForgetToSheafModuleCat _ _ _
+    (initialOpOfTerminal isTerminalTop)) _ ≪≫ Functor.associator _ _ _ ≪≫
+    (Functor.isoWhiskerLeft _ (Functor.associator _ _ _)) ≪≫
+    Functor.isoWhiskerLeft _ (Scheme.Modules.sheafComposePushforwardComp φ) ≪≫
+    (Functor.associator _ _ _).symm
+
+open scoped ModuleCat.Algebra in
+theorem isLocalizing_pushforward_of_isLocalizing {M : (Spec S).Modules}
+    (h : IsLocalizing (modulesSpecToSheaf.obj M)) :
+    IsLocalizing (modulesSpecToSheaf.obj ((Scheme.Modules.pushforward (Spec.map φ)).obj M)) := by
+  rw [← Functor.comp_obj,
+  isLocalizing_iff_of_iso ((pushforwardCompModulesSpecToSheafIso φ).app M)]
+  have : CommRing ((Spec S).ringCatSheaf.obj.obj ((Opens.map (Spec.map φ).base).op.obj (op ⊤))) :=
+    inferInstanceAs (CommRing Γ(Spec S, ⊤))
+  algebraize [φ.hom]
+  exact fun f => IsLocalizedModule.restrictScalars_powers f _ (h := h (φ f))
+
+/- TODO: Once `IsIso M.fromTildeΓ` is shown to be equivalent to `M` being quasicoherent, use
+this to show that quasicoherent sheaves pushforward to quasicoherent sheaves for affine morphisms -/
+theorem isIso_fromTildeΓ_pushforward (M : (Spec S).Modules) [h : IsIso M.fromTildeΓ] :
+    IsIso ((Scheme.Modules.pushforward (Spec.map φ)).obj M).fromTildeΓ := by
+  simp_all only [isIso_fromTildeΓ_iff_isLocalizing]
+  exact isLocalizing_pushforward_of_isLocalizing φ h
+
+end IsLocalizing
+
 end IsQuasicoherent
 
 end AlgebraicGeometry

Mathlib/Topology/Sheaves/SheafCondition/Sites.lean

@@ -246,6 +246,15 @@ theorem hom_ext (h : Opens.IsBasis (Set.range B))
   ext i
   exact he i.unop
 
+theorem isIso_iff_isIso_basis {F G : Sheaf C X} (h : Opens.IsBasis (Set.range B))
+    {φ : F ⟶ G} (hi : ∀ i, IsIso (φ.hom.app (op (B i)))) :
+    IsIso φ := by
+  have : (inducedFunctor B).IsCoverDense (Opens.grothendieckTopology X) :=
+    Opens.coverDense_inducedFunctor h
+  refine Functor.IsCoverDense.iso_of_restrict_iso (G := inducedFunctor B) _ ?_
+  rw [NatTrans.isIso_iff_isIso_app]
+  exact fun _ ↦ hi _
+
 end TopCat.Sheaf
 
 namespace TopologicalSpace.Opens