feat(AlgebraicGeometry): essential image of tilde is quasi-coherent modules (#40052)

We show that for a quasi-coherent module `M` over `Spec R`, the counit `M.fromTildeΓ` is an isomorphism, i.e., `M` is isomorphic to the tilde of the global sections of `M`.

Co-authored-by: Andrew Yang <the.erd.one@gmail.com>
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: chrisflav

Mathlib/AlgebraicGeometry/Modules/Tilde.lean

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Category.ModuleCat.Localization
 public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
 public import Mathlib.Algebra.Module.LocalizedModule.Away
 public import Mathlib.AlgebraicGeometry.Modules.Sheaf
+public import Mathlib.Data.Fintype.Order
 
 /-!
 
@@ -595,6 +596,265 @@ lemma Scheme.Modules.exists_affineOpenCover_presentation {X : Scheme.{u}} (M : X
   exact SheafOfModules.Presentation.ofIsIso.{u, u, u} ((restrictFunctorComp _ _).app M).inv <|
     (presentationRestrict (hU' i).isoSpec.inv (pres i))
 
+namespace QuasicoherentTilde
+
+variable (M : (Spec R).Modules)
+
+/-- Auxiliary structure used in the proof of `Scheme.Modules.isIso_fromTildeΓ_of_isQuasicoherent`.
+These are conditions d1) and d2) from [Theoreme 1.4.1, grothendieck-1971]. -/
+-- TODO: Generalise this to a general scheme, replacing `f : R` by sections over a suitable set.
+private structure Aux (V : (Spec R).Opens) where
+  existence (f : R) (hf : basicOpen f ≤ V) (s : Γ(M, basicOpen f)) :
+    ∃ (n : ℕ) (t : Γ(M, V)), M.presheaf.map (homOfLE hf).op t = f ^ n • s
+  uniqueness (f : R) (hf : basicOpen f ≤ V) (t : Γ(M, V)) :
+    M.presheaf.map (.op <| homOfLE hf) t = (0 : Γ(M, basicOpen f)) →
+    ∃ (n : ℕ), f ^ n • t = 0
+
+set_option backward.isDefEq.respectTransparency false in
+private lemma Aux.of_le {M : (Spec R).Modules} {V : (Spec R).Opens} (g : R) (hg : basicOpen g ≤ V)
+    (hV : Aux M V) :
+    Aux M (basicOpen g) where
+  existence f hfg s := by
+    obtain ⟨n, t, ht⟩ := hV.existence f (le_trans hfg hg) s
+    use n, M.presheaf.map (homOfLE hg).op t
+    simp [← M.presheaf.map_comp_apply, ← op_comp, homOfLE_comp, ht]
+  uniqueness f hfg t ht := by
+    obtain ⟨n, t', ht'⟩ := hV.existence g hg t
+    obtain ⟨m, hm⟩ := hV.uniqueness _ (le_trans hfg hg) t' <| by
+      rw [← homOfLE_comp hfg hg, op_comp, M.presheaf.map_comp_apply, ht', M.map_smul_Spec, ht]
+      simp
+    refine ⟨m, ((M.isSMulRegular_of_le_basicOpen le_rfl).pow n).right_eq_zero_of_smul ?_⟩
+    simp [smul_comm, ← ht', ← M.map_smul_Spec, hm]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- This is the key computation for the proof of
+`Scheme.Modules.isQuasicoherent_iff_isIso_fromTildeΓ`.
+ [Lemme 1.4.1.1][grothendieck-1971] -/
+private lemma Aux.of_eq_iSup_basicOpen {M : (Spec R).Modules} (V : (Spec R).Opens)
+    {ι : Type*} [Finite ι] (g : ι → R) (hg : V = ⨆ i, basicOpen (g i))
+    (h₁ : ∀ (i : ι), Aux M (basicOpen (g i))) :
+    Aux M V := by
+  have h₂ (i j : ι) : Aux M (basicOpen (g i * g j)) :=
+    .of_le _ (basicOpen_mul_le_left _ _) (h₁ i)
+  have hgle (i : ι) : basicOpen (g i) ≤ V := by rw [hg]; exact le_iSup_of_le _ le_rfl
+  have hug (i : ι) (m : ℕ) :
+      IsUnit (algebraMap R (Module.End R Γ(M, basicOpen (g i))) (g i ^ m)) := by
+    rw [map_pow]
+    exact (Scheme.Modules.isUnit_algebraMap_end_of_le_basicOpen (g i) le_rfl).pow m
+  -- We show existence and uniqueness separately.
+  refine ⟨fun f hf s ↦ ?_, fun f hf t hs ↦ ?_⟩
+  · have hfgi (i : ι) : basicOpen (f * g i) ≤ basicOpen (g i) := basicOpen_mul_le_right f (g i)
+    let s' (i : ι) : Γ(M, basicOpen (f * g i)) :=
+      M.presheaf.map (homOfLE <| basicOpen_mul_le_left f (g i)).op s
+    /- By `h₁`, up to a factor of `f ^ N`, the restrictions of `s` to `D(f) ∩ D(gᵢ)` lift
+    to sections `tᵢ` over `D(gᵢ)`. -/
+    obtain ⟨N, t, ht⟩ : ∃ (N : ℕ) (t : ∀ i, Γ(M, basicOpen (g i))),
+        ∀ i, f ^ N • s' i = M.presheaf.map (homOfLE (basicOpen_mul_le_right f (g i))).op (t i) := by
+      have (i : ι) : ∃ (n : ℕ) (t : Γ(M, basicOpen (g i))),
+          f ^ n • s' i = M.presheaf.map (homOfLE (hfgi i)).op t := by
+        obtain ⟨n, t', ht'⟩ := (h₁ i).existence (f * g i) (hfgi i) (s' i)
+        rw [mul_pow, mul_smul, smul_comm] at ht'
+        obtain ⟨ψ, hψ⟩ := IsUnit.exists_right_inv (hug i n)
+        use n, ψ t'
+        apply (M.isSMulRegular_of_le_basicOpen (basicOpen_mul_le_right f (g i))).pow n
+        dsimp
+        rw [← ht', ← Scheme.Modules.map_smul_Spec]
+        congr 1
+        exact congr($hψ t').symm
+      choose n t' ht' using this
+      have (i : ι) : n i ≤ ⨆ i, n i := le_ciSup (Finite.bddAbove_range _) _
+      have hN (i : ι) : ⨆ i, n i = ((⨆ i, n i) - n i) + n i := by grind
+      refine ⟨⨆ i, n i, fun i ↦ f ^ ((⨆ i, n i) - n i) • t' i, fun i ↦ ?_⟩
+      conv_lhs => rw [hN i]
+      rw [pow_add, mul_smul, ht', M.map_smul_Spec]
+    /- By `h₂`, up to a factor of `f ^ K`, the restrictions of `tᵢ` and `tⱼ` to
+    to `D(gᵢ) ∩ D(gⱼ)` agree. -/
+    obtain ⟨K, hK⟩ : ∃ (K : ℕ), ∀ (i j : ι),
+        M.presheaf.map (homOfLE (basicOpen_mul_le_left (g i) (g j))).op (f ^ K • t i) =
+          M.presheaf.map (homOfLE (basicOpen_mul_le_right (g i) (g j))).op (f ^ K • t j) := by
+      have (i j : ι) : ∃ (m : ℕ),
+          M.presheaf.map (homOfLE (basicOpen_mul_le_left (g i) (g j))).op (f ^ m • t i) =
+            M.presheaf.map (homOfLE (basicOpen_mul_le_right (g i) (g j))).op (f ^ m • t j) := by
+        have := (h₂ i j).uniqueness (f * (g i * g j)) (basicOpen_mul_le_right _ _)
+          (M.presheaf.map (homOfLE (basicOpen_mul_le_left (g i) (g j))).op (t i) -
+            M.presheaf.map (homOfLE (basicOpen_mul_le_right (g i) (g j))).op (t j)) ?_
+        · obtain ⟨m, hm⟩ := this
+          use m
+          apply (M.isSMulRegular_of_le_basicOpen le_rfl).pow m
+          simpa [M.map_smul_Spec _ (f ^ m), ← mul_smul, ← mul_smul, ← mul_pow, ← mul_comm f,
+            smul_sub, sub_eq_zero] using hm
+        · have hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i) := by
+            rw [← mul_assoc]
+            exact basicOpen_mul_le_left _ _
+          have hfgigj : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g j) := by
+            rw [mul_comm (g i) (g j), ← mul_assoc]
+            exact basicOpen_mul_le_left _ _
+          rw [map_sub, ← M.presheaf.map_comp_apply, ← op_comp, ← M.presheaf.map_comp_apply,
+            ← op_comp, homOfLE_comp, homOfLE_comp, ← homOfLE_comp hfgigi (hfgi i),
+            ← homOfLE_comp hfgigj (hfgi j), op_comp, M.presheaf.map_comp_apply, ← ht i,
+            M.map_smul_Spec, ← M.presheaf.map_comp_apply, ← op_comp, homOfLE_comp, op_comp,
+            M.presheaf.map_comp_apply, ← ht j, M.map_smul_Spec, ← M.presheaf.map_comp_apply,
+            ← op_comp, homOfLE_comp]
+          simp
+      choose m hm using this
+      let K := ⨆ i, ⨆ j, m i j
+      refine ⟨K, fun i j ↦ ?_⟩
+      have : m i j ≤ K :=
+        le_ciSup_of_le (Finite.bddAbove_range _) i (le_ciSup (Finite.bddAbove_range _) _)
+      have : K = (K - m i j) + m i j := by lia
+      rw [this, pow_add, mul_smul, mul_smul, M.map_smul_Spec, M.map_smul_Spec _ (f ^ (K - m i j)),
+        hm i j]
+    -- So up to a factor of `f ^ (N + K)`, the `tᵢ` glue.
+    refine ⟨N + K, ?_⟩
+    have := TopCat.Sheaf.existsUnique_gluing' ⟨_, M.isSheaf⟩ (fun i ↦ basicOpen (g i)) V
+      (fun i ↦ homOfLE (by rw [hg]; exact le_iSup_of_le _ le_rfl)) (by simp [hg])
+      (fun i ↦ f ^ K • t i) ?_
+    · obtain ⟨a, ha, -⟩ := this
+      use a
+      refine TopCat.Sheaf.eq_of_locally_eq' ⟨_, M.isSheaf⟩ (fun i ↦ basicOpen (f * g i)) _
+          (fun i ↦ homOfLE (basicOpen_mul_le_left f (g i))) ?_ _ _ ?_
+      · rw [left_eq_inf.mpr hf, hg, inf_iSup_eq]
+        simp_rw [basicOpen_mul]
+        exact le_rfl
+      · intro i
+        rw [← M.presheaf.map_comp_apply, ← op_comp, homOfLE_comp,
+          ← homOfLE_comp (basicOpen_mul_le_right _ _) (hgle i), op_comp, M.presheaf.map_comp_apply,
+          M.map_smul_Spec, ha, M.map_smul_Spec, pow_add, mul_smul, smul_comm, ht i]
+    · intro i j
+      have : Function.Injective (M.presheaf.map (eqToHom <| (basicOpen_mul (g i) (g j))).op) :=
+        ConcreteCategory.injective_of_mono_of_preservesPullback _
+      apply this
+      dsimp [Opens.infLELeft, Opens.infLERight]
+      simp_rw [← M.presheaf.map_comp_apply, ← op_comp, eqToHom_comp_homOfLE]
+      exact hK i j
+  · have (i : ι) : ∃ (n : ℕ), M.presheaf.map (homOfLE (hgle i)).op (f ^ n • t) = 0 := by
+      have := (h₁ i).uniqueness (f * g i) (basicOpen_mul_le_right f (g i))
+        (M.presheaf.map (homOfLE (hgle i)).op t) ?_
+      · obtain ⟨n, hn⟩ := this
+        use n
+        rw [mul_pow, mul_comm, mul_smul, ← Scheme.Modules.map_smul_Spec] at hn
+        exact ((M.isSMulRegular_of_le_basicOpen le_rfl).pow n).right_eq_zero_of_smul hn
+      · rw [← M.presheaf.map_comp_apply, ← op_comp, homOfLE_comp,
+          ← homOfLE_comp ((basicOpen_mul_le_left f (g i))) hf, op_comp, M.presheaf.map_comp_apply]
+        simp [hs]
+    choose n hn using this
+    use ⨆ i, n i
+    apply TopCat.Sheaf.eq_of_locally_eq' ⟨_, M.isSheaf⟩ (fun i ↦ basicOpen (g i)) _
+      (fun i ↦ homOfLE (by rw [hg]; exact le_iSup_of_le _ le_rfl))
+    · simp [hg]
+    · intro i
+      have : n i ≤ ⨆ i, n i := le_ciSup (Finite.bddAbove_range _) _
+      have : ⨆ i, n i = ((⨆ i, n i) - n i) + n i := by lia
+      rw [this, pow_add, mul_smul, Scheme.Modules.map_smul_Spec, hn i]
+      simp
+
+private lemma isLocalizing_iff_aux (M : (Spec R).Modules) :
+    IsLocalizing (modulesSpecToSheaf.obj M) ↔ Aux M ⊤ := by
+  let φ (f : R) := ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op).hom
+  refine ⟨fun h ↦ ?_, fun h f ↦ IsLocalizedModule.Away.mk_of_addCommGroup ?_ ?_ ?_⟩
+  · have hf (f : R) : IsLocalizedModule.Away f (φ f) := h f
+    refine ⟨fun f hle s ↦ ?_, fun f hle s hs ↦ ?_⟩
+    · obtain ⟨n, y, hy⟩ := (hf f).surj _ _ s
+      use n, y, hy.symm
+    · obtain ⟨⟨_, n, rfl⟩, hn⟩ := (IsLocalizedModule.eq_zero_iff (.powers f) (φ f)).mp hs
+      use n, hn
+  · exact Scheme.Modules.isUnit_algebraMap_end_of_le_basicOpen f le_rfl
+  · intro x
+    obtain ⟨n, t, ht⟩ := h.existence _ _ x
+    use n, t, ht.symm
+  · intro x hx
+    obtain ⟨n, hn⟩ := h.uniqueness _ _ _ hx
+    use n, hn
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+private lemma aux_basicOpen_of_aux_restrict (M : (Spec R).Modules) (g : R)
+    (h : Aux (M.restrict <|
+        Spec.map <| CommRingCat.ofHom <| algebraMap R <| Localization.Away g) ⊤) :
+      Aux M (basicOpen g) := by
+  let a : R ⟶ CommRingCat.of (Localization.Away g) :=
+    CommRingCat.ofHom <| algebraMap R _
+  set ψ : Spec (.of <| Localization.Away g) ⟶ Spec (.of R) := Spec.map a
+  set M' : (Spec (.of <| Localization.Away g)).Modules := M.restrict ψ
+  have heq (f : R) (hf : basicOpen f ≤ basicOpen g) :
+      basicOpen f = ψ ''ᵁ basicOpen (a f) := by
+    rw [← SpecMap_preimage_basicOpen, Scheme.Hom.image_preimage_eq_opensRange_inf]
+    simp [a, ψ, hf]
+  let iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
+    M.restrictAppIso _ _ ≪≫ M.presheaf.mapIso (eqToIso <| by simp [ψ, a]).op
+  let e (f : R) (hf : basicOpen f ≤ basicOpen g) : Γ(M', basicOpen (a f)) ≅ Γ(M, basicOpen f) :=
+    M.restrictAppIso ψ (basicOpen (a f)) ≪≫ M.presheaf.mapIso (eqToIso <| heq f hf).op
+  refine ⟨fun f hf s ↦ ?_, fun f hf t ht ↦ ?_⟩
+  · obtain ⟨n, t, ht⟩ := h.existence (a f) le_top ((e _ hf).inv s)
+    use n, iso.hom t
+    have := congr((e _ hf).hom $ht)
+    dsimp [M'] at this
+    rw [← ConcreteCategory.comp_apply] at this
+    simp only [homOfLE_leOfHom, Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, eqToIso.hom,
+      eqToHom_op, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, eqToIso.inv, e, iso] at this ⊢
+    simp only [homOfLE_leOfHom, Scheme.Modules.map_restrictAppIso_hom_assoc, AddCommGrpCat.hom_comp,
+      AddMonoidHom.coe_comp, Function.comp_apply, ← map_pow, ψ] at this
+    rw [Scheme.Modules.restrictAppIso_smul_Spec] at this
+    simpa [← Functor.map_comp_apply, eqToHom_comp_homOfLE_op, homOfLE_op_comp_eqToHom] using this
+  · obtain ⟨n, hn⟩ := h.uniqueness (a f) le_top (iso.inv t) <| by
+      simpa [M', iso, ← M.presheaf.map_comp_apply, homOfLE_op_comp_eqToHom, e] using
+        congr((e _ hf).inv $ht)
+    use n
+    have := congr(iso.hom $hn)
+    dsimp [iso, ψ] at this
+    rw [eqToHom_op, map_zero, ← map_pow, Scheme.Modules.restrictAppIso_smul_Spec,
+      M.map_smul_Spec, Iso.inv_hom_id_apply] at this
+    simpa using this
+
+end QuasicoherentTilde
+
+open QuasicoherentTilde in
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+/-- If `M` is a quasi-coherent `𝒪_{Spec R}` module, it is isomorphic to `Γ(M)^~`. -/
+instance Scheme.Modules.isIso_fromTildeΓ_of_isQuasicoherent (M : (Spec R).Modules)
+    [M.IsQuasicoherent] : IsIso M.fromTildeΓ := by
+  rw [isIso_fromTildeΓ_iff_isLocalizing, isLocalizing_iff_aux]
+  obtain ⟨ι, U, pres, hU, hU'⟩ := M.exists_isOpenCover_presentation
+  obtain ⟨s, hs⟩ := hU.exists_finite_of_compactSpace
+  choose κ hκ a ha using fun i : s ↦
+    PrimeSpectrum.isBasis_basic_opens.exists_iSup_eq_of_isCompact (U i) (hU' i).isCompact
+  refine Aux.of_eq_iSup_basicOpen _ (fun i : Sigma κ ↦ a _ i.2) ?_ ?_
+  · rw [IsOpenCover] at hs
+    rw [eq_comm, iSup_sigma, ← hs]
+    exact iSup_congr fun i ↦ (ha i).symm
+  · intro i
+    let t := (Spec R).homOfLE (U := PrimeSpectrum.basicOpen (a _ i.2)) (V := U i.1)
+      (by rw [ha]; exact le_iSup_of_le _ le_rfl)
+    let iso : restrictFunctor (U i.1).ι ⋙ restrictFunctor ((basicOpenIsoSpecAway _).inv ≫ t) ≅
+        restrictFunctor (Spec.map (CommRingCat.ofHom <| algebraMap _ _)) :=
+      (restrictFunctorComp _ _).symm ≪≫
+        restrictFunctorCongr (by simp [t, basicOpenIsoSpecAway])
+    let pres := SheafOfModules.Presentation.ofIsIso.{u, u, u} (iso.app M).hom <|
+      presentationRestrict ((basicOpenIsoSpecAway _).inv ≫ t) (pres i.1)
+    have : IsIso _ := isIso_fromTildeΓ_of_presentation (M.restrict _) pres
+    rw [isIso_fromTildeΓ_iff_isLocalizing, isLocalizing_iff_aux] at this
+    exact aux_basicOpen_of_aux_restrict _ _ this
+
+set_option backward.isDefEq.respectTransparency false in
+/-- An `𝒪_{Spec R}` module `M` is quasicoherent if and only if it is isomorphic to `Γ(M)^~`. -/
+theorem isQuasicoherent_iff_isIso_fromTildeΓ (M : (Spec R).Modules) :
+    M.IsQuasicoherent ↔ IsIso M.fromTildeΓ := by
+  refine ⟨fun h ↦ inferInstance, fun h ↦ ?_⟩
+  exact (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).prop_of_iso
+    (asIso <| M.fromTildeΓ) inferInstance
+
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
+lemma essImage_tilde : (tilde.functor R).essImage =
+    SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf := by
+  refine le_antisymm ?_ ?_
+  · intro M ⟨N, ⟨e⟩⟩
+    exact (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).prop_of_iso e
+      (by dsimp; infer_instance)
+  · intro M (h : M.IsQuasicoherent)
+    exact ⟨((modulesSpecToSheaf.obj M).presheaf.obj (.op ⊤)), ⟨asIso <| M.fromTildeΓ⟩⟩
+
 end IsQuasicoherent
 
 end AlgebraicGeometry