Generating sections of sheaves of modules

In this file, given a sheaf of modules M over a sheaf of rings R, we introduce the structure M.GeneratingSections which consists of a family of (global) sections s : I → M.sections which generate M.

We also introduce the structure M.LocalGeneratorsData which contains the data of a covering X i of the terminal object and the data of a (M.over (X i)).GeneratingSections for all i. This is used in order to define sheaves of modules of finite type.

References

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

structure SheafOfModules.GeneratingSections {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')

The type of sections which generate a sheaf of modules.

• I : Type u

  the index type for the sections

• s : self.I → M.sections

  a family of sections which generate the sheaf of modules

• epi : CategoryTheory.Epi (M.freeHomEquiv.symm self.s)

@[reducible, inline]

noncomputable abbrev SheafOfModules.GeneratingSections.π {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} (σ : M.GeneratingSections) : free σ.I ⟶ M

The epimorphism free σ.I ⟶ M given by σ : M.GeneratingSections.

def SheafOfModules.GeneratingSections.ofEpi {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 N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] : N.GeneratingSections

If M ⟶ N is an epimorphism and that M is generated by some sections, then N is generated by the images of these sections.

@[simp]

theorem SheafOfModules.GeneratingSections.ofEpi_s {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 N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] (i : σ.I) : (σ.ofEpi p).s i = sectionsMap p (σ.s i)

@[simp]

theorem SheafOfModules.GeneratingSections.ofEpi_I {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 N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] : (σ.ofEpi p).I = σ.I

theorem SheafOfModules.GeneratingSections.opEpi_id {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} (σ : M.GeneratingSections) : σ.ofEpi (CategoryTheory.CategoryStruct.id M) = σ

theorem SheafOfModules.GeneratingSections.opEpi_comp {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 N P : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) (q : N ⟶ P) [CategoryTheory.Epi p] [CategoryTheory.Epi q] : σ.ofEpi (CategoryTheory.CategoryStruct.comp p q) = (σ.ofEpi p).ofEpi q

@[simp]

theorem SheafOfModules.GeneratingSections.ofEpi_π {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 N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] : (σ.ofEpi p).π = CategoryTheory.CategoryStruct.comp σ.π p

def SheafOfModules.GeneratingSections.equivOfIso {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 N : SheafOfModules R} (e : M ≅ N) : M.GeneratingSections ≃ N.GeneratingSections

Two isomorphic sheaves of modules have equivalent families of generating sections.

class SheafOfModules.GeneratingSections.IsFiniteType {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} (σ : M.GeneratingSections) : Prop

σ : M.GeneratingSections is finite type if the index type σ.I is finite.

• finite : Finite σ.I

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

The data of generating sections of the restriction of a sheaf of modules over a covering of the terminal object.

• 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
• generators (i : self.I) : (M.over (self.X i)).GeneratingSections

  the data of sections of M over X i which generate M.over (X i)

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

The data of local generators of a sheaf of modules is finite type if each family of generators is finite type.

• isFiniteType (i : p.I) : (p.generators i).IsFiniteType

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

A sheaf of modules is of finite type if locally, it is generated by finitely many sections.

• exists_localGeneratorsData : ∃ (σ : M.LocalGeneratorsData), σ.IsFiniteType

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

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

A choice of local generators when M is a sheaf of modules of finite type.