TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 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.

Every nonempty principal open is a classical affine variety

Statement

Assume the Axiom of Choice, inherited from the Nullstellensatz route. For an affine variety $X$ and $0 \neq f \in A = k [X]$ , $D_{X} (f)$ with its regular functions is isomorphic to the closed graph $Z = {(x, t) \in X \times k : t f (x) = 1} .$ Its coordinate ring is canonically $A [T] / (T f - 1) ≅ A_{f}$ , a nonzero domain; hence $D_{X} (f)$ is affine in this intrinsic realization.

Facts & Assumptions

Given: AC, an affine variety $X$ over algebraically closed $k$ , $A = k [X]$ , and a nonzero element $f \in A$ .

[F1]

A variety has a nonzero domain coordinate ring and conversely (A classical affine variety has a domain coordinate ring, and conversely).

[F2]

Regular functions on D(f) form A_f (Regular functions on a principal open are the principal localization).

[F3]

Coordinate-ring maps describe affine morphisms (Classical affine morphisms are contravariantly equivalent to coordinate-ring homomorphisms).

[F4]

A value for T defines a polynomial-ring map (Universal property of $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

[F5]

An annihilated relation permits passage to the quotient (A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring).

[F6]

A map making f invertible factors through A_f (Universal property of localisation: maps that invert $S$ factor uniquely through $S^{- 1} R$ ).

[F7]

Prime ideals equal the vanishing ideals of their zero loci (Classical affine algebraic sets correspond to radical ideals, and irreducible sets to prime ideals).

[F8]

Locally regular functions pull back under morphisms (A classical morphism pulls Zariski closed sets back to closed sets).

[F9]

Every global regular function on an affine algebraic set belongs to its coordinate ring (Global regular functions on a classical affine variety are its coordinate ring).

[F10]

Coordinate-ring elements are polynomial functions in the coordinate classes (Polynomial functions on an affine algebraic set are its coordinate ring).

Proof

technique · direct

1.1F4F5F6givenalgebra

In $B = A [T] / (T f - 1)$ the classes of $T$ and $f$ are inverses. F6 defines $A_{f} \to B$ sending $a / f^{r}$ to $a T^{r}$ . Conversely F4 and F5 define $B \to A_{f}$ by $T \mapsto 1 / f$ , since the relation maps to zero. The composites fix $A$ and $T$ on one side and send $a / f^{r}$ to itself on the other, hence are identities.

2.1F1F7step 1.1algebra

By F1, A is a domain. Since $f \neq 0$ , fractions with powers of $f$ embed into its fraction field (a zero image forces the numerator zero). Thus $A_{f}$ , and hence $B$ , is a nonzero domain. The polynomial presentation of $B$ has prime kernel: the inverse image of 0 under its surjection is proper and satisfies the product test. F7 makes its zero locus precisely $Z$ and its coordinate ring exactly $B$ . F1 therefore makes $Z$ a variety.

3.1F2F3step 2.1F9F10

The projection $p : Z \to X$ has image $D (f)$ , and $q : D (f) \to Z$ , $x \mapsto (x, 1 / f (x))$ , is its set-theoretic inverse. Projection is a morphism by the coordinate dictionary F3. The coordinate pullbacks for q are regular: those of X are polynomial restrictions and the last is $1 / f$ , which belongs to F2. Every global regular function on Z is a polynomial in its coordinates by F9 and F10, so q is a morphism as well.

4.1F2F8step 3.1∎

F8 upgrades these maps to pullback on all target opens. Viewing p as a map into the open $D (f)$ has the same property, because any section on an open there is a section on the same open in X. Thus p and q are inverse locally regular morphisms. Finally $D (f)$ is nonempty: otherwise f is the zero polynomial function, contrary to $f \neq 0$ by F2.

Sources

Source comparison: Milne, Algebraic Geometry, v6.10, §3h pp. 71–72 and Proposition 3.11 pp. 61–62. Conventions here distinguish arbitrary affine algebraic sets from nonempty irreducible varieties.

Depends on

Dependency tree · 2 levels

Sources

J. S. Milne, Algebraic Geometry v6.10, §3h pp. 71–72 and Proposition 3.11 pp. 61–62