TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Classical products and scheme products

Statement

Let $k$ be algebraically closed and let $V, W$ be irreducible classical $k$ -varieties. Write $V^{*}, W^{*}$ for their associated schemes. Then the associated scheme of their classical product is canonically isomorphic to $V^{*} \times_{k} W^{*}$ , compatibly with the projections. For nonempty affine charts with coordinate rings $A, B$ , the product chart ring is the unreduced tensor product $A \otimes_{k} B$ , which is a domain in this setting.

Facts & Assumptions

Given: The objects, hypotheses and conventions in the statement above.

[F1]

Let $X, Y$ be classical affine varieties over an algebraically closed field $k$ . Then their affine product exists, is a classical affine variety, and has coordinate ring $k [X \times_{k} Y] ≅ k [X] \otimes_{k} k [Y] .$ Its projections make it a product in the classical affine-variety category. (The product of affine varieties has coordinate ring k[X] tensor_k k[Y])

[F2]

Let $k$ be algebraically closed. The closed-point construction and its inverse whose points are the nonempty irreducible closed subsets (with each original point identified with its singleton) give an equivalence between irreducible classical $k$ -varieties (which have a finite affine cover by definition) and integral finite-type $k$ -schemes satisfying the affine-overlap separation condition. (Irreducible classical varieties and integral separated finite-type schemes)

[F3]

Every diagram $X \to S \leftarrow Y$ of schemes has a fibre product. Given an affine cover $S = ⋃_{i} Spec A_{i}$ and affine covers $f^{- 1} (Spec A_{i}) = ⋃_{j} Spec B_{i j}$ and $g^{- 1} (Spec A_{i}) = ⋃_{k} Spec C_{i k}$ , the product has open affine cover $Spec (B_{i j} \otimes_{A_{i}} C_{i k}) .$ (Existence of all scheme fibre products)

[F4]

Suppose $P = X \times_{S} Y$ exists, with projections $p, q$ . If opens $V \subseteq X$ , $W \subseteq Y$ map into an open $U \subseteq S$ , then the open subscheme $Q = p^{- 1} (V) \cap q^{- 1} (W)$ represents $V \times_{U} W$ , and also $V \times_{S} W$ . Independently, for $f : X \to S$ and an open $U \subseteq S$ , the open subscheme $f^{- 1} (U)$ represents $X \times_{S} U$ . (Restricting fibre products to open subschemes)

Proof

1.1

Choose nonempty classical affine charts $U \subset V$ , $Z \subset W$ . F1 constructs their classical affine product with ring $A \otimes_{k} B$ . It asserts that this is a classical affine variety, not an arbitrary reduced scheme. By F2 its associated scheme is integral, so its affine coordinate ring is a domain. Thus no reduction of the tensor ring is required. The hypotheses algebraically closed and irreducible are retained.

givenF1F2

2.1

F3 and F4 identify the corresponding open in $V^{*} \times_{k} W^{*}$ with $Spec (A \otimes_{k} B)$ , with the same projections. On chart overlaps these identifications agree after the two projections: a map from any test scheme into the product is uniquely determined by those projections. The associated-scheme construction in F2 preserves the affine restrictions. Hence the local identifications glue and their local inverses glue.

F2F3F4step 1.1

3.1

For completeness, these local classical products construct the classical product globally: glue their chart transitions along overlaps of the two factors. A pair of classical maps factors locally into these charts, and F1 gives its unique local lift; uniqueness glues the lifts. The glued classical space has a finite affine cover by the products of finite covers of $V, W$ . It is separated in the classical sense: the equalizer of two maps into it is the intersection of the equalizers of their two projections, which are closed since $V, W$ are classical varieties. Thus once irreducibility is checked below it is a classical variety. Its associated scheme is the product of step 2.1. The glued classical space is irreducible: its irreducible product charts have pairwise nonempty open intersections, because nonempty affine opens in each irreducible factor intersect; a cover by irreducible opens with these intersections is irreducible. Indeed any nonempty open in one chart meets its intersection with another, and then meets every nonempty open there. Nonemptiness follows from any chart. If a factor is a point, the tensor ring is the other ring.

F1F2step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

Vakil 10.1.3 and 10.4.E; local published affine product theorem (standard reference, not scraped)