[Merged by Bors] - feat(Algebra/Category): IsQuasicoherent from a cover

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

@@ -75,6 +75,11 @@ lemma opEpi_id (σ : M.GeneratingSections) :
 lemma opEpi_comp (σ : M.GeneratingSections) (p : M ⟶ N) (q : N ⟶ P) [Epi p] [Epi q] :
     σ.ofEpi (p ≫ q) = (σ.ofEpi p).ofEpi q := rfl
 
+@[simp]
+lemma ofEpi_π (σ : M.GeneratingSections) (p : M ⟶ N) [Epi p] :
+    (σ.ofEpi p).π = σ.π ≫ p := by
+  simp [ofEpi, freeHomEquiv_symm_comp]
+
 /-- Two isomorphic sheaves of modules have equivalent families of generating sections. -/
 def equivOfIso (e : M ≅ N) :
     M.GeneratingSections ≃ N.GeneratingSections where

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

@@ -282,4 +282,48 @@ end
 
 end Adjunction
 
+section Equivalence
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+  {J : GrothendieckTopology C} {K : GrothendieckTopology D} (eqv : C ≌ D)
+  {S : Sheaf J RingCat.{u}} {R : Sheaf K RingCat.{u}}
+  [Functor.IsContinuous.{u} eqv.functor J K] [Functor.IsContinuous.{v} eqv.functor J K]
+  [Functor.IsContinuous.{u} eqv.inverse K J] [Functor.IsContinuous.{v} eqv.inverse K J]
+  (φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat.{u} J K).obj R)
+  (ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat.{u} K J).obj S)
+  (H₁ : Functor.whiskerRight (NatTrans.op eqv.counit) R.val =
+    ψ.val ≫ eqv.inverse.op.whiskerLeft φ.val)
+  (H₂ : φ.val ≫ eqv.functor.op.whiskerLeft ψ.val ≫
+    Functor.whiskerRight (NatTrans.op eqv.unit) S.val = 𝟙 S.val)
+
+/-- If `e : C ≌ D`, then the pushforwards along `e.functor` and `e.inverse` forms an equivalence. -/
+noncomputable
+def pushforwardPushforwardEquivalence : SheafOfModules R ≌ SheafOfModules S where
+  functor := pushforward.{v} φ
+  inverse := pushforward.{v} ψ
+  unitIso :=
+    letI := CategoryTheory.Functor.isContinuous_comp.{v} eqv.inverse eqv.functor K J K
+    letI := CategoryTheory.Functor.isContinuous_comp.{u} eqv.inverse eqv.functor K J K
+    (pushforwardId _).symm ≪≫ pushforwardNatIso _ eqv.counitIso ≪≫
+      pushforwardCongr (by ext1; simpa) ≪≫ (pushforwardComp _ _).symm
+  counitIso :=
+    letI := CategoryTheory.Functor.isContinuous_comp.{v} eqv.functor eqv.inverse J K J
+    letI := CategoryTheory.Functor.isContinuous_comp.{u} eqv.functor eqv.inverse J K J
+    pushforwardComp _ _ ≪≫ pushforwardNatIso _ eqv.unitIso ≪≫
+      pushforwardCongr (by ext1; simpa) ≪≫ pushforwardId _
+  functor_unitIso_comp :=
+    (pushforwardPushforwardAdj eqv.toAdjunction φ ψ H₁ H₂).left_triangle_components
+
+-- Not a simp because the type of the LHS is dsimp-able
+lemma pushforwardPushforwardEquivalence_unit_app_val_app (M U x) :
+    ((pushforwardPushforwardEquivalence eqv φ ψ H₁ H₂).unit.app M).val.app U x =
+      M.val.map (eqv.counit.app U.unop).op x := rfl
+
+-- Not a simp because the type of the LHS is dsimp-able
+lemma pushforwardPushforwardEquivalence_counit_app_val_app (M U x) :
+    ((pushforwardPushforwardEquivalence eqv φ ψ H₁ H₂).counit.app M).val.app U x =
+      M.val.map (eqv.unit.app U.unop).op x := rfl
+
+end Equivalence
+
 end SheafOfModules

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

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
 public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian
+public import Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
 public import Mathlib.CategoryTheory.FiberedCategory.HomLift
 public import Mathlib.CategoryTheory.Comma.Over.Pullback
 
@@ -123,6 +124,13 @@ def Presentation.isColimit {M : SheafOfModules.{u} R} (P : Presentation M) :
   isCokernelEpiComp (c := CokernelCofork.ofπ _ (kernel.condition P.generators.π))
       (Abelian.epiIsCokernelOfKernel _ <| limit.isLimit _) _ rfl
 
