Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-27
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.

Normalization of a nodal affine plane curve

Statement

Let k be a field of characteristic different from 2. Then the quotient A:=k[x,y]/(y2−x2(x+1)) is an integral domain, the substitution x↦t2−1, y↦t(t2−1) induces an injective k-algebra homomorphism A↪k[t], and the integral closure of A in Frac⁡(A)=k(t) is exactly k[t]=A+At, a finite A-module. Under the resulting parametrisation the origin (0,0) has exactly the two preimages t=1 and t=−1.

Facts & Assumptions

Given: a field k with char⁡k≠2, the polynomial ring k[x,y], the ideal P=(y2−x2(x+1)), the quotient A=k[x,y]/P, and the substitution σ:k[x,y]→k[t], σ(x)=t2−1, σ(y)=t(t2−1).

[L1]

A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring, so a homomorphism killing P induces a unique homomorphism out of A (A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring, The quotient ring R/I with (r+I)(s+I)=rs+I, Evaluation and roots of a polynomial in a commutative target ring).

[L2]

Division by a monic polynomial over a commutative ring R: for monic g∈R[s] and any f∈R[s] there are unique q,r with f=qg+r and r=0 or deg⁡r<deg⁡g (Division by a monic polynomial over a commutative ring, Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[L4]

For a field F and d≥0 the ring F[y1,…,yd] is an integrally closed domain (Finite-variable polynomial algebras over fields are integrally closed, Integral closure in an extension ring and integrally closed domains).

[L5]

Over a nonzero commutative ring, for nonzero polynomials f,g, the coefficient of sdeg⁡f+deg⁡g in fg is the product of the leading coefficients, and sm has leading coefficient 1 with degree m (Degree inequalities for sums and products over a commutative ring, Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[L6]

Integrality means being a root of a monic polynomial over the base; integrality is transitive along domain inclusions; integral elements form a subring; an integrally closed domain contains the integral elements of its fraction field (Integral elements over a commutative ring and algebraic integers, Integral extensions are transitive, Integral elements over a nonzero base ring form a subring, Integral closure in an extension ring and integrally closed domains).

Proof

technique · direct
1.1

The substitution σ kills P: σ(y)2−σ(x)2(σ(x)+1)=t2(t2−1)2−(t2−1)2t2=0, because σ(x)+1=t2 and σ(y)=t(t2−1). By [L1] it therefore induces a unique k-algebra homomorphism φ:A→k[t] with φ(xˉ)=t2−1 and φ(yˉ)=t(t2−1), where xˉ,yˉ are the classes of x,y.

L1given
1.2

φ is injective. By [L2], applied in the polynomial ring (k[x])[y] to the monic polynomial y2−x2(x+1) of degree 2, every element of A has a unique representative a(x)+b(x)y with a,b∈k[x]; hence it suffices to show that φ(a+by)=a(t2−1)+t(t2−1)b(t2−1)=0 forces a=b=0. The first summand is a polynomial in t2 and the second is t times a polynomial in t2, so comparing the coefficients of t2m and of t2m+1 in the sum gives a(t2−1)=0 and (t2−1)b(t2−1)=0 separately. For a polynomial c=∑m≤Mcmsm with cM≠0, the value c(t2−1)=∑mcm(t2−1)m has coefficient cM at t2M by [L5], since (t2−1)m is monic of degree 2m and all lower terms have degrees <2M; hence c(t2−1)≠0. Applying this to c=a gives a=0. Since k[t] is a domain by [L3] and t2−1≠0 (it is monic of degree 2), (t2−1)b(t2−1)=0 forces b(t2−1)=0, and the same argument gives b=0. So φ is injective, and A is a domain, a k-subalgebra of k[t].

L2L3L5given
2.1

In Frac⁡(A) one has φ(yˉ)=t φ(xˉ) with φ(xˉ)=t2−1≠0, so t=yˉ/xˉ∈Frac⁡(A); hence k[t]⊆Frac⁡(A) and k(t)=Frac⁡(k[t])⊆Frac⁡(A) by [L3], while A⊆k[t] gives the reverse inclusion, so Frac⁡(A)=k(t). Moreover φ(xˉ)+1=t2, so t is a root of the monic polynomial T2−(xˉ+1)∈A[T] and is integral over A by [L6]; and k[t]=A+At, because t2=xˉ+1∈A reduces all exponents modulo 2, so k[t] is a finite A-module and every element of k[t] is integral over A.

L3L6step 1.2
3.1

If z∈k(t)=Frac⁡(A) is integral over A, then a monic equation for z over A has coefficients in A⊆k[t], so z is integral over k[t]; since k[t] is integrally closed in k(t) by [L4] and [L3], z∈k[t]. With step 2.1 this identifies the integral closure of A in Frac⁡(A) with k[t]=A+At, a finite A-module.

L3L4L6step 2.1
4.1

The parametrisation: a point of the curve with xˉ=0 has yˉ2=0, so yˉ=0 in the field k; thus the origin is the unique point with both coordinates zero. Under the parametrisation x=t2−1, y=t(t2−1) the condition x=0 is t2=1, that is t2−1=(t−1)(t+1)=0, so t=1 or t=−1 by [L3] (a product of two elements of the field k vanishes only if one factor does); these two values are distinct because char⁡k≠2 gives 1≠−1, and both give y=t(t2−1)=0. Hence the origin has exactly the two preimages t=1 and t=−1; the hypothesis char⁡k≠2 is used here, since in characteristic 2 the two values coincide.

L3step 1.2given∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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