Documentation

Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

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 #

The type of sections which generate a sheaf of modules.

  • I : Type u

    the index type for the sections

  • s : self.IM.sections

    a family of sections which generate the sheaf of modules

  • epi : CategoryTheory.Epi (M.freeHomEquiv.symm self.s)
Instances For
    @[reducible, inline]

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

    Equations
    • σ = M.freeHomEquiv.symm σ.s
    Instances For
      @[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]

      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
      Instances For

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          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.IC

            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)

          Instances For
            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)] :

            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
            Instances
              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
              Instances For
                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
                • =