Alphabeta Math
TheoremStatement: 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.

Classical affine zero loci form the Zariski closed sets

Statement

Affine zero loci are the closed sets of a topology on kn: arbitrary intersections and finite unions are zero loci. In particular V(I)V(J)=V(IJ). Every algebraic subset X carries the induced topology, whose closed sets are XV(S).

Facts & Assumptions

Given: An algebraically closed field k, a nonnegative integer n, arbitrary equation sets in k[x1,,xn], and ideals I,J in that ring.

[F1]
[F2]

Replacing equations by their generated ideal does not change their zero locus (A classical zero locus depends only on the generated ideal and its radical).

[F3]

The product ideal consists of finite sums of products (The sum I+J and product IJ of two-sided ideals).

Proof

technique · direct
1.1

For any indexed family (Sλ), a tuple vanishes on λSλ exactly when it vanishes on every Sλ. Hence λV(Sλ)=V(λSλ); the empty intersection is kn.

F1given
1.2

If aV(I)V(J), every product of an element of I with one of J vanishes at a, hence every element of IJ does. If a belongs to neither locus, there are fI,gJ with f(a),g(a)0; then (fg)(a)0, so aV(IJ). This proves both inclusions.

F3givenalgebra
2.1

Replace arbitrary equation sets by generated ideals and iterate the two-set union identity. The zero-set identities for 0 and 1 supply the empty union and the full space. Intersecting these identities with X verifies the induced closed-set axioms.

F1F2step 1.1step 1.2

Sources

Source comparison: Milne, Algebraic Geometry, v6.10, Proposition 2.10, pp. 38–39. Conventions here distinguish arbitrary affine algebraic sets from nonempty irreducible varieties.

Depends on

Used by

Dependency tree · two levels

9 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