One twist exponent for a whole finite family of sections #
exists_globalSection_twistBy produces an exponent N, one per section. Serre's global
generation needs a single N serving every generator of every chart at once, because the
surjection it builds, free I ⟶ F(N), has one target sheaf.
This file supplies that: exists_globalSection_twistBy_forall_ge upgrades the existential to
"every sufficiently large N works", and exists_globalSection_twistBy_uniform takes the maximum
over a finite family.
Where the raising happens, and why not at the sheaf level #
The obvious way to raise a global section of F(N) to one of F(N') is to multiply by
f ^ (N' - N) and then transport along F(N)(N' - N) ≅ F(N'). That isomorphism does not exist
for an arbitrary F, and TensorTwist.lean's "What is not here, and why it cannot be got the
easy way" is where the repository already records it: tensorAssocIso requires both outer
factors invertible, and no rearrangement of (F ⊗ O(d)) ⊗ O(e) under tensorCommIso gets the
non-invertible F off an outer slot. TwistComparison.lean's tensorTwistAddIso supplies the
composition only for F an associated sheaf, which is not the hypothesis here.
Even granting the isomorphism the argument would still have to compute what it does to a section,
and these witnesses are built by "sheafification inverts W" — which is exactly what #585
established they cannot do.
Raising is done one level down instead, on the chart extensions, where it is plain algebra.
exists_globalSection_twistBy's recipe has two exponents: n extends s across each chart and
m forces agreement on the pairwise overlaps, with N = 2m + n. Both steps take place in
Γ(F, -) on Proj 𝒜, and:
- the extension at exponent
n + kis the extension at exponentnmultiplied by(f / gᵢ)ᵏ, a section of the structure sheaf over the whole ofD₊(gᵢ)becausefandgᵢboth have degree one; - consequently the overlap discrepancy at exponent
n + kis the discrepancy at exponentnscaled by that same unit, so onemserves everyn' ≥ n.
So N = 2m + n' ranges over every integer ≥ 2m + n with m held fixed, and no sheaf-level
twist comparison is needed anywhere.
This is the same move as exists_pow_smul_eq_res_chart_of_le, which raises the extension exponent
in the chart's own coordinates by isLocalizationElem ^ (m - n) • t. Two differences matter:
ChartExtension.lean is one chart at a time and in away-ring coordinates, and — the reason its
existential form cannot be used here — it returns some extension at the larger exponent, while
holding one overlap exponent m fixed needs the raised family to be the original one times a known
unit. Discard that relation and m has to be re-derived at each n, which puts N = 2m(n) + n
back out of reach.
The multiplier is (f / gᵢ)ᵏ, not a fixed monomial #
gᵢ is inverted on D₊(gᵢ) and nowhere else, and D₊(gᵢ) is the only open where the extension
tᵢ is asked to say anything. Raising by a fraction with a different denominator would produce
a statement that still typechecks — the fraction is a legitimate section wherever its denominator
is invertible — but that vanishes somewhere on D₊(gᵢ), and the raised family would no longer
extend s. The denominator here is fixed by the chart, not chosen.
Scope #
The exponent only. Nothing here mentions generation, local surjectivity, or free I; those need
the chart-local half of Serre's theorem, which is not in this file.
The two fraction identities raising costs #
Both are fracSection_mul followed by fracSection_eq; they are named because the degree
bookkeeping is unreadable inline and because each is used under a •, where the ascription at
Γ(Proj 𝒜, U) is mandatory.
Raising the extension exponent, on the scalar.
(f / g)ᵏ · (f / g)ⁿ = (f / g)ⁿ⁺ᵏ, with the right-hand fractions in the spelling
isLocalizationFrac produces.
Raising commutes with the overlap comparison.
(f / g₁)ᵏ · (g₂ / g₁)ⁿ = (g₂ / g₁)ⁿ⁺ᵏ · (f / g₂)ᵏ. This is why one overlap exponent m serves
every raised family: the two sides of the agreement are raised by different multipliers, one per
chart, and this identity is exactly the statement that the difference between them is absorbed by
the comparison fraction.
The twist exponent can be taken as large as one likes.
exists_globalSection_twistBy with the existential over N replaced by "every N from some
point on". This is the form a family of sections can be given a common exponent in, and it is
the missing ingredient between #585 and Serre's global generation.
The proof holds the overlap exponent m fixed and raises the chart extensions: the family
(f / gᵢ)ᵏ · tᵢ extends s with exponent n + k, and the overlap agreement survives because
fracSection_pow_mul_comm absorbs the difference between the two charts' multipliers. So
N = 2m + (n + k) is reachable for every k, which is every N ≥ 2m + n.
One twist exponent for a finite family of sections, above any prescribed threshold.
The maximum of the per-section thresholds and of N₀; every larger exponent works for every
section by exists_globalSection_twistBy_forall_ge. The threshold is what lets the dévissage on
Pⁿ take N ≥ 1, so that H⁰(O(-N)) vanishes.
One twist exponent for a finite family of sections.
Every sₐ, defined on its own degree-one chart D₊(fₐ), becomes the restriction of a global
section of the same F(N). This is the form Serre's global generation consumes: the generators
of Γ(F, D₊(gᵢ)) for every i form one finite family, and free I ⟶ F(N) needs them all in one
sheaf.
The exponent is the maximum of the thresholds exists_globalSection_twistBy_forall_ge supplies,
which exists because the family is finite.