claimroutineinferred_dep

Generic points embed function fields

Claim·§8.2 A complete grid with generic positions·inside propNo algebraic configuration with large heights

Statement (paper)

Let B0⊂B⊂UB_0\subset\mathcal B\subset\mathcal U be fields and let VV be a plane locus (the plane or a curve with irreducible equation ff) over B\mathcal B. If a point of VV with coordinates in U\mathcal U has transcendence degree dim⁡V\dim V over B\mathcal B, then evaluation at that point embeds the function field B(V)\mathcal B(V) into U\mathcal U; in particular every nonzero denominator in B(V)\mathcal B(V) evaluates to a nonzero element. The same holds for a point after adjoining the other grid points to B\mathcal B, using .

In plain English

If a point of a plane locus VV (the plane or a curve with irreducible equation ff) over B\mathcal B has coordinates in U\mathcal U and transcendence degree dim⁡V\dim V over B\mathcal B, then evaluating at it embeds B(V)\mathcal B(V) into U\mathcal U, so nonzero denominators stay nonzero. The same holds for a point after adjoining the other grid points to B\mathcal B.

Why it's here

A point of full transcendence degree satisfies no polynomial relation over B\mathcal B beyond those generated by ff, so evaluation is well defined and injective on B(V)\mathcal B(V). The grid version follows because the generic complete grid keeps the coordinates independent after adjoining the other grid points. This lets the next lemma identify K0(V1)K_0(V_1) with K0(p)K_0(p) for a surviving grid vertex pp without worrying about vanishing denominators.
Classified routine:
This is the standard algebraic-geometry fact that a generic point of an irreducible variety (transcendence degree equal to its dimension) gives an embedding of its function field, as in Lang's treatment of generic points. The grid version follows directly from the earlier generic-grid lemma.

Uses

claimMinimal loci are symmetric, not a common unit circlelemGeneric complete grid with independent coordinates

Used by

lemSome grid vertex is generic

Sources

PaperOpen
Section
§8.2 A complete grid with generic positions
Page
—
Label
—
Line
sections/07-algebra.tex:293
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Generic points embed function fields" rests on claim-alg-obstruction-2
  • info
    inferred_dep
    outline: "Generic points embed function fields" rests on alg:generic-grid