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 be nonzero homogeneous forms of positive degrees over the algebraically closed field with no common factor, and suppose the point lies on neither nor ; equivalently the coefficient of in and the coefficient of in are nonzero constants, so that and have exact degrees for every . Then is a nonzero form of degree , and for one has if and only if there is with . Consequently the projections of the common points of and are exactly the projective zeros of the resultant; over each such zero the fibre of common points is finite, of size at most when counted without multiplicity. In particular is finite.
Facts & Assumptions
Given: An algebraically closed field , nonzero forms of positive degrees with no common factor and with nonzero constant - and -coefficients, , , and the resultant of Resultant of two plane forms, viewed in one variable with .
is a unique factorisation domain and 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.
is the determinant of the Sylvester map on forms of nominated degrees, and for its value is the Sylvester resultant of the specialisations of nominated degrees 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 over an algebraically closed field The binary Sylvester resultant detects a common geometric projective root, projective space points.
A nonzero polynomial of degree over an integral domain has at most distinct roots A nonzero polynomial of degree over an integral domain has at most distinct roots. Points of have the form , and the points with are exactly those lying in the two charts , whose union contains neither-curve hypothesis excluded only projective space points, standard projective opens are affine spaces.
Proof
Let and regard . They have no common factor of positive -degree in : if a polynomial of positive degree divided both, then clearing denominators and applying Gauss's lemma to the primitive parts produces a nonconstant common divisor of and in , contradicting the hypothesis.
For each the specialised polynomials have exact degrees and , and if and only if they have a common root in : the specialisation rule identifies the value with , and for binary forms of nominated positive degrees over the algebraically closed field the resultant vanishes exactly when a common zero in exists. The point cannot be a common zero, since both specialised top coefficients are nonzero by hypothesis; thus the projective common zero is on the chart and is exactly a common finite root.
is a nonzero form of degree . If it were the zero polynomial, then over the fraction field the Sylvester matrix would be singular, so there would be , not both zero, with , and ; then in , and since and are coprime there by step 1.1 and (the top coefficient of in 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 in .
Let be the zero set of in . By step 1.2, for the point lies in exactly when for some ; since , every point of has , so the projection has image exactly . By step 2.1 the resultant is a nonzero form of degree , so is finite, of at most points: after possibly renaming the variables its dehomogenisation is a nonzero polynomial of degree at most , whose roots give the points of with first coordinate nonzero, If the remaining point is a zero, the coefficient of vanishes, so the dehomogenisation has degree at most ; hence including that point still gives at most zeros. For the fibre consists of common roots of and , hence of roots of the nonzero polynomial of degree and also of of degree , so it has at most points. Therefore is finite with the asserted fibre bound, and its projections are exactly the zeros of the nonzero resultant.
Depends on
- homogeneous polynomial and homogeneous ideal
- Plane projective curves and their components
- Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree
- projective space points
- Resultant of two plane forms, viewed in one variable
- Sylvester resultant of two positive-degree binary forms
- Unique factorisation domain
- Scaling, specialization, and the affine and infinite charts of a binary resultant
- Every finite-variable polynomial ring over a field is a UFD, with prime irreducibles and principal height-one primes
- Gauss lemma over a UFD
- standard projective opens are affine spaces
- The binary Sylvester resultant detects a common geometric projective root
- projective zariski topology
- A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots
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
- Michael Artin, MIT 18.721 Notes for a Course in Algebraic Geometry (January 26, 2022 version), Chapter 1 (standard reference, not scraped)
- William Fulton, Algebraic Curves: An Introduction to Algebraic Geometry (2008 electronic edition; Internet Archive copy of the author's PDF) (standard reference, not scraped)