lemmaroutineinferred_dep

Some grid vertex is generic

Lemma·alg:surviving-point·§8.3 Differentiation and the surviving generic point

Statement (paper)

Some p=pip=p_i has transcendence degree d1d_1 over K0K_0, and evaluation identifies the function field K0(V1)K_0(V_1) with K0(p)K_0(p).

In plain English

Among the grid vertices pip_i, some p=pip=p_i has transcendence degree d1d_1 over K0K_0, and evaluation at pp identifies the function field K0(V1)K_0(V_1) with K0(p)K_0(p).

Why it's here

This supplies a single generic point of V1V_1 that stands in for the whole locus, so that rational functions on V1V_1 can be evaluated at pp without denominators vanishing. Full transcendence degree comes from the independent coordinates of the generic grid, and the identification of K0(V1)K_0(V_1) with K0(p)K_0(p) follows from the embedding of function fields at generic points. The later differentiation argument relies on this.
Classified routine:
A direct consequence of the earlier generic-grid lemma, whose independent coordinates give full transcendence degree, combined with the standard fact that evaluation at a generic point embeds the function field. Together these yield the identification of K0(V1)K_0(V_1) with K0(p)K_0(p).

Uses

lemGeneric complete grid with independent coordinatesclaimGeneric points embed function fields

Used by

claimUnused sign change contradicts nonzero derivative

Sources

PaperOpen
Section
§8.3 Differentiation and the surviving generic point
Page
—
Label
alg:surviving-point
Line
sections/07-algebra.tex:395
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: 07-algebra.tex:412-413: "The function-field assertion is the evaluation argument following ", i.e. lines 293-310 (claim-alg-obstruction-3).