Locality of finite presentation on a ringed site

Finite presentation of a sheaf of modules on an arbitrary ringed site is preserved by restriction to an object of the site and descends from a family of objects covering the terminal object.

Main results

• SheafOfModules.QuasicoherentData.isFinitePresentation_over preserves finite local presentation data under restriction;
• SheafOfModules.IsFinitePresentation.over restricts finite presentation;
• SheafOfModules.IsFinitePresentation.of_coversTop glues finite presentation from a covering family.

theorem SheafOfModules.instHasBinaryProductsOver_derivedAlgGeo_1 {C : Type u} [CategoryTheory.Category.{u, u} C] [CategoryTheory.Limits.HasPullbacks C] (X : C) : CategoryTheory.Limits.HasBinaryProducts (CategoryTheory.Over X)

instance SheafOfModules.QuasicoherentData.isFinitePresentation_over {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [hasSheafifyOver : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [hasWeakSheafifyOver : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [wEqualsLocallyBijectiveOver : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [hasSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [hasWeakSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [wEqualsLocallyBijectiveOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {M : SheafOfModules R} (q : M.QuasicoherentData) (U : C) [q.IsFinitePresentation] : (q.over U).IsFinitePresentation

theorem SheafOfModules.IsFinitePresentation.over {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [hasWeakSheafifyOver : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [wEqualsLocallyBijectiveOver : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [hasWeakSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [wEqualsLocallyBijectiveOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] {M : SheafOfModules R} (hM : M.IsFinitePresentation) (U : C) : (M.over U).IsFinitePresentation

Finite presentation is preserved by restriction to an object of the site.

theorem SheafOfModules.IsFinitePresentation.of_coversTop {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [hasSheafifyOver : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [hasWeakSheafifyOver : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [wEqualsLocallyBijectiveOver : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [hasSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [hasWeakSheafifyOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasWeakSheafify ((J.over X).over Y) AddCommGrpCat] [wEqualsLocallyBijectiveOverOver : ∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) {I : Type v} (X : I → C) (hX : J.CoversTop X) (h : ∀ (i : I), (M.over (X i)).IsFinitePresentation) : M.IsFinitePresentation

Finite presentation descends along a family of objects covering the terminal object.