Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

Lying over for integral ring maps

Statement

Assume the Axiom of Choice.

Let f:AB be an integral ring map, and let pSpec(A) with kerfp. Then there exists a prime ideal qSpec(B) such that f1(q)=p.

Facts & Assumptions

Given: An integral ring map f:AB and a prime ideal pA containing kerf.

[L1]

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

[L2]

Integrality is preserved by localisation (Integrality and integral closure commute with localisation).

[L3]

In an integral extension, a prime upstairs is maximal exactly when its contraction is maximal (Under an integral extension, a prime is maximal if and only if its contraction is maximal).

[L5]

The quotient by a prime ideal is a domain (R/P is an integral domain if and only if P is a prime ideal).

[L6]

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

[L7]

Prime ideals of a localisation correspond exactly to primes disjoint from the denominator set (Prime ideals of a localization are exactly the primes disjoint from the denominator set).

[L8]

Assuming the Axiom of Choice, every proper ideal of a nonzero commutative ring is contained in a maximal ideal (In a nonzero commutative ring, every proper ideal is contained in a maximal ideal).

[L9]

A localisation is the zero ring exactly when 0 belongs to the denominator set (Equality, vanishing, and the kernel of the localisation map).

Proof

technique · direct
1.1

Let A:=A/kerf, let π:AA be the quotient map, and let p:=p/kerf. By [L6], prime ideals of A correspond to prime ideals of A containing kerf, so p is prime. The map f factors through an injective integral map f:AB, so it is enough to find a prime of B contracting to p and then pull it back through [L6].

L1L6given
2.1

Replace A by A and write again p for the chosen prime. Set S:=Ap. By [L5], A/p is a domain, so S contains no zero element of A; since AB is injective, 0S inside B as well. Hence [L9] shows that S1B is nonzero. By [L2], the map S1AS1B is integral.

L2L5L9step 1.1
3.1

By [L7], prime ideals of Ap=S1A correspond to prime ideals of A contained in p. Therefore every prime of Ap lies inside pAp, so pAp is the unique maximal ideal of Ap. By [L8], the nonzero ring S1B has a maximal ideal n. Then [L3] implies that nAp=pAp.

L3L7L8step 2.1
4.1

By [L7], the prime ideal n of S1B is S1q for a unique prime ideal q of B disjoint from S, and its contraction to A is the contraction of pAp, namely p. Therefore q lies over p. Pulling back through step 1.1 gives a prime of B lying over the original prime of A.

L7step 1.1step 3.1

Depends on

Used by

Dependency tree · two levels

31 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