Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Going down holds for integral extensions over integrally closed domains

Statement

Assume the Axiom of Choice.

Let A⊆B be an integral extension of domains, and assume that A is integrally closed. If p0⊆p1 are prime ideals of A and q1 is a prime ideal of B with q1∩A=p1, then there exists a prime ideal q0⊆q1 of B such that q0∩A=p0.

Facts & Assumptions

Given: An integral extension of domains A⊆B, an integrally closed base ring A, primes p0⊆p1 of A, and a prime q1 of B over p1.

[L1]

In an integral extension, every element of the upper ring satisfies a monic equation over the lower ring (Integral ring maps and integral extensions).

[L2]

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).

[L3]

Assuming the Axiom of Choice, an ideal disjoint from a multiplicative set lies inside a prime ideal disjoint from that set (A prime containing an ideal and avoiding a multiplicative set).

[L4]

If a monic polynomial in A[T] factors in Frac⁡(A)[T] as (T−a)h(T) with a∈Frac⁡(A) and A integrally closed, then h(T) has coefficients in A (Minimal polynomials of integral elements over an integrally closed domain have coefficients in the domain).

[L5]

A subalgebra generated by finitely many integral elements is module-finite (A subalgebra generated by finitely many integral elements is module-finite).

[L6]

For a square matrix over a commutative ring, Aadj⁡(A)=det⁡(A)I (For every positive-sized square matrix over a commutative ring, Aadj⁡(A)=adj⁡(A)A=det⁡(A)I).

Proof

technique · direct
1.1L2given

Let S:=B∖q1. By [L2], primes of BS=Bq1 correspond exactly to primes of B contained in q1. It is therefore enough to find a prime ideal of Bq1 whose contraction to A is p0.

2.1L1step 1.1given

Let b∈A∩p0Bq1. Write b=y/s with y∈p0B and s∈B∖q1. Choose a representation y=∑j=1majbj with aj∈p0 and bj∈B. Because the extension is integral, [L1] says that each bj and s is integral over A.

3.1L5L6step 2.1givenalgebra

Let M:=A[s,b1,…,bm]. By [L5], M is module-finite over A. Since y=∑ajbj lies in p0B, multiplication by y sends M into p0M: for m′∈M, one has ym′=∑jaj(bjm′) and each bjm′ again lies in M. Choose A-generators m1,…,mr of M. Then there are coefficients cij∈p0 with ymj=∑icijmi. Writing C=(cij), the adjugate identity [L6] applied to yIr−C yields a monic polynomial P(T)=Tr+cr−1Tr−1+⋯+c0 with every ci∈p0 and P(y)=0.

4.1L4step 3.1algebra

Suppose b∉p0. Let K:=Frac⁡(A). Since s is integral over A, [L4] gives a monic minimal polynomial ms(T)=Td+dd−1Td−1+⋯+d0 with coefficients in A. Because y=bs and P(y)=0, dividing by br in K[T] gives a monic polynomial Q(T)=Tr+cr−1bTr−1+⋯+c0br with coefficients in the localisation Ap0 and satisfying Q(s)=0. Since ms is monic and divides every polynomial over K that vanishes at s, it divides Q in K[T], hence also in Ap0[T].

5.1step 4.1algebra

Reduce that divisibility relation modulo p0Ap0. The image of Q is Tr, so the image of ms is a monic divisor of Tr in Frac⁡(A/p0)[T]. Therefore ms‾(T)=Td, and every coefficient di lies in p0.

6.1step 5.1givenalgebra

The relation ms(s)=0 now shows that sd∈p0B⊆q1. Because q1 is prime, this forces s∈q1, contradicting the choice of s. Hence b∈p0. Therefore A∩p0Bq1=p0.

7.1L3step 6.1given

Let C:=Bq1/p0Bq1. Step 6.1 identifies A/p0 with a subring of C; because A/p0 is a domain, its nonzero elements form a multiplicative subset T⊆C. The zero ideal of C is disjoint from T, so [L3] gives a prime ideal n of C disjoint from T. Its inverse image q0′ in Bq1 contains p0Bq1, and the disjointness from T says exactly that q0′∩A=p0.

8.1L2step 7.1∎

By [L2], the prime q0′ of Bq1 is the localisation of a unique prime ideal q0⊆q1 of B. Its contraction to A is p0 by step 7.1. Therefore q0 is the required prime below q1.

Depends on

Used by

Dependency tree · two levels

26 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