chore(AlgebraicGeometry): make SheafOfModule.IsQuasicoherent an ObjectProperty and clean up of finiteness conditions (#30372)

We introduce `isQuasicoherent` as an `ObjectProperty (SheafOfModules _)` (and similarly for `isFinitePresentation`). The basic API also undergoes some cleaning up.

Author: joelriou

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

@@ -84,6 +84,12 @@ def equivOfIso (e : M ≅ N) :
     dsimp
     simp only [← opEpi_comp, e.inv_hom_id, opEpi_id]
 
+/-- `σ : M.GeneratingSections` is finite type if the index type `σ.I` is finite. -/
+class IsFiniteType (σ : M.GeneratingSections) : Prop where
+  finite : Finite σ.I := by infer_instance
+
+attribute [instance] IsFiniteType.finite
+
 end GeneratingSections
 
 variable [∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat.{u}]
@@ -101,24 +107,24 @@ structure LocalGeneratorsData where
   /-- the data of sections of `M` over `X i` which generate `M.over (X i)` -/
   generators (i : I) : (M.over (X i)).GeneratingSections
 
+variable {M} in
+/-- The data of local generators of a sheaf of modules is finite type if
+each family of generators is finite type. -/
+class LocalGeneratorsData.IsFiniteType (p : M.LocalGeneratorsData) : Prop where
+  isFiniteType (i : p.I) : (p.generators i).IsFiniteType := by infer_instance
+
 /-- A sheaf of modules is of finite type if locally, it is generated by finitely
 many sections. -/
-class IsFiniteType : Prop where
-  exists_localGeneratorsData :
-    ∃ (σ : M.LocalGeneratorsData), ∀ (i : σ.I), Finite (σ.generators i).I
-
-section
-
-variable [h : M.IsFiniteType]
+class IsFiniteType (M : SheafOfModules.{u} R) : Prop where
+  exists_localGeneratorsData (M) :
+    ∃ (σ : M.LocalGeneratorsData), σ.IsFiniteType
 
 /-- A choice of local generators when `M` is a sheaf of modules of finite type. -/
-noncomputable def localGeneratorsDataOfIsFiniteType : M.LocalGeneratorsData :=
-  h.exists_localGeneratorsData.choose
-
-instance (i : M.localGeneratorsDataOfIsFiniteType.I) :
-    Finite (M.localGeneratorsDataOfIsFiniteType.generators i).I :=
-  h.exists_localGeneratorsData.choose_spec i
-
-end
+@[deprecated "Use the lemma `IsFiniteType.exists_localGeneratorsData` instead."
+  (since := "2025-10-28")]
+noncomputable def localGeneratorsDataOfIsFiniteType (M : SheafOfModules.{u} R)
+    [M.IsFiniteType] :
+    M.LocalGeneratorsData :=
+  (IsFiniteType.exists_localGeneratorsData M).choose
 
 end SheafOfModules

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

@@ -23,14 +23,10 @@ universe u v' u'
 open CategoryTheory Limits
 
 variable {C : Type u'} [Category.{v'} C] {J : GrothendieckTopology C}
-
-
-variable {R : Sheaf J RingCat.{u}}
+  {R : Sheaf J RingCat.{u}}
 
 namespace SheafOfModules
 
