Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-adaptedaudited 2026-09-12
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The rational map (x,y) mapsto y / x on the affine plane is undefined along x = 0

Statement refuted

Not every rational map on affine space extends to a regular map everywhere.

On Ak2 with coordinates (x,y), the quotient y/x is regular on the principal open D(x) and therefore defines a rational map η:Ak2⇢Ak1. Its domain of definition contains every point with x≠0.

It does not extend regularly across any point (0,b) with b≠0. Indeed, an extension near such a point would give an open neighbourhood W of (0,b) and a regular function g on W that agrees with y/x on W∩D(x). By Principal opens form a basis for the Zariski topology on an affine variety, choose a principal open D(h)⊆W with (0,b)∈D(h). Then Regular functions on a principal open are the principal localization of the coordinate ring identifies g∣D(h) with some fraction a/hn∈k[x,y]h, and on the smaller principal open D(h)∩D(x)=D(hx) the same theorem identifies the equality g=y/x with the localization identity ahn=yxin k[x,y]hx. Thus some power of hx annihilates xa−yhn. Since k[x,y] is a domain, it follows that xa=yhn in k[x,y]. Evaluating at (0,b) gives 0=b h(0,b)n, which is impossible because b≠0 and (0,b)∈D(h) means h(0,b)≠0. This contradiction shows that no regular extension exists near (0,b).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources