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

A classical affine algebraic set has a unique finite irredundant decomposition

Statement

Assume also Dependent Choice for the cited minimal-prime existence theorem. Assume the Axiom of Choice, inherited from the Nullstellensatz route. Every affine algebraic set X has a finite irredundant decomposition into nonempty irreducible closed subsets, unique up to permutation. These are its maximal irreducible closed subsets. The empty set has the empty decomposition.

Facts & Assumptions

Given: AC and DC, an algebraically closed field k, and an affine algebraic set X⊆kn.

[F1]

A finite-variable polynomial ring over a Noetherian ring is Noetherian (If R is Noetherian then R[x1,…,xn] is Noetherian for every n∈N).

[F3]

A radical ideal in a Noetherian ring is the intersection of finitely many minimal primes, with the empty intersection for the unit ideal (A radical ideal in a Noetherian ring is a finite intersection of minimal primes).

[F4]

Prime ideals correspond to irreducible closed sets; radical ideals are recovered from their loci (Classical affine algebraic sets correspond to radical ideals, and irreducible sets to prime ideals).

Proof

technique · direct
1.1F1F2F3given

Every ideal of the field k is either 0 or k: a nonzero member is invertible, putting 1 in the ideal. These ideals are generated by 0 and 1, respectively, so F2 makes k Noetherian and F1 makes R=k[x1,…,xn] Noetherian, including n=0. Apply F3 to the radical ideal I(X), with its stipulated DC cost, to obtain its distinct minimal primes P1,…,Pm with I(X)=⋂iPi.

2.1F4step 1.1algebra

Put Xi=V(Pi). F4 makes each nonempty irreducible. A point outside every Xi admits fi∈Pi nonzero there; the finite product belongs to every Pi and is nonzero at the point. Thus V(⋂iPi)⊆⋃iXi; the reverse inclusion follows because every element of the intersection vanishes on each Xi. So X=⋃iXi. For m=0, the intersection is R and the union empty. Distinct minimal primes are incomparable; F4 therefore makes the Xi incomparable.

3.1F4F5step 2.1

An irreducible nonempty closed set Z covered by finitely many closed sets must be contained in one: repeatedly split the cover as the first member and the union of the others; if Z is not contained in the first, irreducibility puts it in the remaining union. For a one-member cover this ends immediately; a zero-member cover cannot cover nonempty Z. Thus every irreducible closed subset of X is contained in some Xi, and incomparability makes the Xi precisely the maximal ones. It also prevents removal of an Xi from the cover.

4.1step 3.1∎

If X=⋃jYj is another finite irredundant irreducible closed decomposition, step 3.1 puts each Yj inside an Xi and that Xi inside some Yh. Irredundancy forces Yj=Yh (otherwise Yj could be removed), so Yj=Xi. Reversing the two covers shows their members coincide. After removal of duplicate indexing, this is uniqueness up to permutation.

Sources

Source comparison: Milne, Algebraic Geometry, v6.10, Propositions 2.27, 2.31 and Corollary 2.32, pp. 45–47. Conventions here distinguish arbitrary affine algebraic sets from nonempty irreducible varieties.

Depends on

Used by

Dependency tree · two levels

46 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