Theorems · Definition · algebraic geometry

SheafOfModules.Presentation.quasicoherentData

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasBinaryProducts C] →
      {J : CategoryTheory.GrothendieckTopology C} →
        {R : CategoryTheory.Sheaf J RingCat} →
          [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat] →
            [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] →
              [inst_4 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] →
                [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
                  {M : SheafOfModules R} → M.Presentation → M.QuasicoherentData

Given a sheaf of R-modules M and a Presentation M, we may construct the quasi-coherent data on the trivial cover.

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Cited by

4 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasBinaryProductsCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijectiveCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijective