Serre's theorem: a coherent sheaf on Proj is generated by global sections after a twist #
Hartshorne II.5.17 / EGA II 2.7.9, in the global-generation form. For π generated over
π 0 by finitely many elements of degree one and F coherent on Proj π, there is an N such
that F(N) = F β O(N) is a quotient of a finite free sheaf: free I β F(N), equivalently F(N)
has finitely many generating sections.
This closes #586, and it is the first place in the tree where Serre's theorem itself is proved,
as opposed to the section-extension lemma (Glue.lean, Hartshorne II.5.14(a)) that
exists_globalSection_twistBy is. Nothing here assumes global generation, a resolution property,
or an instance supplying the surjection: the inputs are coherence of F, finiteness of the
degree-one generating set, and nothing else.
The argument #
Three layers, each already in the tree, joined here:
- Chart generators (
ChartGeneration.lean). On each chartDβ(gα΅’), coherence gives finitely many sectionssα΅’,βofFover the chart that generateFlocally there. - One twist for all of them (
GlueUniform.lean). Eachsα΅’,β, multiplied bygα΅’α΄Ί, extends to a global sectionΟα΅’,βofF(N), with a singleNserving every chart and every generator. This is where the uniform exponent, not a maximum of per-section exponents, is essential -- see that file for why raising an exponent after the fact is unavailable. - The
O(N)factor (TwistGenerated.lean). OnDβ(gα΅’), every section ofO(N)is locally a multiple ofgα΅’α΄Ί / 1, so every pure tensort β wis locally(r β’ t) β (gα΅’α΄Ί / 1), hence a combination of thetwistBy gα΅’α΄Ίof the chart generators, hence of theΟα΅’,β.
A section of the sheafified tensor product is locally a finite sum of pure tensors
(exists_eq_sum_tmulSection), so IsLocalCombination closes the sum, and its epimorphism
criterion closes the theorem.
F(N) here, β O(-N) β F in TwistInverse.lean #
The statement proved here is the one Hartshorne II.5.17 states first. The passage to
β O(-N) β F is one tensor with O(-N) and the untwisting (F β O(N)) β O(-N) β
F, which
TwistInverse.lean supplies from the tensor inverse of O(N) (the L = O(N) case of #806);
exists_epi_coproduct_twistingSheaf there is the coproduct form.
The exponent is 1 * N #
exists_globalSection_twistBy_uniform twists by f ^ N at degree e * N for generators of
degree e; here e = 1, and 1 * N is not definitionally N. The theorem is therefore stated
with an existential N and instantiated at 1 * Nβ, and the two spellings gα΅’ ^ Nβ and
gα΅’ ^ (1 * Nβ) of the twisting element are reconciled by twistBy_congr rather than by rewriting
inside a dependent type.
A pure tensor of F β O(N) is locally a combination of the twisted chart generators.
Near a point of Dβ(g), the O(N) factor is a multiple of gα΄Ί / 1
(exists_smul_sectionOfMem_eq_res), so the pure tensor is (r β’ t) β (gα΄Ί / 1); the chart
generators write r β’ t as a combination (hs); and sβ β (gα΄Ί / 1) is twistBy gα΄Ί applied to
sβ (twistBy_app). The scalars are carried onto the first factor by smul_tmulSection_left.
The family is given with its local-generation property as a hypothesis, in the exact shape
exists_finite_generators_of_isCoherent produces it, so that the choice of generators is made
once in the main theorem and not again here.
Serre's theorem, in the global-generation form: F(N) is a quotient of a finite free
sheaf for N large.
For π generated over π 0 by finitely many degree-one elements g i and F coherent on
Proj π, there are N and a finite I with an epimorphism free I β F β O(N).
Hartshorne II.5.17 / EGA II 2.7.9. The hypotheses are exactly the ones the chart lemmas take:
coherence, and the degree-one generating family with its finiteness. No global-generation or
resolution hypothesis enters anywhere, and no instance supplies the surjection. The index I is
the disjoint union over the charts of the chart generators, and N is the uniform exponent of
exists_globalSection_twistBy_uniform_ge, pushed above any prescribed Nβ: the dΓ©vissage on
PβΏ wants N β₯ 1, so that Hβ°(O(-N)) vanishes.
Serre's theorem, in the global-generation form, with the exponent unconstrained.
Serre's theorem, phrased through GeneratingSections: F(N) has finitely many generating
sections for N large.