@[reducible, inline]

noncomputable abbrev homogQuotPiece (k : Type u_1) [Field k] (I : Ideal (MvPolynomial (Fin 3) k)) (n : ℕ) : Type u_1

The degree-n piece of the homogeneous quotient ring k[x₀, x₁, x₂] / I, presented as the quotient of the space of degree-n homogeneous polynomials by the corresponding piece of I.

def hasTotalDegreeAtMost {k : Type u_1} [CommSemiring k] (f : Polynomial (Polynomial k)) (n : ℕ) : Prop

Predicate stating that the bivariate polynomial f ∈ k[X][Y] has total degree at most n, i.e. for each coefficient f.coeff i ∈ k[X] the sum of its X-degree and Y-index i is ≤ n.

theorem resultant_degree_formula (k : Type u_1) [Field k] (g : Polynomial (Polynomial k)) (hg : g.Monic) (hirr : Irreducible g) (f : Polynomial (Polynomial k)) (hf : (AdjoinRoot.mk g) f ≠ 0) (d e : ℕ) (hg_deg : hasTotalDegreeAtMost g e) (hf_deg : hasTotalDegreeAtMost f d) : ((Algebra.norm (Polynomial k)) ((AdjoinRoot.mk g) f)).natDegree = d * e

Resultant degree formula: when g and f have total degrees at most e and d respectively, the norm of AdjoinRoot.mk g f has degree d * e.

theorem graded_affine_stabilization (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) : ∃ (g' : Polynomial (Polynomial k)) (f' : Polynomial (Polynomial k)), g'.Monic ∧ Irreducible g' ∧ (AdjoinRoot.mk g') f' ≠ 0 ∧ hasTotalDegreeAtMost g' e ∧ hasTotalDegreeAtMost f' d ∧ ∀ (n : ℕ), d + e - 2 ≤ n → Module.finrank k (homogQuotPiece k (Ideal.span {f} ⊔ Ideal.span {g}) n) = Module.finrank k (Polynomial (Polynomial k) ⧸ Ideal.span {g', f'})

Graded-affine stabilization: for large enough n ≥ d + e - 2, the degree-n piece of the homogeneous coordinate ring of V(f) ∩ V(g) ⊂ P² is k-linearly equivalent to an affine quotient k[X][Y] / ⟨g', f'⟩ for suitable bivariate polynomials g', f'.

theorem bezout_theorem (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 → Module.finrank k (homogQuotPiece k (Ideal.span {f} ⊔ Ideal.span {g}) n) = d * e

Bezout's theorem (Thm 5.2, Thm 16.1): for coprime homogeneous polynomials f, g of degrees d, e defining curves in P², the Hilbert function of the quotient stabilises at d * e once the degree n is at least d + e - 2.