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 and nonempty open , there is a canonical injective -algebra map . 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 over algebraically closed , a nonempty open , and a regular function on .
Finite intersections of nonempty opens are nonempty and dense (Every nonempty open of a classical affine variety is dense).
Polynomial functions identify faithfully with elements of the coordinate ring (Polynomial functions on an affine algebraic set are its coordinate ring).
Every regular section is locally a quotient (A regular function on an open subset of a classical affine variety).
Regular functions admit pointwise algebra operations (Classical regular functions satisfy locality and unique gluing).
k(X) is the fraction field of the domain A (The function field of an irreducible classical affine variety).
Polynomial zero loci are Zariski closed (Classical affine zero loci form the Zariski closed sets).
Proof
For , choose a nonempty quotient neighbourhood with and nowhere zero on . Then in , so . If on another nonempty quotient neighbourhood , F1 says is nonempty dense. There pointwise. Its zero locus is closed, so it vanishes on X, and F2 gives in A. F5 therefore identifies the two fractions.
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 -algebra map. If s maps to 0, every local quotient has by F5 and step 1.1, hence s vanishes on each quotient neighbourhood and therefore on all U. Thus the map is injective.
If is nonempty open, a quotient neighbourhood for 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.
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
- Every nonempty open of a classical affine variety is dense
- Polynomial functions on an affine algebraic set are its coordinate ring
- A regular function on an open subset of a classical affine variety
- Classical regular functions satisfy locality and unique gluing
- The function field of an irreducible classical affine variety
- The Axiom of Choice
- Classical affine zero loci form the Zariski closed sets
Used by
- Compatible affine charts of an integral classical variety have one function field Lemma
- Dominant maps pull back function fields functorially Lemma
- Dominant rational maps to an affine variety correspond to field embeddings Theorem
- The function field is independent of the chosen nonempty principal affine open Theorem
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
- J. S. Milne, Algebraic Geometry v6.10, §3k p. 74; Definition 3.8 p. 61 (standard reference, not scraped)