claimroutineinferred_dep

Curve inequality makes blowup class nef

Shows

A-(1+\sigma)E

is nef on the blow-up, using the curve inequality

gives the margin that makes the target divisor ample

Claim·§2.3 From the curve inequality to all coefficient packets·inside thmInterpolation with separated weights

Statement (paper)

The class

A-(1+\sigma)E

is nef on

X'

, where

A=p^*L

p:X'\to X

is the blow-up of the ideal

I

, and

I\mathcal O_{X'}=\mathcal O_{X'}(-E)

In plain English

On the blow-up

X'

X

along the ideal

I

, with

A=p^*L

and exceptional divisor

E

(so

I\mathcal O_{X'}=\mathcal O_{X'}(-E)

), the class

A-(1+\sigma)E

is nef.

Why it's here

Nefness is checked curve by curve. For a curve

C

X'

, the intersection with

E

is the sum of the ideal orders along its branches, which are

Rh_P

, and the degree of

A

R\deg_W C

. The curve inequality then gives

(A-(1+\sigma)E)\cdot C\ge 0

. This nefness is what the next step uses to show that

aA-E

is ample for large

a

Classified routine:

This follows by checking intersections with curves: the two preceding claims identify the intersections with A and E, and the curve inequality makes their difference nonnegative. It is a direct application of the curve criterion for nefness.

Uses

claimProjective degree equals weighted curve degreeclaimIdeal order along a branch equals weighted contactpropCurve inequality for weighted degree

Used by

claimNef margin makes target divisor ample

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Curve inequality makes blowup class nef" rests on claim-geom-interpolation-2
info
inferred_dep
outline: "Curve inequality makes blowup class nef" rests on claim-geom-interpolation-3
info
inferred_dep
outline: "Curve inequality makes blowup class nef" rests on geom:curve-inequality