Theorems · Inductive type · algebraic geometry

SheafOfModules.Presentation

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [J.WEqualsLocallyBijective AddCommGrpCat] → SheafOfModules R → Type (max (u + 1) u₁)

A global presentation of a sheaf of modules M consists of a family generators.s of sections s which generate M, and a family of sections which generate the kernel of the morphism generators.π : free (generators.I) ⟶ M.

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Cited by

24 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.HasWeakSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijective