Documentation

Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

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 #

source
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.

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

    Instances For
      source
      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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      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 }
      Instances For
        source
        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
        Instances
          source
          theorem SheafOfModules.IsQuasicoherent.nonempty_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] [self : M.IsQuasicoherent] :
          Nonempty M.QuasicoherentData
          source
          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
          Instances
            source
            theorem SheafOfModules.IsFinitePresentation.exists_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] [self : M.IsFinitePresentation] :
            ∃ (σ : M.QuasicoherentData), ∀ (i : σ.I), Finite (σ.presentation i).generators.I ∧ Finite (σ.presentation i).relations.I
            source
            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
            Instances For
              source
              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
              • ⋯ = ⋯
              source
              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
              • ⋯ = ⋯
              source
              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
              • ⋯ = ⋯