Finite presentation of invertible sheaves

An invertible sheaf is locally free on a one-element basis, so it is locally finitely presented. This file makes that implication available to the scheme-level sheaf API.

The general finite-presentation theorem for locally free data is in TauCeti/Algebra/Category/ModuleCat/Sheaf/FinitePresentation.lean. The only additional step for an invertible sheaf is finiteness of the local bases, supplied by their Subsingleton instances.

The main result is the instance TauCeti.SheafOfModules.IsInvertible.isFinitePresentation. It applies over an arbitrary site; the scheme-level finitely-presented-sheaf packaging is in TauCeti/AlgebraicGeometry/FinitelyPresentedSheaf/Basic.lean.

This advances TauCetiRoadmap/JacobianChallenge/README.md, from Layer A's invertible sheaves to Layer B's coherent sheaves. No formalization is vendored.

instance TauCeti.SheafOfModules.IsInvertible.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} [hM : IsInvertible M] : M.IsFinitePresentation

An invertible sheaf of modules is finitely presented.

The rank-one local bases give finite generating families, and the locally free presentations have no relations.