noncomputable def projectiveIntersectionNumber (k : Type u_1) [Field k] (f g : MvPolynomial (Fin 3) k) (n : ℕ) : ℕ

The projective intersection number of two homogeneous polynomials f, g in three variables, defined as the k-dimension of the degree-n piece of k[x,y,z] / (⟨f⟩ + ⟨g⟩).

theorem homogQuotPiece_ideal_eq (k : Type u_1) [Field k] {I J : Ideal (MvPolynomial (Fin 3) k)} (h : I = J) (n : ℕ) : Module.finrank k (homogQuotPiece k I n) = Module.finrank k (homogQuotPiece k J n)

Equal ideals give equal homogeneous quotient piece dimensions.

theorem bezout_theorem_multiplicity_sum (k : Type u_1) [Field k] (d e : ℕ) (hd : 0 < d) (he : 0 < e) (f g : MvPolynomial (Fin 3) k) (hf_homog : f.IsHomogeneous d) (hg_homog : g.IsHomogeneous e) (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hcoprime : IsCoprime f g) (n : ℕ) : d + e - 2 ≤ n → projectiveIntersectionNumber k f g n = d * e

Bezout's theorem in multiplicity-sum form: for coprime homogeneous f, g of degrees d, e and sufficiently large n, the projective intersection number equals d * e.

theorem projectiveIntersectionNumber_comm (k : Type u_1) [Field k] (f g : MvPolynomial (Fin 3) k) (n : ℕ) : projectiveIntersectionNumber k f g n = projectiveIntersectionNumber k g f n

Symmetry of the projective intersection number in its two homogeneous arguments.

theorem bezout_line_line (k : Type u_1) [Field k] (f g : MvPolynomial (Fin 3) k) (hf : f.IsHomogeneous 1) (hg : g.IsHomogeneous 1) (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hcop : IsCoprime f g) (n : ℕ) : projectiveIntersectionNumber k f g n = 1

Two distinct lines in P² intersect in exactly one point (counted with multiplicity).

theorem bezout_line_conic (k : Type u_1) [Field k] (f g : MvPolynomial (Fin 3) k) (hf : f.IsHomogeneous 1) (hg : g.IsHomogeneous 2) (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hcop : IsCoprime f g) (n : ℕ) (hn : 1 ≤ n) : projectiveIntersectionNumber k f g n = 2

A line meets a conic in P² in exactly 1 · 2 = 2 points (counted with multiplicity).

theorem bezout_conic_conic (k : Type u_1) [Field k] (f g : MvPolynomial (Fin 3) k) (hf : f.IsHomogeneous 2) (hg : g.IsHomogeneous 2) (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hcop : IsCoprime f g) (n : ℕ) (hn : 2 ≤ n) : projectiveIntersectionNumber k f g n = 4

Two distinct conics in P² intersect in 2 · 2 = 4 points (counted with multiplicity).

theorem bezout_line_cubic (k : Type u_1) [Field k] (f g : MvPolynomial (Fin 3) k) (hf : f.IsHomogeneous 1) (hg : g.IsHomogeneous 3) (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hcop : IsCoprime f g) (n : ℕ) (hn : 2 ≤ n) : projectiveIntersectionNumber k f g n = 3

A line meets a smooth cubic in P² in 1 · 3 = 3 points (counted with multiplicity).

structure ProjectivePoint (k : Type u_2) [Field k] (f g : MvPolynomial (Fin 3) k) : Type u_2

A point of intersection of the projective varieties V(f) and V(g), encoded as a prime ideal of k[x, y, z] containing both f and g.

• P : Ideal (MvPolynomial (Fin 3) k)
• hP_prime : self.P.IsPrime
• hf_mem : f ∈ self.P
• hg_mem : g ∈ self.P

noncomputable def projLocalIntersectionMultiplicity (k : Type u_1) [Field k] (f g : MvPolynomial (Fin 3) k) (p : ProjectivePoint k f g) : ℕ

Local intersection multiplicity at a projective intersection point p of f and g, defined as the k-dimension of the localisation of k[x, y, z] / (⟨f⟩ + ⟨g⟩) at the image of p.

theorem projLocalIntersectionMultiplicity_finite (k : Type u_1) [Field k] (d e : ℕ) (hd : 0 < d) (he : 0 < e) (f g : MvPolynomial (Fin 3) k) (hf_homog : f.IsHomogeneous d) (hg_homog : g.IsHomogeneous e) (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hcoprime : IsCoprime f g) : ∃ (S : Finset (ProjectivePoint k f g)), (∀ (p : ProjectivePoint k f g), projLocalIntersectionMultiplicity k f g p ≠ 0 → p ∈ S) ∧ ∀ p ∈ S, projLocalIntersectionMultiplicity k f g p ≠ 0

For coprime homogeneous polynomials f, g, only finitely many projective points have a nonzero local intersection multiplicity.

theorem artinian_decomposition_sum (k : Type u_2) [Field k] (d e : ℕ) (hd : 0 < d) (he : 0 < e) (f g : MvPolynomial (Fin 3) k) (hf_homog : f.IsHomogeneous d) (hg_homog : g.IsHomogeneous e) (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hcoprime : IsCoprime f g) (S : Finset (ProjectivePoint k f g)) (hS : ∀ (p : ProjectivePoint k f g), projLocalIntersectionMultiplicity k f g p ≠ 0 → p ∈ S) (hS' : ∀ p ∈ S, projLocalIntersectionMultiplicity k f g p ≠ 0) (n : ℕ) (hn : d + e - 2 ≤ n) : ∑ p ∈ S, projLocalIntersectionMultiplicity k f g p = Module.finrank k (homogQuotPiece k (Ideal.span {f} ⊔ Ideal.span {g}) n)

Artinian decomposition for the homogeneous quotient: the sum of local multiplicities at the intersection points equals the dimension of the stable graded piece.

theorem projective_bezout_multiplicity_sum (k : Type u_1) [Field k] (d e : ℕ) (hd : 0 < d) (he : 0 < e) (f g : MvPolynomial (Fin 3) k) (hf_homog : f.IsHomogeneous d) (hg_homog : g.IsHomogeneous e) (hf_ne : f ≠ 0) (hg_ne : g ≠ 0) (hcoprime : IsCoprime f g) (S : Finset (ProjectivePoint k f g)) (hS : ∀ (p : ProjectivePoint k f g), projLocalIntersectionMultiplicity k f g p ≠ 0 → p ∈ S) (hS' : ∀ p ∈ S, projLocalIntersectionMultiplicity k f g p ≠ 0) : ∑ p ∈ S, projLocalIntersectionMultiplicity k f g p = d * e

Projective Bezout (multiplicity-sum form): for coprime homogeneous f, g of degrees d, e the sum of local intersection multiplicities over all intersection points equals d * e.