Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

An integral domain extension can fail going down when the base is not normal

Example

Let K be a field, let

R:=K[x(1x),y,xy]S:=K[x,y],

let

P0:=(x(1x),xy)R,P:=(x(1x),y,xy)R,

and let

Q:=(1x,y)S.

Then RS is an integral extension of domains, P0P is a strict prime chain in R, Q lies over P, and there is no prime ideal Q0Q of S lying over P0. So going down fails although both rings are domains.

Facts & Assumptions

Given: A field K, the rings R:=K[x(1x),y,xy]S:=K[x,y], the ideals P0P in R, and the prime Q=(1x,y) in S.

[L1]

Assuming the Axiom of Choice, going down holds for integral extensions over integrally closed domains (Going down holds for integral extensions over integrally closed domains).

Verification

technique · direct
1.1

The ring S is a domain, and R is a subring of it, so R is also a domain. Moreover x satisfies the monic equation T2T+x(1x)=0 with coefficient x(1x)R, and S=R[x] because yR already. Hence S is integral over R.

L1givenalgebra
2.1

The ideals P0 and P are prime because they are contractions of the prime ideals (x) and (x,y) of S, and they are distinct because yPP0. The ideal Q=(1x,y) is prime in S, and its contraction to R is P, since mod Q one has x=1 and y=0, so x(1x), y, and xy all vanish.

step 1.1givenalgebra
2.2

The base ring is not integrally closed: the element xS is integral over R by step 1.1, but xR. Indeed, if xR, then setting y=0 would express x as a polynomial in x(1x); evaluating at x=0 and x=1 would then give the same value on both inputs, impossible because x takes the values 0 and 1.

L1step 1.1givenalgebra
3.1

Suppose Q0Q were a prime ideal of S with Q0R=P0. Because Q=(1x,y) does not contain x, neither does Q0. But x(1x)P0Q0 and xyP0Q0, so primality of Q0 and xQ0 force 1xQ0 and yQ0. Hence Q=(1x,y)Q0, and therefore Q0=Q. This contradicts Q0R=P0 because step 2.1 showed QR=PP0.

step 2.1givenalgebra
4.1

Thus the integral extension of domains RS has a prime chain P0P and a prime Q over P with no prime below Q lying over P0. So the normality hypothesis in [L1] is essential.

L1step 2.2step 3.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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