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} (M : SheafOfModules R) [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] : 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

structure SheafOfModules.QuasicoherentData {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] : 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

theorem SheafOfModules.QuasicoherentData.coversTop {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] (self : M.QuasicoherentData) : J.CoversTop self.X

def SheafOfModules.QuasicoherentData.localGeneratorsData {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] (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_X {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] (q : M.QuasicoherentData) : ∀ (a : q.I), q.localGeneratorsData.X a = q.X a

@[simp]

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

@[simp]

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

class SheafOfModules.IsQuasicoherent {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] : 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

theorem SheafOfModules.IsQuasicoherent.nonempty_quasicoherentData {C : Type u'} : ∀ {inst : CategoryTheory.Category.{v', u'} C} {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {inst_1 : ∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)} {inst_2 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp} {inst_3 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp} [self : M.IsQuasicoherent], Nonempty M.QuasicoherentData

class SheafOfModules.IsFinitePresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] : 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), ∀ (i : σ.I), Finite (σ.presentation i).generators.I ∧ Finite (σ.presentation i).relations.I

theorem SheafOfModules.IsFinitePresentation.exists_quasicoherentData {C : Type u'} : ∀ {inst : CategoryTheory.Category.{v', u'} C} {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {M : SheafOfModules R} {inst_1 : ∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)} {inst_2 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp} {inst_3 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp} [self : M.IsFinitePresentation], ∃ (σ : M.QuasicoherentData), ∀ (i : σ.I), Finite (σ.presentation i).generators.I ∧ Finite (σ.presentation i).relations.I

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

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

Equations

• M.quasicoherentDataOfIsFinitePresentation = ⋯.choose

instance SheafOfModules.instFiniteIOverXQuasicoherentDataOfIsFinitePresentationGeneratorsPresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] [h : M.IsFinitePresentation] (i : M.quasicoherentDataOfIsFinitePresentation.I) : Finite (M.quasicoherentDataOfIsFinitePresentation.presentation i).generators.I

Equations

• ⋯ = ⋯

instance SheafOfModules.instFiniteIOverXQuasicoherentDataOfIsFinitePresentationRelationsPresentation {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (M : SheafOfModules R) [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] [h : M.IsFinitePresentation] (i : M.quasicoherentDataOfIsFinitePresentation.I) : Finite (M.quasicoherentDataOfIsFinitePresentation.presentation i).relations.I

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