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.

Invariance of the Bezout sum under projective coordinate changes

Statement

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

Let $C, D$ be plane projective curves of degrees $d, e$ over the algebraically closed field $k$ with no common component, and let $A \in {P G L}_{3} (k)$ be a projective change of coordinates. Then $A (C)$ and $A (D)$ are plane curves of the same degrees with no common component and

$\sum_{p \in C \cap D} I_{p} (C, D) = \sum_{q \in A (C) \cap A (D)} I_{q} (A (C), A (D)) .$

More precisely $I_{p} (C, D) = I_{A (p)} (A (C), A (D))$ for every $p$ , so any convenient coordinate system may be used to compute the sum.

Facts & Assumptions

Given: AC The Axiom of Choice, plane projective curves $C = V (F)$ of degree $d$ and $D = V (G)$ of degree $e$ over the algebraically closed field $k$ with no common component, and a projective change of coordinates $A \in {P G L}_{3} (k)$ .

[F1]

$A$ is an automorphism of $P^{2}$ : it is a morphism of projective spaces given by homogeneous coordinates of degree one, with inverse of the same kind, and it carries closed sets to closed sets and curves of degree $f$ to curves of degree $f$ morphism to projective space homogeneous coordinates, projective coordinate morphisms well defined, Plane projective curves and their components. It maps $C \cap D$ bijectively onto $A (C) \cap A (D)$ , and a common component to a common component, so $A (C), A (D)$ still have no common component.

[F2]

Local intersection multiplicities transform by the induced isomorphism of local rings: $I_{p} (C, D) = I_{A (p)} (A (C), A (D))$ for every $p \in C \cap D$ , and the values are finite exactly together Invariance of the local intersection multiplicity.

Proof

1.1F1given

By [F1] the curves $A (C), A (D)$ have the same degrees $d, e$ and no common component, and $p \mapsto A (p)$ is a bijection $C \cap D \to A (C) \cap A (D)$ ; the intersection sets are finite by the no-common-component hypothesis.

1.2F2given

For every $p \in C \cap D$ the local multiplicities agree, $I_{p} (C, D) = I_{A (p)} (A (C), A (D))$ , by [F2].

2.1step 1.1step 1.2algebra∎

Summing the equality of step 1.2 over the finite set $C \cap D$ and using the bijection of step 1.1 gives $\sum_{p \in C \cap D} I_{p} (C, D) = \sum_{q \in A (C) \cap A (D)} I_{q} (A (C), A (D)),$ so the Bezout sum is invariant and may be computed in any system of projective coordinates.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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)