Quasicoherent sheaves

A sheaf of modules is quasi-coherent if it admits locally a presentation as the cokernel of a morphism between coproducts of copies of the sheaf of rings. When these coproducts are finite, we say that the sheaf is of finite presentation.

References

• https://stacks.math.columbia.edu/tag/01BD

structure SheafOfModules.Presentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (M : SheafOfModules R) : Type (max (u + 1) u')

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.

• generators : M.GeneratingSections

  generators

• relations : (CategoryTheory.Limits.kernel self.generators.π).GeneratingSections

  relations

class SheafOfModules.Presentation.IsFinite {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] {M : SheafOfModules R} (p : M.Presentation) : Prop

A global presentation of a sheaf of module if finite if the type of generators and relations are finite.

• isFiniteType_generators : p.generators.IsFiniteType
• finite_relations : Finite p.relations.I

structure SheafOfModules.QuasicoherentData {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : Type (max (max (u + 1) (u' + 1)) v')

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.

• I : Type u'

  the index type of the covering

• X : self.I → C

  a family of objects which cover the terminal object

• coversTop : J.CoversTop self.X
• presentation (i : self.I) : (M.over (self.X i)).Presentation

  a presentation of the sheaf of modules M.over (X i) for any i : I

def SheafOfModules.QuasicoherentData.localGeneratorsData {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) : M.LocalGeneratorsData

If M is quasicoherent, it is locally generated by sections.

Equations

• q.localGeneratorsData = { I := q.I, X := q.X, coversTop := ⋯, generators := fun (i : q.I) => (q.presentation i).generators }

@[simp]

theorem SheafOfModules.QuasicoherentData.localGeneratorsData_I {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) : q.localGeneratorsData.I = q.I

@[simp]

theorem SheafOfModules.QuasicoherentData.localGeneratorsData_X {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) (a✝ : q.I) : q.localGeneratorsData.X a✝ = q.X a✝

@[simp]

theorem SheafOfModules.QuasicoherentData.localGeneratorsData_generators {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) (i : q.I) : q.localGeneratorsData.generators i = (q.presentation i).generators

class SheafOfModules.QuasicoherentData.IsFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) : Prop

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.

• isFinite_presentation (i : q.I) : (q.presentation i).IsFinite

instance SheafOfModules.QuasicoherentData.instIsFiniteTypeLocalGeneratorsDataOfIsFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) [q.IsFinitePresentation] : q.localGeneratorsData.IsFiniteType

class SheafOfModules.IsQuasicoherent {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : Prop

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.

• nonempty_quasicoherentData : Nonempty M.QuasicoherentData

@[reducible, inline]

abbrev SheafOfModules.isQuasicoherent {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.ObjectProperty (SheafOfModules R)

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.

Equations

• SheafOfModules.isQuasicoherent R = SheafOfModules.IsQuasicoherent

class SheafOfModules.IsFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) : Prop

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.

• exists_quasicoherentData : ∃ (σ : M.QuasicoherentData), σ.IsFinitePresentation

@[reducible, inline]

abbrev SheafOfModules.isFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.ObjectProperty (SheafOfModules R)

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.

Equations

• SheafOfModules.isFinitePresentation R = SheafOfModules.IsFinitePresentation

instance SheafOfModules.instIsQuasicoherentOfIsFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) [M.IsFinitePresentation] : M.IsQuasicoherent

instance SheafOfModules.instIsFiniteTypeOfIsFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) [M.IsFinitePresentation] : M.IsFiniteType

@[deprecated "Use the lemma `IsFinitePresentation.exists_quasicoherentData` instead." (since := "2025-10-28")]

noncomputable def SheafOfModules.quasicoherentDataOfIsFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) [M.IsFinitePresentation] : M.QuasicoherentData

A choice of local presentations when M is a sheaf of modules of finite presentation.

Equations

• M.quasicoherentDataOfIsFinitePresentation = ⋯.choose