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

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

Example

Let K be a field, let R:=K[x(1−x),y,xy]⊆S:=K[x,y], let P0:=(x(1−x),xy)R,P:=(x(1−x),y,xy)R, and let Q:=(1−x,y)S. Then R⊆S is an integral extension of domains, P0⊊P is a strict prime chain in R, Q lies over P, and there is no prime ideal Q0⊆Q 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(1−x),y,xy]⊆S:=K[x,y], the ideals P0⊊P in R, and the prime Q=(1−x,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.1L1givenalgebra

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 T2−T+x(1−x)=0 with coefficient x(1−x)∈R, and S=R[x] because y∈R already. Hence S is integral over R.

2.1step 1.1givenalgebra

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 y∈P∖P0. The ideal Q=(1−x,y) is prime in S, and its contraction to R is P, since mod Q one has x=1 and y=0, so x(1−x), y, and xy all vanish.

2.2L1step 1.1givenalgebra

The base ring is not integrally closed: the element x∈S is integral over R by step 1.1, but x∉R. Indeed, if x∈R, then setting y=0 would express x as a polynomial in x(1−x); 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.

3.1step 2.1givenalgebra

Suppose Q0⊆Q were a prime ideal of S with Q0∩R=P0. Because Q=(1−x,y) does not contain x, neither does Q0. But x(1−x)∈P0⊆Q0 and xy∈P0⊆Q0, so primality of Q0 and x∉Q0 force 1−x∈Q0 and y∈Q0. Hence Q=(1−x,y)⊆Q0, and therefore Q0=Q. This contradicts Q0∩R=P0 because step 2.1 showed Q∩R=P≠P0.

4.1L1step 2.2step 3.1∎

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

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