Descent of finite presentation along a covering family

If the restrictions of a sheaf of modules to the members of a cover are finitely presented, then the original sheaf is finitely presented. Mathlib's SheafOfModules.QuasicoherentData.bind assembles local presentations; the generators and relations of each assembled presentation have the same finite index types as the corresponding local presentation. This supplies a descent criterion used for finite locally free sheaves, whose defining condition includes finite presentation.

instance SheafOfModules.QuasicoherentData.isFinitePresentation_shrink {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (q : M.QuasicoherentData) [q.IsFinitePresentation] : q.shrink.IsFinitePresentation

Shrinking the covering family of finite quasicoherent data keeps each selected local presentation, so the generators and relations of the shrunk data remain finite.

instance SheafOfModules.QuasicoherentData.isFinitePresentation_bind {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), CategoryTheory.HasSheafify ((J.over X).over Y) AddCommGrpCat] [∀ (X : C) (Y : CategoryTheory.Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R) {I : Type u} (X : I → C) (hX : J.CoversTop X) (D : (i : I) → (M.over (X i)).QuasicoherentData) [∀ (i : I), (D i).IsFinitePresentation] : (bind M X hX D).IsFinitePresentation

Assembling finite local presentations along a cover gives a finite presentation on the resulting common cover.

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

A sheaf of modules is finitely presented if its restrictions to a covering family are finitely presented.