CorollaryStatement: Literature-sourcedProof: 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.

Algebraic Bezout formula as a sum of local scheme lengths

Statement

Assume the Axiom of Choice. Let $k$ be a field and let $F, G \in k [x_{0}, x_{1}, x_{2}]$ be nonzero homogeneous forms of positive degrees $d$ and $e$ with no common nonconstant factor, and put $X = Proj (k [x_{0}, x_{1}, x_{2}] / (F, G))$ . Then $\sum_{x \in X} ℓ_{O_{X, x}} (O_{X, x}) [κ (x) : k] = d e,$ a finite sum of local lengths weighted by residue degrees. If moreover $k$ is algebraically closed, then $[κ (x) : k] = 1$ for every $x \in X$ , and therefore $\sum_{x \in X} ℓ_{O_{X, x}} (O_{X, x}) = d e$ .

This is the algebraic length statement supplied to the later plane-curve page. It asserts nothing about local equations other than the dehomogenised $F, G$ , nothing about invariance under other choices of equations for the same local curve, and no geometric intersection formulation.

Facts & Assumptions

Given: The Axiom of Choice, a field $k$ , nonzero homogeneous forms $F, G \in k [x_{0}, x_{1}, x_{2}]$ of positive degrees $d, e$ with no common nonconstant factor, the standard graded quotient $S = k [x_{0}, x_{1}, x_{2}] / (F, G)$ , and $X = Proj S$ .

[L1]

Assume AC. $X$ is nonempty and finite, every chart ring is zero or of Krull dimension $0$ , and the total length satisfies ${len}_{k} (X) = d e$ (Two coprime projective plane forms meet in total length equal to their degree product).

[L2]

Assume AC. For a zero-dimensional $X$ the total length is the finite sum ${len}_{k} (X) = \sum_{x \in X} ℓ_{O_{X, x}} (O_{X, x}) [κ (x) : k]$ over the finitely many points, each local ring $O_{X, x}$ being a finite-dimensional local $k$ -algebra of finite length and each residue field $κ (x)$ being finite over $k$ (Total length of a zero-dimensional projective scheme, A zero-dimensional projective scheme has finitely many closed points with finite-dimensional local rings, The residue field at a point of an affine scheme, The degree $[K : F] = \dim_{F} K$ of a finite field extension).

[L3]

A field $F$ is algebraically closed exactly when it has no nontrivial finite extension; equivalently $F$ is algebraically closed if and only if every finite extension $F \subseteq K$ satisfies $K = F$ (An algebraically closed field: every nonconstant polynomial has a root in the field, A field is algebraically closed exactly when every nonconstant polynomial splits, equivalently when it has no nontrivial finite extension).

[L4]

Assume AC (declared for consumers of this corollary). The Axiom of Choice

Proof

technique · direct

1.1

By [L1] the scheme $X$ is finite, nonempty and has total length ${len}_{k} (X) = d e$ .

1.2

By [L2] the total length of $X$ is the finite weighted sum ${len}_{k} (X) = \sum_{x \in X} ℓ_{O_{X, x}} (O_{X, x}) [κ (x) : k]$ over the finitely many points of $X$ , with every residue degree $[κ (x) : k]$ finite over $k$ .

2.1

Combining steps 1.1 and 1.2 gives $\sum_{x \in X} ℓ_{O_{X, x}} (O_{X, x}) [κ (x) : k] = {len}_{k} (X) = d e$ , which is the displayed formula.

step 1.1step 1.2

3.1

Now assume that $k$ is algebraically closed; by step 1.2 each $κ (x)$ is a finite extension field of $k$ , so [L3] gives $κ (x) = k$ and hence $[κ (x) : k] = 1$ for every $x \in X$ ; substituting into step 2.1 gives $\sum_{x \in X} ℓ_{O_{X, x}} (O_{X, x}) = d e$ .

L3step 1.2step 2.1

4.1

The weighted sum equals $d e$ over an arbitrary field by step 2.1, and over an algebraically closed field it collapses to the unweighted sum of local lengths by step 3.1; the Axiom of Choice is inherited from [L1] and [L2] and is declared here for users of the corollary as the standing assumption [L4].

L1L2L4step 2.1step 3.1given∎

Depends on

Used by

A tangent line and conic have one intersection point of local length two Example

Dependency tree · two levels

58 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

A. Gathmann, Algebraic Geometry class notes (2002), Example 6.2.2, p. 96 (standard reference, not scraped)
J. S. Milne, Algebraic Geometry v6.10, Remark 6.38, p. 153 (standard reference, not scraped)