Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)
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.

The resultant detects finitely many common projective points

Statement

Let F,G∈k[x0,x1,x2] be nonzero homogeneous forms of positive degrees d,e over the algebraically closed field k with no common factor, and suppose the point [0:0:1] lies on neither C=V(F) nor D=V(G); equivalently the coefficient of x2d in F and the coefficient of x2e in G are nonzero constants, so that F(a,b,x2) and G(a,b,x2) have exact degrees d,e for every (a,b)≠(0,0). Then Res⁡x2(F,G)∈k[x0,x1] is a nonzero form of degree de, and for (a,b)≠(0,0) one has Res⁡x2(F,G)(a,b)=0 if and only if there is c∈k with [a:b:c]∈C∩D. Consequently the projections (x0:x1) of the common points of C and D are exactly the projective zeros of the resultant; over each such zero the fibre of common points is finite, of size at most min⁡(d,e) when counted without multiplicity. In particular C∩D is finite.

Facts & Assumptions

Given: An algebraically closed field k, nonzero forms F,G∈k[x0,x1,x2] of positive degrees d,e with no common factor and with nonzero constant x2d- and x2e-coefficients, C=V(F), D=V(G), and the resultant Res⁡x2(F,G)∈k[x0,x1] of Resultant of two plane forms, viewed in one variable with R=k[x0,x1].

[F1]

R=k[x0,x1] is a unique factorisation domain and R[x2]=k[x0,x1,x2] is a unique factorisation domain in which every irreducible is prime Every finite-variable polynomial ring over a field is a UFD, with prime irreducibles and principal height-one primes, Unique factorisation domain. In a UFD, an element of a polynomial ring that is primitive of positive degree is irreducible over the ring exactly when it is irreducible over the fraction field Gauss lemma over a UFD.

[F2]

Res⁡x2(F,G) is the determinant of the Sylvester map (A,B)↦AF+BG on forms of nominated degrees, and for (a,b)≠(0,0) its value is the Sylvester resultant of the specialisations of nominated degrees d,e Resultant of two plane forms, viewed in one variable, Sylvester resultant of two positive-degree binary forms, Scaling, specialization, and the affine and infinite charts of a binary resultant. The Sylvester resultant of two binary forms of nominated positive degrees vanishes exactly when the two forms have a common zero in P1 over an algebraically closed field The binary Sylvester resultant detects a common geometric projective root, projective space points.

[F3]

A nonzero polynomial of degree n over an integral domain has at most n distinct roots A nonzero polynomial of degree n over an integral domain has at most n distinct roots. Points of P2 have the form [a:b:c], and the points with (a,b)≠(0,0) are exactly those lying in the two charts D+(x0)∪D+(x1), whose union contains neither-curve hypothesis excluded only [0:0:1] projective space points, standard projective opens are affine spaces.

Proof

1.1F1givenalgebra

Let K=Frac⁡(R) and regard F,G∈K[x2]. They have no common factor of positive x2-degree in K[x2]: if a polynomial H∈K[x2] of positive degree divided both, then clearing denominators and applying Gauss's lemma to the primitive parts produces a nonconstant common divisor of F and G in R[x2]=k[x0,x1,x2], contradicting the hypothesis.

1.2F2F3given

For each (a,b)≠(0,0) the specialised polynomials F(a,b,x2),G(a,b,x2)∈k[x2] have exact degrees d and e, and Res⁡x2(F,G)(a,b)=0 if and only if they have a common root in k: the specialisation rule identifies the value with Res⁡d,e(F(a,b,x2),G(a,b,x2)), and for binary forms of nominated positive degrees over the algebraically closed field k the resultant vanishes exactly when a common zero in Pk1 exists. The point [1:0] cannot be a common zero, since both specialised top coefficients are nonzero by hypothesis; thus the projective common zero is on the chart [t:1] and is exactly a common finite root.

2.1step 1.1F2givenalgebra

Res⁡x2(F,G) is a nonzero form of degree de. If it were the zero polynomial, then over the fraction field K the Sylvester matrix would be singular, so there would be A,B∈K[x2], not both zero, with deg⁡B≤d−1, deg⁡A≤e−1 and AF+BG=0; then F∣BG in K[x2], and since F and G are coprime there by step 1.1 and deg⁡B<d=deg⁡F (the top coefficient of F in x2 is a nonzero constant), this is impossible. Hence the determinant is nonzero, and the determinant-weight calculation in Resultant of two plane forms, viewed in one variable gives its total degree de in x0,x1.

3.1step 1.2step 2.1F3given∎

Let Z be the zero set of Res⁡x2(F,G) in P1. By step 1.2, for (a,b)≠(0,0) the point [a:b] lies in Z exactly when [a:b:c]∈C∩D for some c∈k; since [0:0:1]∉C∪D, every point of C∩D has (a,b)≠(0,0), so the projection π:C∩D→P1 has image exactly Z. By step 2.1 the resultant is a nonzero form of degree de, so Z is finite, of at most de points: after possibly renaming the variables its dehomogenisation Res⁡(1,t) is a nonzero polynomial of degree at most de, whose roots give the points of Z with first coordinate nonzero, If the remaining point [0:1] is a zero, the coefficient of x1de vanishes, so the dehomogenisation has degree at most de−1; hence including that point still gives at most de zeros. For [a:b]∈Z the fibre consists of common roots of F(a,b,x2) and G(a,b,x2), hence of roots of the nonzero polynomial F(a,b,x2) of degree d and also of G(a,b,x2) of degree e, so it has at most min⁡(d,e) points. Therefore C∩D is finite with the asserted fibre bound, and its projections are exactly the zeros of the nonzero resultant.

Depends on

Used by

Dependency tree · two levels

53 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