The section-extension lemma: a section over D₊(f) becomes a global section of a twist #
exists_globalSection_twistBy is the deliverable of #585. For F quasi-coherent on Proj 𝒜
and s a section over D₊(f), some f ᵏ · s is the restriction of a global section of a
twist of F.
This is not Serre's theorem #
It is Hartshorne II.5.14(a) / Stacks 01PW, the section-extension lemma.
Serre's theorem is Hartshorne II.5.17 / EGA II 2.7.9: a coherent F on Proj S is a quotient
of a finite ⊕ O(-dᵢ), equivalently F(n) is generated by global sections for n ≫ 0. The
completed #570 route passes through #586: GlobalGeneration.lean proves the global-generation
form exists_epi_free_tensorTwist, and TwistInverse.lean supplies the final untwisted coproduct
epimorphism. This file is the section-extension input to that route, not Serre's theorem by itself.
The distinction is stated here because it is the one a summary loses. TwistSection.lean calls
this "the extension theorem of #585", which is right; roadmap prose has more than once slid from
that to "Serre". This file alone does not prove Serre; the surjection is assembled downstream.
The two exponents, and why they cannot be one #
ChartProj.exists_pow_smul_eq_res_image_uniform gives an n and, over each D₊(gᵢ), a section
tᵢ restricting to fⁿ / gᵢᵉⁿ · s where D₊(f) reaches. That is all the geometry there is, and
it is not enough: TopCat.Sheaf.IsCompatible wants the tᵢ to agree on the whole overlap
D₊(gᵢ) ⊓ D₊(gⱼ), and D₊(f) is not contained in it.
The second exponent closes that. tᵢ and gⱼᵉⁿ / gᵢᵉⁿ · tⱼ do agree on
D₊(gᵢ) ⊓ D₊(gⱼ) ⊓ D₊(f) -- that is the computation hagree below, and it is where the two
charts' different denominators cancel -- so separatedness on the overlap gives an m with
(f² / (gᵢgⱼ)ᵉ)ᵐ killing the difference on the whole overlap. The overlap is the chart of gᵢ gⱼ,
which has degree two; that is why AwayChart.lean exists.
The e in that denominator is the degree of f. isLocalizationFrac balances a degree-e
numerator against a degree-d denominator by raising each to the other's degree, so every
g-side exponent below carries a factor of e that the degree-one statement cannot see.
What is twisted, and with which element #
Not gᵢ ᴺ. The section that glues is twistBy (f²ᵐ gᵢᵉⁿ) of tᵢ, a section of F(e · N) for
N = 2m + n. Two facts fall out of FracSection.twistBy_app_eq_smul' and no others are needed:
- over
D₊(gᵢ) ⊓ D₊(gⱼ), the ratiof²ᵐ gᵢᵉⁿ / ((gᵢgⱼ)ᵉ)ᵐ gᵢᵉⁿis exactly the scalar the agreement supplies, so the two twisted sections differ by applying one map to the two sides of the agreement; - over
D₊(gᵢ) ⊓ D₊(f),f ᴺ / f²ᵐ gᵢᵉⁿis exactlyfⁿ / gᵢᵉⁿ, so every twisted section restricts totwistBy (f ᴺ)ofsthere -- which is what identifies the glued section.
Choosing twistBy (gᵢᵉᴺ) instead would still target F(e · N), but the chart agreement first
lives in F(e · n). Passing from that comparison to the needed section would require the
unavailable composition F(e · n)(2e · m) ≅ F(e · N); nothing provides that, and it is not needed.
The three-step shape #
The theorem is assembled from two lemmas that take the exponents as data, because a downstream caller needs to choose them rather than accept whatever the chart lemmas happen to produce.
exists_overlap_exponenttakes the extension exponentnand the familytand produces the overlap exponentm;exists_globalSection_twistBy_of_datatakes both exponents and the family and does the gluing. It does not need quasi-coherence -- that hypothesis is spent entirely on producingn,tandm, and nothing in the gluing itself uses it.
GlueUniform.lean reuses the same two lemmas with m held fixed and n raised, which is how a
single exponent is reached for a whole finite family.
Scope #
The theorem and its two halves. The hypotheses are the honest ones: F quasi-coherent, the cover
given by finitely many degree-one elements generating A over 𝒜 0, and f homogeneous of any
positive degree.
Generation in degree one is not a convenience and must not be weakened: it is Hartshorne
II.5.12's hypothesis, and without it the standard guarantee that O(n) is locally free is
unavailable. It is f alone that #823
lifted off degree one, which is what Hartshorne II.5.14(a) and Stacks 01PW state.
Restriction of sections #
The generic facts -- resSection_trans, resSection_smul, homApp_res -- moved to
Modules/Restriction/Sections.lean in #824; they are stated for any scheme and never used the
grading. What stays here is the one that is genuinely about Proj.
A fraction restricts to the same fraction, because it is defined pointwise.
The glue, from the two exponents and the chart extensions as data.
The mathematical content of exists_globalSection_twistBy, with the two exponents and the family
of chart extensions taken as inputs rather than produced inside. n, t and ht are what
exists_pow_smul_eq_res_image_uniform supplies; m and hm are what
exists_pow_smul_eq_of_res_eq_image_uniform supplies once the overlap agreement is derived from
ht.
Splitting it out is what makes the exponent controllable. The theorem below instantiates it at the
exponents those two lemmas happen to produce, and GlueUniform.lean instantiates it at a
prescribed n, which is how a single N is reached for a whole finite family of sections.
The overlap exponent, from the chart extensions as data.
The second half of exists_globalSection_twistBy's recipe: given the family t extending s
across each chart with exponent n, this is the exponent m that forces the extensions to agree
on the whole pairwise overlap, not only where D₊(f) reaches.
Like exists_globalSection_twistBy_of_data, it takes n, t and ht as inputs. That is what
lets GlueUniform.lean fix one m and then vary n freely: the agreement at exponent n + k is
the agreement at exponent n scaled by (f / gᵢ)ᵏ, so the same m serves every larger
exponent.
#585: a section over D₊(f), twisted, is the restriction of a global section.
For F quasi-coherent on Proj 𝒜, f homogeneous of any positive degree e, and a finite
family of degree-one elements generating A over 𝒜 0, every s ∈ Γ(F, D₊(f)) has a k with
twistBy (f ᵏ) s the restriction of a global section of F(e · k).
This is Hartshorne II.5.14(a) / Stacks 01PW. It is not Serre's theorem (II.5.17), which is
#570; this is one of its three steps.
The twist degree is e * k rather than k because f ᵏ has degree e * k. At e = 1 the two
agree, which is the form #585 proved and GlueUniform.lean still consumes.
The two exponents are independent: n extends s across each chart, m forces agreement on the
pairwise overlaps, and k = 2m + n. The section over D₊(gᵢ) that glues is twistBy (f²ᵐ gᵢᵉⁿ)
of the chart extension, not twistBy (gᵢᵉᴺ); the chart agreement first lives in F(e · n), and
the chosen factor avoids the unavailable passage from F(e · n)(2e · m) to F(e · k).
The g-side exponents carry a factor of e that the degree-one statement cannot see:
isLocalizationFrac balances a degree-e numerator against a degree-one denominator by raising
the denominator to the e, so gᵢ ⁿ becomes gᵢ ᵉⁿ everywhere below.
Two things this does not say, and what they would take #
The glued section is not claimed unique. TopCat.Sheaf.existsUnique_gluing' returns ∃!, and
the proof below discards the uniqueness half when it destructures. For the local family it is
built from, σ is unique; the statement simply does not carry that. A consumer needing
canonicity — the same σ reached by two routes, say — has to redo the gluing rather than recover
uniqueness from this. Strengthening the conclusion to ∃! would mean naming the local family in
the statement, which is what the existential over k currently hides.
The exponent cannot be raised here. There is deliberately no _of_le: from a witness at k
one cannot conclude one at k + j. Raising would need F(e k)(e j) ≅ F(e (k + j)) for arbitrary
F, and TensorTwist.lean records why the monoidal structure cannot supply it — tensorAssocIso
needs both outer factors invertible and F is not. GlueUniform.lean gets a uniform exponent
the only available way, by re-running this construction at a prescribed n rather than raising
what it produced.