Theorems · Theorem · algebraic geometry

SheafOfModules.QuasicoherentData.ofIsIso_X

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (f : M ⟶ N)
  [inst_3 : CategoryTheory.IsIso f] (σ : M.QuasicoherentData) (a : σ.I),
  (SheafOfModules.QuasicoherentData.ofIsIso f σ).X a = σ.X a

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.HasSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijectiveCategoryTheory.IsIso