claimroutineinferred_dep

Nef margin makes target divisor ample

Shows aA−EaA-E is ample for large aa, hence A−EA-E is ample
positivity needed for vanishing of H1H^1
Claim·§2.3 From the curve inequality to all coefficient packets·inside thmInterpolation with separated weights

Statement (paper)

For all sufficiently large a>1a>1, the divisor aA−EaA-E is ample, and consequently, using and the identity , which writes A−EA-E as a positive multiple of the nef class A−(1+σ)EA-(1+\sigma)E plus a positive multiple of the ample class aA−EaA-E, the divisor A−EA-E is ample.

In plain English

For all sufficiently large a>1a>1, the divisor aA−EaA-E on the blow-up is ample, and hence A−EA-E is ample too.

Why it's here

The nef class A−(1+σ)EA-(1+\sigma)E from the previous claim provides the margin: adding a large multiple of AA makes aA−EaA-E ample. Then A−EA-E is a positive multiple of the nef class plus a positive multiple of the ample class aA−EaA-E, so it is ample, which is the positivity needed to get vanishing and jet generation in the next claim.
Classified routine:
This follows from the standard fact that aA−EaA-E is ample for sufficiently large aa on a blow-up, together with the fact that a positive combination of an ample class and a nef class is ample. The nef input is the preceding curve-inequality claim.

Uses

claimCurve inequality makes blowup class nef

Used by

claimVanishing and projective sections generate jets

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Nef margin makes target divisor ample" rests on claim-geom-interpolation-4