Bézout's theorem

AbbreviationProjective space#✓fully proved

For a division ring \(K\) and \(n \in \mathbb{N}\), the projective space \(\mathbb{P}^n(K)\) is the projectivization of \(K^{n+1}\): the set of nonzero vectors of \(K^{n+1}\) modulo multiplication by nonzero scalars, equivalently the lines through the origin.

abbrev ProjSpace (K : Type*) [DivisionRing K] (n : ℕ) :=
  ℙ K (Fin (n + 1) → K)

Used by 5

Used byAffine coordinates of a projective point · Bézout's theorem (with multiplicity) · Chart index of a projective point · Intersection multiplicity at a projective point · Projective vanishing set

DefinitionProjective vanishing set#✓fully proved

For a field \(K\) and a polynomial \(f \in K[X_0, \dots, X_n]\), the vanishing set of \(f\) is the set of points \(p \in \mathbb{P}^n(K)\) such that \(f(v) = 0\), where \(v \in K^{n+1} \setminus \{0\}\) is the chosen representative of \(p\).

When \(f\) is homogeneous of degree \(d\), \(f(\lambda v) = \lambda^d f(v)\), so this set does not depend on the choice of representatives.

def vanishingSet {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) :
    Set (ProjSpace K n) :=
  {p | MvPolynomial.eval (Projectivization.rep p) f = 0}

Uses 1 · Used by 1

Statement usesProjective space

Used byBézout's theorem (with multiplicity)

DefinitionChart index of a projective point#✓fully proved

For a field \(K\) and a point \(p \in \mathbb{P}^n(K)\) with chosen representative \(v = (v_0, \dots, v_n) \in K^{n+1} \setminus \{0\}\), the chart index of \(p\) is a fixed choice of an index \(i \in \{0, \dots, n\}\) with \(v_i \neq 0\).

noncomputable def chartIndex {n : ℕ} (p : ProjSpace K n) : Fin (n + 1) :=
  Classical.choose (Function.ne_iff.mp p.rep_nonzero)

Uses 1 · Used by 2

Statement usesProjective space

Used byAffine coordinates of a projective point · Intersection multiplicity at a projective point

DefinitionAffine coordinates of a projective point#✓fully proved

For a field \(K\) and a point \(p \in \mathbb{P}^n(K)\), let \(v = (v_0, \dots, v_n) \in K^{n+1} \setminus \{0\}\) be the chosen representative of \(p\) and \(i\) its chart index (a chosen index with \(v_i \neq 0\)). The affine cone coordinates of \(p\) are the vector \(q \in K^{n+1}\) with \(q_j = v_j / v_i\) for every \(j\); in particular \(q_i = 1\).

noncomputable def affineConeCoord {n : ℕ} (p : ProjSpace K n) :
    Fin (n + 1) → K :=
  fun j => Projectivization.rep p j / Projectivization.rep p (chartIndex p)

Uses 2 · Used by 1

Statement usesProjective space · Chart index of a projective point

Used byIntersection multiplicity at a projective point

DefinitionEvaluation at an affine point#✓fully proved

For a field \(K\) and a point \(q = (q_0, \dots, q_n) \in K^{n+1}\), this is the ring homomorphism \(K[X_0, \dots, X_n] \to K\) sending each polynomial \(g\) to its value \(g(q)\); it fixes \(K\) and sends \(X_j\) to \(q_j\).

noncomputable def evalAt {n : ℕ} (q : Fin (n + 1) → K) :
    MvPolynomial (Fin (n + 1)) K →+* K :=
  MvPolynomial.eval q

Used by 3

Used byIntersection multiplicity at a projective point · Local ring of affine space at a point · Maximal ideal of an affine point

DefinitionMaximal ideal of an affine point#✓fully proved

For a field \(K\) and a point \(q \in K^{n+1}\), this is the ideal of \(K[X_0, \dots, X_n]\) consisting of the polynomials \(g\) with \(g(q) = 0\), that is, the kernel of evaluation at \(q\).

It is a maximal ideal, since evaluation at \(q\) is surjective onto \(K\).

noncomputable def maxIdealAt {n : ℕ} (q : Fin (n + 1) → K) :
    Ideal (MvPolynomial (Fin (n + 1)) K) :=
  RingHom.ker (evalAt q)

Uses 1 · Used by 2

Statement usesEvaluation at an affine point

Used byIntersection multiplicity at a projective point · Local ring of affine space at a point

AbbreviationLocal ring of affine space at a point#✓fully proved

