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

Two plane projective curves meet

Statement

Assume the Axiom of Choice, inherited from the cited local-length, smoothness or Bezout suppliers.

Let $C, D$ be plane projective curves of positive degrees over the algebraically closed field $k$ . If $C$ and $D$ have no common component they meet, and their local intersection multiplicities sum to $d e \geq 1$ ; if they share a component they meet along that component. In all cases $C \cap D \neq \emptyset$ .

Facts & Assumptions

Given: AC The Axiom of Choice, plane projective curves $C = V (F)$ of degree $d \geq 1$ and $D = V (G)$ of degree $e \geq 1$ over the algebraically closed field $k$ .

[F1]

If $C, D$ have no common component, then $C \cap D$ is nonempty and finite Curves without a common component meet finitely often, and $\sum_{p \in C \cap D} I_{p} (C, D) = d e$ Bezout's theorem for plane projective curves. Each summand $I_{p}$ is positive exactly at the points of $C \cap D$ and nonnegative everywhere Symmetry, additivity and local nature of intersection multiplicity.

[F2]

Every plane projective curve is nonempty, and if $C, D$ share an irreducible component $E$ , then $E \subseteq C \cap D$ Plane projective curves and their components. In the no-common-component case, the intersection scheme is nonempty and zero-dimensional A plane intersection with no common component is nonempty and zero-dimensional, A zero-dimensional projective scheme has finitely many closed points with finite-dimensional local rings.

Proof

1.1F1algebra

If $C$ and $D$ have no common component: by [F1] the multiplicities form a finite sum of nonnegative integers equal to $d e \geq 1$ , so at least one point $p$ has $I_{p} (C, D) \geq 1$ , which by [F1] happens exactly when $p \in C \cap D$ . Hence $C \cap D \neq \emptyset$ and the multiplicities sum to $d e$ .

1.2F2given

If $C$ and $D$ share a component $E$ : by [F2] the component is nonempty and contained in $C \cap D$ , so $C \cap D \neq \emptyset$ ; in this case the intersection is infinite along $E$ and the Bezout sum is not finite.

2.1step 1.1step 1.2∎

The two cases exhaust the possibilities for two plane curves, so in all cases $C \cap D \neq \emptyset$ , and in the no-common-component case the sum of the local multiplicities is $d e \geq 1$ .

Depends on

Used by

Dependency tree · two levels

74 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)
Michael Artin, MIT 18.721 Notes for a Course in Algebraic Geometry (January 26, 2022 version), Chapter 1 (standard reference, not scraped)