-variable (M : SheafOfModules.{u} R)
-
 section
 
 variable [HasWeakSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
@@ -39,12 +35,21 @@ variable [HasWeakSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCom
 /-- A global presentation of a sheaf of modules `M` consists of a family `generators.s`
 of sections `s` which generate `M`, and a family of sections which generate
 the kernel of the morphism `generators.π : free (generators.I) ⟶ M`. -/
-structure Presentation where
+structure Presentation (M : SheafOfModules.{u} R) where
   /-- generators -/
   generators : M.GeneratingSections
   /-- relations -/
   relations : (kernel generators.π).GeneratingSections
 
+/-- A global presentation of a sheaf of module if finite if the type
+of generators and relations are finite. -/
+class Presentation.IsFinite {M : SheafOfModules.{u} R} (p : M.Presentation) : Prop where
+  isFiniteType_generators : p.generators.IsFiniteType := by infer_instance
+  finite_relations : Finite p.relations.I := by infer_instance
+
+attribute [instance] Presentation.IsFinite.isFiniteType_generators
+  Presentation.IsFinite.finite_relations
+
 end
 
 
@@ -54,7 +59,7 @@ variable [∀ X, (J.over X).HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat
 
 /-- This structure contains the data of a family of objects `X i` which cover
 the terminal object, and of a presentation of `M.over (X i)` for all `i`. -/
-structure QuasicoherentData where
+structure QuasicoherentData (M : SheafOfModules.{u} R) where
   /-- the index type of the covering -/
   I : Type u'
   /-- a family of objects which cover the terminal object -/
@@ -65,55 +70,65 @@ structure QuasicoherentData where
 
 namespace QuasicoherentData
 
-variable {M}
-
 /-- If `M` is quasicoherent, it is locally generated by sections. -/
 @[simps]
-def localGeneratorsData (q : M.QuasicoherentData) : M.LocalGeneratorsData where
+def localGeneratorsData {M : SheafOfModules.{u} R} (q : M.QuasicoherentData) :
+    M.LocalGeneratorsData where
   I := q.I
   X := q.X
   coversTop := q.coversTop
   generators i := (q.presentation i).generators
 
+/-- A (local) presentation of a sheaf of module `M` is a finite presentation
+if each given presentation of `M.over (X i)` is a finite presentation. -/
+class IsFinitePresentation {M : SheafOfModules.{u} R} (q : M.QuasicoherentData) : Prop where
+  isFinite_presentation (i : q.I) : (q.presentation i).IsFinite := by infer_instance
+
+attribute [instance] IsFinitePresentation.isFinite_presentation
+
+instance {M : SheafOfModules.{u} R} (q : M.QuasicoherentData) [q.IsFinitePresentation] :
+    q.localGeneratorsData.IsFiniteType where
+  isFiniteType := by dsimp; infer_instance
+
 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 : Prop where
-  nonempty_quasicoherentData : Nonempty M.QuasicoherentData
+class IsQuasicoherent (M : SheafOfModules.{u} R) : Prop where
+  nonempty_quasicoherentData : Nonempty M.QuasicoherentData := by infer_instance
+
+variable (R) in
+@[inherit_doc IsQuasicoherent]
+abbrev isQuasicoherent : ObjectProperty (SheafOfModules.{u} R) :=
+  IsQuasicoherent
 
 /-- A sheaf of modules is finitely presented if it is locally the cokernel of a
 morphism between coproducts of finitely many copies of the sheaf of rings. -/
-class IsFinitePresentation : Prop where
-  exists_quasicoherentData :
-    ∃ (σ : M.QuasicoherentData), ∀ (i : σ.I), (Finite (σ.presentation i).generators.I ∧
-      Finite (σ.presentation i).relations.I)
-
-section
-
-variable [h : M.IsFinitePresentation]
+class IsFinitePresentation (M : SheafOfModules.{u} R) : Prop where
+  exists_quasicoherentData (M) :
+    ∃ (σ : M.QuasicoherentData), σ.IsFinitePresentation
+
+variable (R) in
+@[inherit_doc IsFinitePresentation]
+abbrev isFinitePresentation : ObjectProperty (SheafOfModules.{u} R) :=
+  IsFinitePresentation
+
+instance (M : SheafOfModules.{u} R) [M.IsFinitePresentation] :
+    M.IsQuasicoherent where
+  nonempty_quasicoherentData :=
+    ⟨(IsFinitePresentation.exists_quasicoherentData M).choose⟩
+
+instance (M : SheafOfModules.{u} R) [M.IsFinitePresentation] :
+    M.IsFiniteType where
+  exists_localGeneratorsData := by
+    obtain ⟨σ, _⟩ := IsFinitePresentation.exists_quasicoherentData M
+    exact ⟨σ.localGeneratorsData, inferInstance⟩
 
 /-- A choice of local presentations when `M` is a sheaf of modules of finite presentation. -/
-noncomputable def quasicoherentDataOfIsFinitePresentation : M.QuasicoherentData :=
-  h.exists_quasicoherentData.choose
-
-instance (i : M.quasicoherentDataOfIsFinitePresentation.I) :
-    Finite (M.quasicoherentDataOfIsFinitePresentation.presentation i).generators.I :=
-  have : _ ∧ Finite (M.quasicoherentDataOfIsFinitePresentation.presentation i).relations.I :=
-    h.exists_quasicoherentData.choose_spec i
-  this.1
-
-instance (i : M.quasicoherentDataOfIsFinitePresentation.I) :
-    Finite (M.quasicoherentDataOfIsFinitePresentation.presentation i).relations.I :=
-  have : _ ∧ Finite (M.quasicoherentDataOfIsFinitePresentation.presentation i).relations.I :=
-    h.exists_quasicoherentData.choose_spec i
-  this.2
-
-end
-
-instance [M.IsFinitePresentation] : M.IsFiniteType where
-  exists_localGeneratorsData :=
-    ⟨M.quasicoherentDataOfIsFinitePresentation.localGeneratorsData,
-      by intro; dsimp; infer_instance⟩
+@[deprecated "Use the lemma `IsFinitePresentation.exists_quasicoherentData` instead."
+  (since := "2025-10-28")]
+noncomputable def quasicoherentDataOfIsFinitePresentation
+    (M : SheafOfModules.{u} R) [M.IsFinitePresentation] : M.QuasicoherentData :=
+  (IsFinitePresentation.exists_quasicoherentData M).choose
 
 end SheafOfModules