For a field \(K\) and a point \(q \in K^{n+1}\), this is the localization of \(K[X_0, \dots, X_n]\) at the maximal ideal of \(q\) (the ideal of polynomials vanishing at \(q\)), that is, the local ring of affine space \(\mathbb{A}^{n+1}\) at \(q\).

noncomputable abbrev localRingAt {n : ℕ} (q : Fin (n + 1) → K) :=
  Localization.AtPrime (maxIdealAt q)

Uses 2 · Used by 1

Statement usesEvaluation at an affine point · Maximal ideal of an affine point

Used byIntersection multiplicity at a projective point

DefinitionIntersection multiplicity at a projective point#✓fully proved

Let \(K\) be a field and \(f_1, \dots, f_n \in K[X_0, \dots, X_n]\). For a point \(p \in \mathbb{P}^n(K)\), let \(i\) be its chart index, \(q \in K^{n+1}\) its affine cone coordinates (so \(q_i = 1\)), and \(\mathcal{O}_q\) the localization of \(K[X_0, \dots, X_n]\) at the maximal ideal of \(q\). The intersection multiplicity of \(f_1, \dots, f_n\) at \(p\) is the length, as an \(\mathcal{O}_q\)-module, of the quotient of \(\mathcal{O}_q\) by the ideal generated by \(f_1, \dots, f_n\) and \(X_i - 1\); it is an element of \(\mathbb{N} \cup \{\infty\}\).

The value is \(\infty\) exactly when this quotient does not have finite length, for example along a positive-dimensional component of the common zero set.

noncomputable def intersectionMultiplicity {n : ℕ}
    (f : Fin n → MvPolynomial (Fin (n + 1)) K)
    (p : ProjSpace K n) : ℕ∞ :=
  let q := affineConeCoord p
  let i := chartIndex p
  let φ : MvPolynomial (Fin (n + 1)) K →+* localRingAt q := algebraMap _ _
  let I : Ideal (localRingAt q) :=
    Ideal.span ((Set.range fun k : Fin n => φ (f k)) ∪ {φ (X i - C 1)})
  Module.length (localRingAt q) (localRingAt q ⧸ I)

Uses 6 · Used by 1

Statement usesProjective space · Affine coordinates of a projective point · Chart index of a projective point · Evaluation at an affine point · Local ring of affine space at a point · Maximal ideal of an affine point

Used byBézout's theorem (with multiplicity)

TheoremBézout's theorem (with multiplicity)#●ready to prove

Let \(K\) be an algebraically closed field, let \(n \in \mathbb{N}\), and let \(f_1, \dots, f_n \in K[X_0, \dots, X_n]\) and integers \(d_1, \dots, d_n \ge 1\) be such that each \(f_k\) is homogeneous of degree \(d_k\) and has total degree exactly \(d_k\). Suppose the common projective zero set \(Z = V(f_1) \cap \dots \cap V(f_n) \subseteq \mathbb{P}^n(K)\) is finite. Then \(\sum_{p \in Z} i_p(f_1, \dots, f_n) = d_1 d_2 \cdots d_n\) in \(\mathbb{N} \cup \{\infty\}\), where \(i_p(f_1, \dots, f_n)\) is the intersection multiplicity of \(f_1, \dots, f_n\) at \(p\).

The total degree hypothesis rules out \(f_k = 0\), which is homogeneous of every degree but has total degree \(0\).

public theorem_wanted bezout_multiplicity [IsAlgClosed K] {n : ℕ}
    (f : Fin n → MvPolynomial (Fin (n + 1)) K)
    (d : Fin n → ℕ) (_hd : ∀ k, (f k).IsHomogeneous (d k))
    (_hdeg : ∀ k, (f k).totalDegree = d k)
    (_hd_pos : ∀ k, 1 ≤ d k)
    (_hfin : (⋂ k, vanishingSet (f k)).Finite) :
    ∑ᶠ p ∈ (⋂ k, vanishingSet (f k)), intersectionMultiplicity f p
      = (∏ k, d k : ℕ∞)

Sources

• É. Bézout, Théorie générale des équations algébriques, Paris, 1779. Modern projective formulation: see Eisenbud, Commutative Algebra, Chapter 12, or Hartshorne, Algebraic Geometry, Ch. I §7. Listed as §50 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem bezout_projective_multiplicity of the lean-eval benchmark.

Uses 3

Statement usesProjective space · Intersection multiplicity at a projective point · Projective vanishing set

8 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.