Theorems · Theorem · algebraic geometry

SheafOfModules.IsQuasicoherent.of_coversTop

∀ {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)).IsQuasicoherent], M.IsQuasicoherent

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijectiveCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijectiveSheafOfModules.IsQuasicoherent