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 : arbitrary intersections and finite unions are zero loci. In particular . Every algebraic subset carries the induced topology, whose closed sets are .
Facts & Assumptions
Given: An algebraically closed field , a nonnegative integer , arbitrary equation sets in , and ideals in that ring.
The empty and full sets are zero loci (Classical affine algebraic sets, including the empty boundaries).
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).
The product ideal consists of finite sums of products (The sum and product of two-sided ideals).
Proof
For any indexed family , a tuple vanishes on exactly when it vanishes on every . Hence ; the empty intersection is .
If , every product of an element of with one of vanishes at , hence every element of does. If belongs to neither locus, there are with ; then , so . This proves both inclusions.
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 verifies the induced closed-set axioms.
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
- A classical affine variety Definition
- A principal open subset of a classical affine variety Definition
- A classical affine algebraic set has a unique finite irredundant decomposition Lemma
- A classical morphism pulls Zariski closed sets back to closed sets Lemma
- Dominant maps pull back function fields functorially Lemma
- Principal opens form a basis and multiply under intersection Lemma
- Regular functions on a nonempty open embed in the affine function field Lemma
- Zero loci and vanishing ideals form a Galois connection Lemma
- Classical affine algebraic sets correspond to radical ideals, and irreducible sets to prime ideals Theorem
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
- J. S. Milne, Algebraic Geometry v6.10, Proposition 2.10, pp. 38–39 (standard reference, not scraped)