Finite presentation of locally free sheaves

This file supplies a general site-level criterion for a locally free sheaf of modules to be finitely presented. Locally free data gives presentations with the chosen bases as generators and no relations, so finiteness of the local bases is enough.

The main result is SheafOfModules.LocalGeneratorsData.IsLocallyFreeData.isFinitePresentation. In particular, when the site has binary products, the free sheaf of modules on a finite type is finitely presented (TauCeti.SheafOfModules.isFinitePresentation_free).

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer B, item "Coherent sheaves and cohomology Hⁱ(X, ℱ)". No formalization is vendored. The proof reuses Mathlib's SheafOfModules.LocalGeneratorsData.quasiCoherentData.

theorem SheafOfModules.LocalGeneratorsData.IsLocallyFreeData.isFinitePresentation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} {q : M.LocalGeneratorsData} (hfree : q.IsLocallyFreeData) (hfinite : q.IsFiniteType) : M.IsFinitePresentation

Locally free data with finite local bases exhibits a finitely presented sheaf.

Mathlib's presentation associated to locally free data uses the local bases as generators and has no relations.

instance TauCeti.SheafOfModules.isFinitePresentation_free {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [∀ (Y : C), CategoryTheory.HasSheafify (J.over Y) AddCommGrpCat] [∀ (Y : C), (J.over Y).WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C] (I : Type u) [Finite I] : (SheafOfModules.free I).IsFinitePresentation

The free sheaf of modules on a finite type is finitely presented.