Theorems · Theorem · algebraic geometry

SheafOfModules.Presentation.quasicoherentData_I

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : 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} (P : M.Presentation),
  P.quasicoherentData.I = C

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.Limits.HasBinaryProductsCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijectiveCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijective