ExampleConstruction: AI-adaptedVerification: 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.

A binary resultant detects a common root at infinity lost by naive dehomogenization

Example

Let $k$ be any field, let $F (X, Y) = Y$ be of nominated degree one and $G (X, Y) = X Y$ of nominated degree two, and let $K$ be an algebraic closure of $k$ . Then ${Res}_{1, 2} (F, G) = 0$ , because $F$ and $G$ both vanish at the point $[1 : 0]$ of $P^{1} (K)$ , whereas the dehomogenisations $F (T, 1) = 1$ and $G (T, 1) = T$ have no common affine root. The nominated degrees $1$ and $2$ are not reset after dehomogenisation.

Facts & Assumptions

Given: A field $k$ , the forms $F = Y \in k [X, Y]_{1}$ and $G = X Y \in k [X, Y]_{2}$ of nominated degrees $1$ and $2$ , and an algebraic closure $K$ of $k$ .

[L1]

For $d = 1, e = 2$ the Sylvester map is $(A, B) \mapsto A Y + B X Y$ from $k [X, Y]_{1} \oplus k [X, Y]_{0}$ to $k [X, Y]_{2}$ , with the $F$ -block basis $X, Y$ listed first and then the $G$ -block basis $1$ , and ${Res}_{1, 2} (F, G)$ is the determinant of this map in those bases (Sylvester resultant of two positive-degree binary forms, For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

[L2]

Over a field $k$ with algebraic closure $K$ , ${Res}_{d, e} (F, G) = 0$ if and only if $F$ and $G$ vanish together at some point of $P^{1} (K)$ (The binary Sylvester resultant detects a common geometric projective root, projective space points, An algebraic closure of a field).

[L3]

For a field $k$ , an algebraically closed extension $K$ , and homogeneous $F, G$ of nominated positive degrees $d, e$ , the common zeros in $P^{1} (K)$ are exactly the points $[a : 1]$ with $f (a) = g (a) = 0$ for $f (T) = F (T, 1)$ , $g (T) = G (T, 1)$ , together with the point $[1 : 0]$ when the coefficient of $X^{d}$ in $F$ and the coefficient of $X^{e}$ in $G$ both vanish (Scaling, specialization, and the affine and infinite charts of a binary resultant).

Verification

technique · direct

1.1

The Sylvester map has $Φ (X, 0) = X Y$ , $Φ (Y, 0) = Y^{2}$ and $Φ (0, 1) = X Y$ , so the first and the third column of its matrix are equal; the matrix is therefore singular and ${Res}_{1, 2} (F, G) = 0$ .

L1algebra

2.1

One has $F (1, 0) = 0$ and $G (1, 0) = 0$ , so $[1 : 0] \in P^{1} (K)$ is a common zero of $F$ and $G$ , in agreement with the vanishing of the resultant by [L2]; in the chart description of [L3] this is the extra point $[1 : 0]$ , because the coefficient of $X^{1}$ in $F = Y$ is $0$ and the coefficient of $X^{2}$ in $G = X Y$ is $0$ .

L2L3step 1.1

3.1

The dehomogenisations are $F (T, 1) = 1$ and $G (T, 1) = T$ , and a common affine root would satisfy $T = 0$ from $G (T, 1) = 0$ and $1 = 0$ from $F (T, 1) = 0$ , which is impossible in $k$ ; so there is no affine common root even though the resultant vanishes.

L3step 2.1algebra

4.1

Hence the vanishing of the resultant detects the common projective zero $[1 : 0]$ that naive affine dehomogenisation misses: the affinely dehomogenised forms $1$ and $T$ are coprime, and the nominated degrees $1$ and $2$ are still the degrees used in the matrix of step 1.1.

step 3.1given∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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

J. S. Milne, Algebraic Geometry v6.10, Proposition 7.27 boundary and Proposition 7.28, pp. 166-167 (standard reference, not scraped)