TheoremStatement: 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.

Bezout's theorem for plane projective curves

Statement

Assume the Axiom of Choice. Let $C = V (F)$ and $D = V (G)$ be plane projective curves of degrees $d, e \geq 1$ over the algebraically closed field $k$ , with no common component. Then

$\sum_{p \in C \cap D} I_{p} (C, D) = d e,$

a finite sum over the finitely many intersection points, each term the local intersection multiplicity of the two curves.

Facts & Assumptions

Given: AC, plane projective curves $C = V (F)$ , $D = V (G)$ of degrees $d, e \geq 1$ over the algebraically closed field $k$ with no common component, and $X = Proj (k [x_{0}, x_{1}, x_{2}] / (F, G))$ Projective scheme of a homogeneous quotient and its standard affine charts.

[F1]

$C \cap D$ is nonempty and finite, and the points of $X$ correspond to the points of $C \cap D$ Curves without a common component meet finitely often.

[F2]

The total length of $X$ equals the degree product: ${len}_{k} (X) = d e$ Global length of a plane complete intersection equals the degree product.

[F3]

The total length of $X$ equals the sum of the local intersection multiplicities: ${len}_{k} (X) = \sum_{p \in C \cap D} I_{p} (C, D)$ Global intersection length is the sum of the local multiplicities, with every term finite by the no-common-component hypothesis Local intersection multiplicity of two plane curves.

Proof

1.1F2F3given

By [F2] the global length of $X$ is ${len}_{k} (X) = d e$ ; by [F3] the same global length equals the finite sum of the local multiplicities $\sum_{p \in C \cap D} I_{p} (C, D)$ over the finitely many intersection points, each summand finite.

2.1step 1.1F1F2F3∎

Equating the two computations of the same number ${len}_{k} (X)$ gives $\sum_{p \in C \cap D} I_{p} (C, D) = d e$ , which is Bezout's identity; finiteness and nonemptiness of the intersection were recorded in [F1] and are used to make the sum meaningful.

Depends on

Used by

A line meets a degree-d curve in d points counted with multiplicity Corollary
The component-counting obstruction template for incidence arguments Corollary
Two plane projective curves meet Corollary
A common component makes the intersection sum infinite Counterexample
Bezout fails on the affine plane because points at infinity are missing Counterexample
Bezout needs algebraic closure: an imaginary conic has no real point Counterexample
Counting distinct points is not enough: tangent contact Counterexample
Lines through a node and its two branches Example
Two transverse cubics meet in nine points Example
Invariance of the Bezout sum under projective coordinate changes Lemma
Why Bezout needs projectivity, algebraic closure and multiplicity Remark
Curves sharing too many points share a component Theorem

Dependency tree · two levels

57 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

William Fulton, Algebraic Curves: An Introduction to Algebraic Geometry (2008 electronic edition; Internet Archive copy of the author's PDF) (standard reference, not scraped)
MIT 18.725 Algebraic Geometry (Fall 2015) lecture notes, consolidated (standard reference, not scraped)