The zero module sheaf has finite presentation

On an arbitrary ringed site with binary products, the zero sheaf of modules admits the empty finite presentation. Thus finite presentation contains a zero object independently of any scheme or coherent-sheaf specialization.

Main result

• SheafOfModules.isFinitePresentation_containsZero.

instance SheafOfModules.isFinitePresentation_containsZero {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] : (isFinitePresentation R).ContainsZero

The zero sheaf of modules has finite presentation.