Vector bundles on semilocal affine schemes are free

A finitely generated flat module over a semilocal ring which has the same rank n at every maximal ideal is free of rank n (Mathlib's Module.free_of_flat_of_finrank_eq, Stacks 02M9). Through the equivalence FiniteLocallyFreeSheaf.finiteProjectiveEquiv between finitely generated projective modules and finite locally free sheaves on an affine scheme, a finite locally free sheaf of constant rank n on an affine scheme whose ring of global functions has finitely many maximal ideals is the free sheaf on n generators.

This applies to every scheme finite over a field k: its ring of global functions is a finite-dimensional k-algebra, hence Artinian, hence semilocal. So on such a scheme, for instance on the closed subscheme cut out by an effective Cartier divisor on a curve, every vector bundle of constant rank is trivial. For schemes finite over a field this is the higher-rank analogue of the triviality of line bundles on discrete schemes (TauCeti.AlgebraicGeometry.LineBundleClass.subsingleton_of_discreteTopology).

Main declarations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.nonempty_iso_free_of_finite_maximalSpectrum: over a semilocal ring R, a finite locally free sheaf of constant rank n on Spec R is free on n generators;
• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.nonempty_iso_free_of_isAffine: the same on an affine scheme with semilocal ring of global functions;
• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.nonempty_iso_free_of_isFinite: on a scheme finite over a field, every vector bundle of constant rank r is 𝒪^r.

References

• The Stacks Project, Tag 02M9

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.nonempty_iso_free_of_finite_maximalSpectrum {R : CommRingCat} [Finite (MaximalSpectrum ↑R)] (E : FiniteLocallyFreeSheaf (AlgebraicGeometry.Spec R)) {n : ℕ} (hn : ∀ (x : ↥(AlgebraicGeometry.Spec R)), E.rank x = n) : Nonempty (E ≅ free (AlgebraicGeometry.Spec R) (ULift.{u, 0} (Fin n)))

Vector bundles over a semilocal ring are free. If R has finitely many maximal ideals, a finite locally free sheaf E on Spec R of rank n at every point is isomorphic to the free sheaf on n generators.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.nonempty_iso_free_of_isAffine {X : AlgebraicGeometry.Scheme} {r : ℕ} [AlgebraicGeometry.IsAffine X] [Finite (MaximalSpectrum ↑(X.presheaf.obj (Opposite.op ⊤)))] (E : FixedRank X r) : Nonempty (E ≅ free X r)

Vector bundles on a semilocal affine scheme are free. On an affine scheme X whose ring of global functions has finitely many maximal ideals, every finite locally free sheaf of constant rank r is isomorphic to the free sheaf 𝒪_X^r.

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.FixedRank.nonempty_iso_free_of_isFinite {X : AlgebraicGeometry.Scheme} {r : ℕ} (k : Type u) [Field k] [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsFinite (X ↘ AlgebraicGeometry.Spec ↧k)] (E : FixedRank X r) : Nonempty (E ≅ free X r)

Vector bundles on a scheme finite over a field are free. If X is finite over a field k, every finite locally free sheaf of constant rank r on X is isomorphic to 𝒪_X^r: the ring of global functions of X is a finite-dimensional k-algebra, hence semilocal.