Theorems · Theorem · algebraic geometry

SheafOfModules.IsFinitePresentation.exists_quasicoherentData

∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat}
  {inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} (M : SheafOfModules R)
  [self : M.IsFinitePresentation], ∃ σ, σ.IsFinitePresentation

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Cited by

0 results in Mathlib

Foundations

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

Assumes

SheafOfModules.IsFinitePresentation