LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27

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.

The spectrum map pulls back vanishing sets

Statement

Let $φ : R \to A$ be a ring homomorphism of commutative rings, and let $I ⊴ R$ be an ideal. Write $I A$ for the ideal of $A$ generated by $φ (I)$ . Then $Spec (φ)^{- 1} (V (I)) = V (I A)$ as subsets of $Spec (A)$ .

Facts & Assumptions

Given: A ring homomorphism $φ : R \to A$ of commutative rings and an ideal $I ⊴ R$ .

[L1]

$V (K)$ is the set of prime ideals containing $K$ (The prime spectrum and vanishing sets).

[L2]

$(φ (I)) = I A$ is the ideal generated by the image of $I$ (The ideal generated by a subset and principal ideals).

Proof

technique · direct

1.1

Let $q \in Spec (A)$ . Then $q \in Spec (φ)^{- 1} (V (I))$ exactly when $φ^{- 1} (q) \in V (I)$ , and by [L1] this is equivalent to $I \subseteq φ^{- 1} (q)$ . That in turn is equivalent to $φ (I) \subseteq q$ .

L1given

2.1

A prime ideal contains the subset $φ (I)$ exactly when it contains the ideal generated by that subset, namely $I A$ by [L2]. Hence the condition from step 1.1 is equivalent to $I A \subseteq q$ , that is, to $q \in V (I A)$ .

L1L2algebra

3.1

Therefore $Spec (φ)^{- 1} (V (I)) = V (I A)$ .

step 1.1step 2.1∎

Depends on

Used by

A ring map induces a contraction map on prime spectra Theorem

Dependency tree · two levels

10 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, A Primer of Commutative Algebra, v4.03, §14 The spectrum of a ring (standard reference, not scraped)
The Stacks Project, Section 10.17: The spectrum of a ring (standard reference, not scraped)