claimroutineinferred_dep

Vanishing and projective sections generate jets

Shows H1(X,In⊗Ln)=0H^1(X,I^n\otimes L^n)=0, so sections surject onto jets for H=nRH=nR
final step turning geometry into polynomial jet surjectivity
Claim·§2.3 From the curve inequality to all coefficient packets·inside thmInterpolation with separated weights

Statement (paper)

For all sufficiently large nn, H1(X,In⊗Ln)=0H^1(X,I^n\otimes L^n)=0, so H0(X,Ln)H^0(X,L^n) surjects onto the local coefficient data modulo InI^n. Since InI^n consists of local series of weight at least nRnR, this gives surjectivity onto the quotient consisting of the desired packets of weight less than nRnR. Every section of LnL^n is given by a homogeneous degree-nn polynomial in the projective embedding coordinates, which restricts on the affine chart to a polynomial of WW-degree at most nRnR. Hence, taking H=nRH=nR and undoing the filtered Taylor-polynomial coordinate change, the map is surjective.

In plain English

For all large nn, H1(X,In⊗Ln)=0H^1(X,I^n\otimes L^n)=0, so global sections of LnL^n surject onto the local jet data modulo InI^n. Taking H=nRH=nR, this gives surjectivity of the jet map .

Why it's here

This is the final step of the interpolation theorem: the ampleness of A−EA-E from the previous claim gives the cohomology vanishing, which yields surjection onto jets modulo InI^n. Sections of LnL^n are polynomials of WW-degree at most nRnR on the affine chart, and the order of II along branches from the earlier claims identifies the quotient with the weighted jet packets, so the geometric surjectivity becomes the stated polynomial statement.
Classified routine:
This is the standard passage from cohomology vanishing to jet surjectivity via the long exact sequence, followed by the projective-coordinate description of sections. It applies the earlier ampleness and ideal-order claims to identify those jets with the required weighted coefficient packets.

Uses

claimProjective degree equals weighted curve degreeclaimIdeal order along a branch equals weighted contactclaimNef margin makes target divisor ample

Used by

Nothing in the paper

Sources

PaperOpen
Section
§2.3 From the curve inequality to all coefficient packets
Page
—
Label
—
Line
sections/interpolation.tex:536
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Vanishing and projective sections generate jets" rests on claim-geom-interpolation-2
  • info
    inferred_dep
    outline: "Vanishing and projective sections generate jets" rests on claim-geom-interpolation-3
  • info
    inferred_dep
    outline: "Vanishing and projective sections generate jets" rests on claim-geom-interpolation-5