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.

Lying over in k[t^2, t^3] subset k[t]

Example

Let $A : = k [t^{2}, t^{3}] \subseteq B : = k [t]$ , where $k$ is a field. Then the zero prime of $A$ is the contraction of $(0) \subseteq B$ , and the cusp maximal ideal $(t^{2}, t^{3}) \subseteq A$ is the contraction of $(t) \subseteq B$ .

Facts & Assumptions

Given: A field $k$ , the inclusion $A : = k [t^{2}, t^{3}] \subseteq B : = k [t]$ , and the theorem of lying over (Lying over for integral ring maps).

[L1]

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

Verification

technique · direct

1.1L1givenalgebra

The element $t \in B$ satisfies the monic equation $T^{2} - t^{2} = 0$ with coefficient $t^{2} \in A$ , so $B$ is integral over $A$ . Since both $A$ and $B$ are subrings of the domain $k [t]$ , the zero prime of $B$ contracts to the zero prime of $A$ .

2.1step 1.1givenalgebra

The quotient $B / (t)$ is $k$ , and the image of $A$ in it is also $k$ because both $t^{2}$ and $t^{3}$ vanish. Hence $(t) \cap A = (t^{2}, t^{3})$ . In particular, the cusp maximal ideal of $A$ has a prime above it in $B$ , namely $(t)$ .

3.1L1step 1.1step 2.1∎

This is the concrete cusp-ring instance of lying over: the two natural base primes $(0)$ and $(t^{2}, t^{3})$ are realised upstairs by $(0)$ and $(t)$ .

Depends on

Lying over for integral ring maps

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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., Example (10.34)(4) (standard reference, not scraped)
Melvin Hochster, Introduction to Commutative Algebra, Ch. 3 (standard reference, not scraped)