noncomputable def BezoutIntersection.mulByXOp (k : Type u_1) [Field k] (f g : Polynomial (Polynomial k)) : Module.End k (Polynomial (Polynomial k) ⧸ Ideal.span {f, g})

Multiplication-by-X operator on the quotient k[X][Y]/⟨f, g⟩, viewed as a k-linear endomorphism.

noncomputable def BezoutIntersection.mulByYOp (k : Type u_1) [Field k] (f g : Polynomial (Polynomial k)) : Module.End k (Polynomial (Polynomial k) ⧸ Ideal.span {f, g})

Multiplication-by-Y operator (i.e. by C X in k[X][Y]) on the quotient k[X][Y]/⟨f, g⟩, viewed as a k-linear endomorphism.

noncomputable def BezoutIntersection.localIntersectionMultiplicity (k : Type u_1) [Field k] (f g : Polynomial (Polynomial k)) (a b : k) : ℕ

Local intersection multiplicity of the affine plane curves f = 0 and g = 0 at the point (a, b), defined as the dimension of the simultaneous generalised eigenspace of the multiplication-by-X and multiplication-by-Y operators with eigenvalues a and b.

noncomputable def BezoutIntersection.totalIntersectionNumber (k : Type u_1) [Field k] (f g : Polynomial (Polynomial k)) : ℕ

Total intersection number of f and g, equal to the k-dimension of the quotient k[X][Y]/⟨f, g⟩. Bezout's theorem identifies this with deg(f) · deg(g).

theorem BezoutIntersection.artinian_local_global_decomposition (k : Type u_1) [Field k] (f g : Polynomial (Polynomial k)) (S : Finset (k × k)) (hS : ∀ (p : k × k), localIntersectionMultiplicity k f g p.1 p.2 ≠ 0 → p ∈ S) (hS' : ∀ p ∈ S, localIntersectionMultiplicity k f g p.1 p.2 ≠ 0) : totalIntersectionNumber k f g = ∑ p ∈ S, localIntersectionMultiplicity k f g p.1 p.2

Artinian local-global decomposition: the total intersection number decomposes as a finite sum of local intersection multiplicities over the points contributing nonzero multiplicity.

theorem BezoutIntersection.totalIntersectionNumber_eq_sup (k : Type u_1) [Field k] (f g : Polynomial (Polynomial k)) : totalIntersectionNumber k f g = Module.finrank k (Polynomial (Polynomial k) ⧸ Ideal.span {f} ⊔ Ideal.span {g})

The total intersection number can equivalently be computed as the k-dimension of the quotient by the supremum of the principal ideals ⟨f⟩ and ⟨g⟩.

theorem BezoutIntersection.bezout_irreducible_base (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) (hirr : Irreducible g) (p : Polynomial k) (hp : (algebraMap (Polynomial k) (AdjoinRoot g)) p ≠ 0) : totalIntersectionNumber k g (Polynomial.C p) = g.natDegree * p.natDegree

Bezout's theorem for an irreducible monic g against a polynomial of the form C p: the total intersection number equals deg(g) · deg(p).

theorem BezoutIntersection.intersection_additivity (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) [IsDomain (AdjoinRoot g)] (f₁ f₂ : Polynomial k) (hf₁ : f₁ ≠ 0) (hf₂ : f₂ ≠ 0) : Module.finrank k (AdjoinRoot g ⧸ Ideal.span {(algebraMap (Polynomial k) (AdjoinRoot g)) (f₁ * f₂)}) = Module.finrank k (AdjoinRoot g ⧸ Ideal.span {(algebraMap (Polynomial k) (AdjoinRoot g)) f₁}) + Module.finrank k (AdjoinRoot g ⧸ Ideal.span {(algebraMap (Polynomial k) (AdjoinRoot g)) f₂})

Additivity of intersection with a product: the k-dimension of the quotient by f₁ · f₂ in AdjoinRoot g splits as the sum of the dimensions for f₁ and f₂.

theorem BezoutIntersection.intersection_depends_only_on_degree (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) [IsDomain (AdjoinRoot g)] (p q : Polynomial k) (hp : p ≠ 0) (hq : q ≠ 0) (hdeg : p.natDegree = q.natDegree) : Module.finrank k (AdjoinRoot g ⧸ Ideal.span {(algebraMap (Polynomial k) (AdjoinRoot g)) p}) = Module.finrank k (AdjoinRoot g ⧸ Ideal.span {(algebraMap (Polynomial k) (AdjoinRoot g)) q})

The k-dimension of the quotient AdjoinRoot g / ⟨p⟩ depends only on the degree of p.

theorem BezoutIntersection.divisor_degree_of_intersection (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) [IsDomain (AdjoinRoot g)] (p : Polynomial k) (hp : p ≠ 0) : Module.finrank k (AdjoinRoot g ⧸ Ideal.span {(algebraMap (Polynomial k) (AdjoinRoot g)) p}) = g.natDegree * p.natDegree

Degree formula: dim_k (AdjoinRoot g / ⟨p⟩) = deg(g) · deg(p).

theorem BezoutIntersection.bezout_theorem (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) (hirr : Irreducible g) (p : Polynomial k) (hp : (algebraMap (Polynomial k) (AdjoinRoot g)) p ≠ 0) : totalIntersectionNumber k g (Polynomial.C p) = g.natDegree * p.natDegree

Bezout's theorem (final packaging): for an irreducible monic g and p ∈ k[X] nonzero in the quotient, the total intersection number of g and C p is deg(g) · deg(p).