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 principal open are the principal localization of the coordinate ring
Statement
Assume the Axiom of Choice.
Let be a classical affine variety over an algebraically closed field , and let . Put .
A function is called regular on if there exist finitely many pairs in such that and
Write for the ring of regular functions on .
Then evaluation induces a ring isomorphism If , both sides are the zero ring.
Facts & Assumptions
Given: The Axiom of Choice, a classical affine variety over an algebraically closed field , an element , and the principal open .
The principal localization consists of fractions , and localizing at gives the zero ring (Principal localisation ).
In a localization, exactly when for some (Equality, vanishing, and the kernel of the localisation map).
An element of is zero exactly when any polynomial representative vanishes on all of (The coordinate ring of an affine algebraic set, The vanishing ideal of a subset of affine space).
Principal opens are open, and (Principal opens form a basis for the Zariski topology on an affine variety).
Every nonempty open subset of a classical affine variety is dense (Every nonempty open subset of an affine variety is dense).
Assuming the Axiom of Choice, over an algebraically closed field one has for every ideal in a polynomial ring (Strong Nullstellensatz: I(V(I)) equals the radical of I).
Proof
A fraction defines a function on by If , then after passing to the common denominator their difference is with . By [L2], some power of annihilates . Evaluating at a point of , where is nonzero, forces , so the two fractions give the same function. Thus there is a well-defined ring homomorphism .
If , then for every , so in . By [L1], the localization is the zero ring. The only function is both additive and multiplicative identity, so is also the zero ring. Hence the statement is proved in this boundary case.
Let , given by a finite principal-open cover and local formulas Discard the indices with ; the remaining family still covers the nonempty open set , and relabel it as . For any , the overlap is open by [L4]. It is also nonempty because is a nonempty open subset of , while [L5] makes dense in . On that overlap the two local expressions for agree, so the class vanishes on a dense subset of and therefore on all of . By [L3],
Choose representatives of . Because , a point of lies outside exactly when all vanish there. Thus inside . Applying [L6] gives so for some there exist and with Passing to yields
Assume now that . To prove injectivity, let map to the zero function on . Then for every . On the complement one has . Therefore for every , so in . By [L2], this implies in . Thus is injective.
Define Fix . Using the relations from step 1.3 and then step 1.4, we compute Since , division in the field gives Because the cover , this holds for every . Hence , so is surjective.
Step 2.1 proves injectivity, step 2.2 proves surjectivity, and step 1.2 handles the empty-open boundary. Therefore is a ring isomorphism.
Depends on
Principal localisation
A principal open subset of a classical affine variety
The coordinate ring of an affine algebraic set
The vanishing ideal of a subset of affine space
Principal opens form a basis for the Zariski topology on an affine variety
Every nonempty open subset of an affine variety is dense
Equality, vanishing, and the kernel of the localisation map
Strong Nullstellensatz: I(V(I)) equals the radical of I