ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

Vanishing sets and vanishing ideals form a contravariant Galois connection

Example

Let $k$ be a field and $A = k [x_{1}, \dots, x_{n}]$ . For $S \subseteq A$ and $X \subseteq k^{n}$ , define

$V (S) : = {a \in k^{n} : f (a) = 0 for every f \in S},$

$I (X) : = {f \in A : f (a) = 0 for every a \in X} .$

Then $V$ and $I$ reverse inclusion and satisfy

$X \subseteq V (S) ⟺ S \subseteq I (X) .$

They therefore form a contravariant Galois connection. Moreover $V I V = V$ and $I V I = I$ .

Facts & Assumptions

Given: A field $k$ , a natural number $n$ , a subset $S \subseteq k [x_{1}, \dots, x_{n}]$ , and a subset $X \subseteq k^{n}$ .

[F1]

Multivariate polynomial rings are defined recursively by $R [x_{1}, \dots, x_{0}] = R$ and $R [x_{1}, \dots, x_{n + 1}] = R [x_{1}, \dots, x_{n}] [x_{n + 1}]$ , with commuting indeterminates (Polynomial rings in finitely many commuting indeterminates by iteration).

[F2]

For $f = \sum_{i} a_{i} x^{i}$ and a unital homomorphism $φ : R \to S$ , evaluation is $f_{φ} (s) = \sum_{i} φ (a_{i}) s^{i}$ , and a root is an $s$ at which this value is zero (Evaluation and roots of a polynomial in a commutative target ring).

[F3]

For commutative rings $R, S$ , a unital ring homomorphism $φ ⁣ : R \to S$ , and $s \in S$ , there is a unique unital ring homomorphism ${ev}_{φ, s} ⁣ : R [x] \to S$ extending $φ$ on constant polynomials and sending $x$ to $s$ (Universal property of $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

[F4]

In a commutative ring, an ideal is an additive subgroup closed under multiplication by arbitrary ring elements (Left, right and two-sided ideals).

[F5]

A nonempty subset is an ideal exactly when it is closed under differences and multiplication by ring elements (Ideal criteria and intersections of ideals).

[F6]

Mutually left and right adjoint contravariant functors are characterized by a natural correspondence of arrows with both variances reversed (Mutually left and mutually right adjoint contravariant functors).

Verification

technique · direct

1.1

Simultaneous evaluation. For $a = (a_{1}, \dots, a_{n}) \in k^{n}$ define ${ev}_{a} ⁣ : A \to k$ by induction on $n$ . For $n = 0$ , [F1] gives $A = k$ and ${ev}_{a} = 1_{k}$ . For the step, [F1] gives $k [x_{1}, \dots, x_{n}] = k [x_{1}, \dots, x_{n - 1}] [x_{n}]$ , so [F3] applied with $φ = {ev}_{(a_{1}, \dots, a_{n - 1})}$ and $s = a_{n}$ yields a unital ring homomorphism ${ev}_{a} ⁣ : A \to k$ fixing $k$ and sending each $x_{i}$ to $a_{i}$ ; on a single indeterminate its formula is that of [F2]. Write $f (a) : = {ev}_{a} (f)$ . Being a ring homomorphism, ${ev}_{a}$ satisfies $(f - g) (a) = f (a) - g (a)$ and $(r f) (a) = r (a) f (a)$ .

F1F2F3inductionconstruct

2.1

The zero polynomial lies in $I (X)$ . If $f, g \in I (X)$ and $r \in A$ , then step 1.1 gives $(f - g) (a) = 0 - 0 = 0$ and $(r f) (a) = r (a) \cdot 0 = 0$ for every $a \in X$ , so [F5] makes $I (X)$ an ideal.

step 1.1F4F5algebra

2.2

If $S \subseteq T$ , every common zero of $T$ is a common zero of $S$ , so $V (T) \subseteq V (S)$ . If $X \subseteq Y$ , every polynomial vanishing on $Y$ vanishes on $X$ , so $I (Y) \subseteq I (X)$ .

step 1.1given

2.3

By the two displayed definitions, $X \subseteq V (S)$ means exactly that $f (a) = 0$ for every $a \in X$ and $f \in S$ , which means exactly that $S \subseteq I (X)$ .

step 1.1given

3.1

Regard subsets and ideals as inclusion preorders. Steps 2.2 and 2.3 give the contravariant arrow correspondence required by [F6], hence $V$ and $I$ form the claimed Galois connection.

step 2.2step 2.3F6

3.2

Applying step 2.3 to $S$ and $V (S)$ gives $S \subseteq I (V (S))$ , hence $V (I (V (S))) \subseteq V (S)$ by step 2.2; the reverse inclusion holds because every polynomial in $I (V (S))$ vanishes on $V (S)$ . Thus $V I V = V$ .

step 2.2step 2.3

4.1

Dually, $X \subseteq V (I (X))$ and inclusion reversal give $I (V (I (X))) \subseteq I (X)$ , while the opposite inclusion follows from the definition of $V (I (X))$ . Thus $I V I = I$ .

step 2.2step 2.3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 37 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Emily Riehl, Category Theory in Context, 2nd ed., Example 4.4.2 (standard reference, not scraped)