Theorems · Definition · algebraic geometry

SheafOfModules.QuasicoherentData.bind

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] →
        [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
          [inst_3 :
              ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] →
            [inst_4 :
                ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] →
              {R : CategoryTheory.Sheaf J RingCat} →
                (M : SheafOfModules R) →
                  {I : Type u} →
                    (X : I → C) → J.CoversTop X → ((i : I) → (M.over (X i)).QuasicoherentData) → M.QuasicoherentData

Given an cover X and a quasicoherent data for M restricted onto each Mᵢ, we may glue them into a quasicoherent data of M itself.

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijectiveCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijective