TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29

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.

Going up for integral ring maps

Statement

Assume the Axiom of Choice.

Let $f : A \to B$ be an integral ring map. Suppose $p_{1} \subseteq p_{2}$ are prime ideals of $A$ and $q_{1}$ is a prime ideal of $B$ with $f^{- 1} (q_{1}) = p_{1}$ . Then there exists a prime ideal $q_{2}$ of $B$ such that $q_{1} \subseteq q_{2}$ and $f^{- 1} (q_{2}) = p_{2}$ .

Facts & Assumptions

Given: An integral ring map $f : A \to B$ , primes $p_{1} \subseteq p_{2}$ in $A$ , and a prime $q_{1}$ of $B$ lying over $p_{1}$ .

[L1]

Integral ring maps are the maps whose target elements satisfy monic equations over the source ring (Integral ring maps and integral extensions).

[L2]

Assuming the Axiom of Choice, every prime of the source containing the kernel has a prime above it under an integral map (Lying over for integral ring maps).

[L3]

Prime ideals of a quotient correspond exactly to primes containing the quotient ideal (Prime ideals of a quotient ring are exactly the prime ideals containing the ideal).

Proof

technique · direct

1.1L1L3given

The map $f$ induces a ring map $\overline{f} : A / p_{1} \to B / q_{1}$ , and this induced map is integral because a monic equation for $b \in B$ over $A$ descends to the same monic equation for $b + q_{1}$ over $A / p_{1}$ . By [L3], the prime $p_{2}$ corresponds to the prime $p_{2} / p_{1}$ of $A / p_{1}$ .

2.1L2step 1.1

Apply [L2] to $\overline{f}$ and the prime $p_{2} / p_{1}$ . This yields a prime ${\overline{q}}_{2}$ of $B / q_{1}$ with contraction $p_{2} / p_{1}$ .

3.1L3step 2.1∎

By [L3], the prime ${\overline{q}}_{2}$ corresponds to a prime ideal $q_{2}$ of $B$ containing $q_{1}$ . Its contraction to $A$ is exactly $p_{2}$ . Therefore $q_{2}$ is the required prime above $p_{2}$ .

Depends on

Used by

Integral extensions lift finite prime chains from the base Corollary
Finite morphisms are closed with finite fibres Theorem

Dependency tree · two levels

13 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

Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Theorem (14.3)(4) (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, v4.03, Theorem 7.6 (standard reference, not scraped)