+/-- Mapping a presentation under an isomorphism. -/
+@[simps]
+noncomputable def Presentation.of_isIso {M N : SheafOfModules.{u} R} (f : M ⟶ N) [IsIso f]
+    (σ : M.Presentation) : N.Presentation where
+  generators := σ.generators.ofEpi f
+  relations := σ.relations.ofEpi ((kernelCompMono _ f).symm.trans <| eqToIso (by simp)).hom
+
 variable {C' : Type u₂} [Category.{v₂} C'] {J' : GrothendieckTopology C'} {S : Sheaf J' RingCat.{u}}
   [HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat]
   [J'.HasSheafCompose (forget₂ RingCat AddCommGrpCat)]
@@ -182,7 +190,7 @@ variable [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat
 the terminal object, and of a presentation of `M.over (X i)` for all `i`. -/
 structure QuasicoherentData (M : SheafOfModules.{u} R) where
   /-- the index type of the covering -/
-  I : Type u₁
+  I : Type w
   /-- a family of objects which cover the terminal object -/
   X : I → C
   coversTop : J.CoversTop X
@@ -191,6 +199,18 @@ structure QuasicoherentData (M : SheafOfModules.{u} R) where
 
 namespace QuasicoherentData
 
+/-- Shrink the indexing type of `QuasicoherentData` into the universe of the site. -/
+noncomputable
+def shrink {M : SheafOfModules.{u} R} (q : M.QuasicoherentData) :
+    QuasicoherentData.{u₁} M where
+  I := Set.range q.X
+  X i := q.X i.2.choose
+  coversTop X := by
+    refine J.superset_covering (fun Y hY H ↦ ?_) (q.coversTop X)
+    obtain ⟨i, ⟨hi⟩⟩ := (Sieve.mem_ofObjects_iff ..).mp H
+    exact ⟨⟨_, i, rfl⟩, ⟨hi ≫ eqToHom (by grind)⟩⟩
+  presentation i := q.presentation i.2.choose
+
 /-- If `M` is quasicoherent, it is locally generated by sections. -/
 @[simps]
 def localGeneratorsData {M : SheafOfModules.{u} R} (q : M.QuasicoherentData) :
@@ -216,7 +236,10 @@ end QuasicoherentData
 /-- A sheaf of modules is quasi-coherent if it is locally the cokernel of a
 morphism between coproducts of copies of the sheaf of rings. -/
 class IsQuasicoherent (M : SheafOfModules.{u} R) : Prop where
-  nonempty_quasicoherentData : Nonempty M.QuasicoherentData := by infer_instance
+  nonempty_quasicoherentData : Nonempty (QuasicoherentData.{u₁} M) := by infer_instance
+
+lemma QuasicoherentData.IsQuasicoherent {M : SheafOfModules.{u} R} (q : M.QuasicoherentData) :
+    M.IsQuasicoherent := ⟨⟨q.shrink⟩⟩
 
 variable (R) in
 @[inherit_doc IsQuasicoherent]
@@ -227,7 +250,7 @@ abbrev isQuasicoherent : ObjectProperty (SheafOfModules.{u} R) :=
 morphism between coproducts of finitely many copies of the sheaf of rings. -/
 class IsFinitePresentation (M : SheafOfModules.{u} R) : Prop where
   exists_quasicoherentData (M) :
-    ∃ (σ : M.QuasicoherentData), σ.IsFinitePresentation
+    ∃ (σ : QuasicoherentData.{u₁} M), σ.IsFinitePresentation
 
 variable (R) in
 @[inherit_doc IsFinitePresentation]
@@ -284,6 +307,41 @@ theorem Presentation.isQuasicoherent {M : SheafOfModules.{u} R} (P : Presentatio
     IsQuasicoherent M where
   nonempty_quasicoherentData := Nonempty.intro (Presentation.quasicoherentData P)
 
-end
+section bind
+
+variable [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
+  [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
+  [∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
+  [∀ X Y, ((J.over X).over Y).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
+  [∀ X Y, HasSheafify ((J.over X).over Y) AddCommGrpCat.{u}]
+  [∀ X Y, ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat.{u}]
+
+/-- Given an cover `X` and a quasicoherent data for `M` restricted onto each `Mᵢ`, we may glue them
+into a quasicoherent data of `M` itself. -/
+noncomputable def QuasicoherentData.bind {R : Sheaf J RingCat.{u}}
+    (M : SheafOfModules.{u} R) {I : Type u}
+    (X : I → C) (hX : J.CoversTop X) (D : Π i, QuasicoherentData (M.over (X i))) :
+    M.QuasicoherentData where
+  I := Σ i, (D i).I
+  X ij := ((D ij.1).X ij.2).left
+  coversTop Y := J.transitive (hX Y) _ fun Z f ⟨i, ⟨g⟩⟩ ↦
+      J.superset_covering ((Sieve.functorPushforward_ofObjects _ _ _).trans
+      (Sieve.ofObjects_mono fun i' ↦ by aesop)) ((D i).coversTop (.mk g))
+  presentation i :=
+    letI e := pushforwardPushforwardEquivalence (Over.iteratedSliceEquiv ((D i.1).X i.2))
+      (S := (R.over _).over _) (R := R.over _) (𝟙 _) (𝟙 _)
+      (by ext : 2; exact R.1.map_id _) (by ext : 2; exact R.1.map_id _)
+    (((D i.1).presentation i.2).map e.inverse (.refl _)).of_isIso
+      (e.fullyFaithfulFunctor.preimageIso
+      (by exact e.counitIso.app ((M.over (X i.1)).over ((D i.1).X i.2)))).hom
+
+lemma IsQuasicoherent.of_coversTop {R : Sheaf J RingCat.{u}}
+    (M : SheafOfModules.{u} R) {I : Type u}
+    (X : I → C) (hX : J.CoversTop X) [∀ i, IsQuasicoherent (M.over (X i))] :
+    IsQuasicoherent M :=
+  (QuasicoherentData.bind M X hX fun _ ↦
+    IsQuasicoherent.nonempty_quasicoherentData.some).IsQuasicoherent
+
+end bind
 
 end SheafOfModules

Mathlib/CategoryTheory/Sites/Sieves.lean

@@ -747,6 +747,13 @@ lemma ofArrows_eq_ofObjects {X : C} (hX : IsTerminal X)
   rintro ⟨i, ⟨h⟩⟩
   exact ⟨i, h, hX.hom_ext _ _⟩
 
+lemma ofObjects_mono {I : Type*} {X : I → C} {I' : Type*} {X' : I' → C} {Y : C}
+    (h : Set.range X ⊆ Set.range X') :
+    Sieve.ofObjects X Y ≤ Sieve.ofObjects X' Y := by
+  rintro Z f ⟨i, ⟨g⟩⟩
+  obtain ⟨i', h⟩ := h ⟨i, rfl⟩
+  exact ⟨i', ⟨h ▸ g⟩⟩
+
 /-- Given a morphism `h : Y ⟶ X`, send a sieve S on X to a sieve on Y
 as the inverse image of S with `_ ≫ h`. That is, `Sieve.pullback S h := (≫ h) '⁻¹ S`. -/
 @[simps]
@@ -794,6 +801,12 @@ lemma pullback_ofObjects_eq_top
   rw [mem_ofObjects_iff]
   exact ⟨i, ⟨h ≫ g⟩⟩
 
+@[simp]
+lemma pullback_ofObjects {I : Type*} (X : I → C) {Y Z : C} (f : Z ⟶ Y) :
+    (ofObjects X Y).pullback f = ofObjects X Z := by
+  ext
+  simp [Sieve.ofObjects]
+
 /-- Push a sieve `R` on `Y` forward along an arrow `f : Y ⟶ X`: `gf : Z ⟶ X` is in the sieve if `gf`
 factors through some `g : Z ⟶ Y` which is in `R`.
 -/
@@ -1092,6 +1105,12 @@ lemma mem_functorPushforward_iff_of_full_of_faithful [F.Full] [F.Faithful]
   refine ⟨fun ⟨g, hcomp, hg⟩ ↦ ?_, fun hf ↦ ⟨f, rfl, hf⟩⟩
   rwa [← F.map_injective hcomp]
 
+lemma functorPushforward_ofObjects
+    {I : Type*} (X : I → C) (Y : C) :
+    (ofObjects X Y).functorPushforward F ≤ ofObjects (F.obj ∘ X) (F.obj Y) := by
+  rintro Z f ⟨W, g₁, g₂, ⟨i, ⟨g₃⟩⟩, hf⟩
+  exact ⟨i, ⟨g₂ ≫ F.map g₃⟩⟩
+
 end Functor
 
 /-- A sieve induces a presheaf. -/