Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09
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.

Regular functions on a nonempty open embed in the affine function field

Statement

Assume the Axiom of Choice, inherited from the Nullstellensatz route. For an affine variety X and nonempty open U, there is a canonical injective k-algebra map OX(U)k(X). A quotient presentation on any nonempty open subdomain computes the same field element, and these embeddings commute with restrictions to nonempty opens.

Facts & Assumptions

Given: AC, an affine variety X over algebraically closed k, a nonempty open UX, and a regular function s on U.

[F1]

Finite intersections of nonempty opens are nonempty and dense (Every nonempty open of a classical affine variety is dense).

[F2]

Polynomial functions identify faithfully with elements of the coordinate ring (Polynomial functions on an affine algebraic set are its coordinate ring).

[F3]

Every regular section is locally a quotient (A regular function on an open subset of a classical affine variety).

[F4]

Regular functions admit pointwise algebra operations (Classical regular functions satisfy locality and unique gluing).

[F5]

k(X) is the fraction field of the domain A (The function field of an irreducible classical affine variety).

[F6]

Polynomial zero loci are Zariski closed (Classical affine zero loci form the Zariski closed sets).

Proof

technique · direct
1.1

For sOX(U), choose a nonempty quotient neighbourhood WU with s=a/b and b nowhere zero on W. Then b0 in A, so a/bk(X). If s=c/d on another nonempty quotient neighbourhood W, F1 says WW is nonempty dense. There adbc=0 pointwise. Its zero locus is closed, so it vanishes on X, and F2 gives ad=bc in A. F5 therefore identifies the two fractions.

F1F2F3F5givenalgebraF6
2.1

Define the image of s to be that uniquely determined fraction. Near a point in a common nonempty quotient neighbourhood for s and t, F4 gives the sum and product by cross multiplication; those are exactly the fraction-field operations. Constants map to themselves, so this is a k-algebra map. If s maps to 0, every local quotient a/b has a=0 by F5 and step 1.1, hence s vanishes on each quotient neighbourhood and therefore on all U. Thus the map is injective.

F3F4F5step 1.1algebra
3.1

If VU is nonempty open, a quotient neighbourhood for sV is also a nonempty open subdomain of U. Step 1.1 shows that it computes the same fraction as s. This proves compatibility with restrictions and with every permitted nonempty quotient presentation.

step 1.1step 2.1

Sources

Source comparison: Milne, Algebraic Geometry, v6.10, §3k p. 74; Definition 3.8 p. 61. Conventions here distinguish arbitrary affine algebraic sets from nonempty irreducible varieties.

Depends on

Used by

Dependency tree · two levels

19 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