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 AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] (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)

theorem SheafOfModules.GeneratingSections.epi {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {M : SheafOfModules R} (self : M.GeneratingSections) : 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 AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {M : SheafOfModules R} (σ : M.GeneratingSections) : SheafOfModules.free σ.I ⟶ M

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

Equations

• σ.π = M.freeHomEquiv.symm σ.s

def SheafOfModules.GeneratingSections.ofEpi {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {M : SheafOfModules R} {N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] : N.GeneratingSections

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

Equations

• σ.ofEpi p = { I := σ.I, s := fun (i : σ.I) => SheafOfModules.sectionsMap p (σ.s i), epi := ⋯ }

@[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 AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {M : SheafOfModules R} {N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N) [CategoryTheory.Epi p] (i : σ.I) : (σ.ofEpi p).s i = SheafOfModules.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 AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {M : SheafOfModules R} {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 AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {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 AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {M : SheafOfModules R} {N : SheafOfModules R} {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

def SheafOfModules.GeneratingSections.equivOfIso {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasWeakSheafify J AddCommGrp] [J.WEqualsLocallyBijective AddCommGrp] [J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] {M : SheafOfModules R} {N : SheafOfModules R} (e : M ≅ N) : M.GeneratingSections ≃ N.GeneratingSections

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

Equations

• One or more equations did not get rendered due to their size.

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) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] : 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)

theorem SheafOfModules.LocalGeneratorsData.coversTop {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) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] (self : M.LocalGeneratorsData) : J.CoversTop self.X

class SheafOfModules.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) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] : Prop

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

• exists_localGeneratorsData : ∃ (σ : M.LocalGeneratorsData), ∀ (i : σ.I), Finite (σ.generators i).I

theorem SheafOfModules.IsFiniteType.exists_localGeneratorsData {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), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrp} {inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp} {inst_3 : ∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)} [self : M.IsFiniteType], ∃ (σ : M.LocalGeneratorsData), ∀ (i : σ.I), Finite (σ.generators i).I

noncomputable def SheafOfModules.localGeneratorsDataOfIsFiniteType {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) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [h : M.IsFiniteType] : M.LocalGeneratorsData

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

Equations

• M.localGeneratorsDataOfIsFiniteType = ⋯.choose

instance SheafOfModules.instFiniteIOverXLocalGeneratorsDataOfIsFiniteTypeGenerators {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) AddCommGrp] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrp] [∀ (X : C), (J.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)] [h : M.IsFiniteType] (i : M.localGeneratorsDataOfIsFiniteType.I) : Finite (M.localGeneratorsDataOfIsFiniteType.generators i).I

Equations

• ⋯ = ⋯