Polynomials in two variables

For φ : MvPolynomial (Fin 2) R the monomial with exponent s : Fin 2 →₀ ℕ is X₀ ^ s 0 * X₁ ^ s 1, of degree s 0 + s 1. This file records the evaluation of φ at a pair (a, b) as a sum over these monomials, and the description of the total degree of φ as the largest s 0 + s 1 over its support. These are the forms in which a plane curve equation φ(x, y) = 0 of degree n is manipulated term by term.

Main results

• MvPolynomial.aeval_fin_two_eq_sum: φ(a, b) = ∑ₛ cₛ a ^ s 0 b ^ s 1.
• MvPolynomial.aeval_monomial_fin_two: the monomial c X₀ ^ s 0 X₁ ^ s 1 evaluates at (a, b) to c a ^ s 0 b ^ s 1.
• MvPolynomial.coeff_X_zero_pow_mul_X_one_pow: the coefficient of X₀ ^ i X₁ ^ j in X₀ ^ r X₁ ^ m is 1 when (r, m) = (i, j) and 0 otherwise.
• MvPolynomial.IsHomogeneous.add_eq_of_mem_support: every monomial of a homogeneous φ of degree n has degree n.
• MvPolynomial.add_le_totalDegree_of_mem_support: every monomial of φ has degree at most the total degree of φ.
• MvPolynomial.exists_mem_support_add_eq_totalDegree: a nonzero φ has a monomial of degree exactly its total degree.
• MvPolynomial.eq_single_one_of_mem_support: if φ has total degree at most n, its only possible monomial with exponent n in X₁ is X₁ ^ n.
• MvPolynomial.totalDegree_pos_of_aeval_eq_zero: if the coefficient of X₁ ^ n in φ is 1, where n is the total degree of φ, and φ has a zero, then n is positive.
• MvPolynomial.sum_coeff_mul_div_pow_mul_inv_pow_eq_zero: dividing a relation φ(x, y) = 0 by y ^ totalDegree φ gives a vanishing sum in the variables x / y and y⁻¹.
• MvPolynomial.exists_sum_coeff_mul_pow_ne_zero: over a domain with more than deg φ elements, the leading form φ_n of φ satisfies φ_n(c, 1) ≠ 0 for some c.
• MvPolynomial.natDegree_minpoly_le_totalDegree: if φ(u + c y, y) = 0 with u ∈ K and φ_n(c, 1) ≠ 0, then y has degree at most deg φ over K.
• Polynomial.Bivariate.aeval_equivMvPolynomial: evaluating p ∈ R[X][Y] at y over an R[X]-algebra is evaluating the corresponding φ ∈ R[X₀, X₁] at (X, y); this reads a plane curve equation φ as a polynomial in X₁ over R[X₀].
• Polynomial.Bivariate.aeval_map_eq_aeval_equivMvPolynomial: the same, after mapping p to K[Y] for an R[X]-algebra K.
• Polynomial.Bivariate.monic_equivMvPolynomial_symm and Polynomial.Bivariate.natDegree_equivMvPolynomial_symm: if φ has total degree at most n and the coefficient of X₁ ^ n is 1, then φ, read as a polynomial in X₁ over R[X₀], is monic of degree n.
• Polynomial.Bivariate.isAlgebraic_of_aeval_algebraMap_eq_zero: if φ(a, T) ≠ 0 and φ(a, y) = 0 for a constant a ∈ k, then y is algebraic over k.
• Polynomial.Bivariate.isAlgebraic_of_isAlgebraic_of_aeval_eq_zero: if φ has coefficient 1 on X₁ ^ (total degree), φ(u, y) = 0 and u is algebraic over k, then y is algebraic over k.

The chart at infinity

For n at least the total degree of φ, the degree-n homogenization of φ is Φ(X₀, X₁, X₂) = ∑ₛ cₛ X₀ ^ s 0 X₁ ^ s 1 X₂ ^ (n - s 0 - s 1), and φ = Φ(X₀, X₁, 1). In the affine chart where the first homogeneous coordinate does not vanish, with coordinates (X₂ / X₀, X₁ / X₀), the equation Φ = 0 reads MvPolynomial.inftyChart n φ = Φ(1, X₁, X₀), that is X₀ ^ n φ(1 / X₀, X₁ / X₀). When n is the total degree of φ, Φ = 0 is the projective closure of the curve φ = 0; for larger n it also contains the line at infinity X₂ = 0. In the case n = φ.totalDegree, this chart contains the points at infinity of φ = 0 other than (0 : 1 : 0), and when the coefficient of X₁ ^ n is nonzero that point is not on the curve.

• MvPolynomial.coeff_inftyChart and MvPolynomial.inftyChart_monomial: the coefficients of the chart equation.
• MvPolynomial.inftyChart_dehomogenize: for G homogeneous of degree n in three variables, the chart at infinity of the affine equation TauCeti.dehomogenize 2 G is the dehomogenization TauCeti.dehomogenize 0 G with its two coordinates swapped.
• MvPolynomial.aeval_inftyChart: ψ(x⁻¹, y x⁻¹) = x⁻ⁿ φ(x, y) for ψ = inftyChart n φ.
• MvPolynomial.aeval_pderiv_one_inftyChart: ∂ψ/∂X₁ (x⁻¹, y x⁻¹) = x^(1 - n) ∂φ/∂X₁ (x, y).
• MvPolynomial.totalDegree_inftyChart_le and MvPolynomial.coeff_single_one_inftyChart: the chart equation again has total degree at most n, with the same coefficient of X₁ ^ n.

theorem MvPolynomial.aeval_fin_two_eq_sum {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] (φ : MvPolynomial (Fin 2) R) (a b : A) : (aeval ![a, b]) φ = ∑ s ∈ φ.support, (algebraMap R A) (φ.coeff s) * (a ^ s 0 * b ^ s 1)

A polynomial in two variables evaluated at (a, b) is the sum of its terms c_s a ^ s 0 b ^ s 1.

theorem MvPolynomial.aeval_monomial_fin_two {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommSemiring A] [Algebra R A] (a b : A) (s : Fin 2 →₀ ℕ) (c : R) : (aeval ![a, b]) ((monomial s) c) = (algebraMap R A) c * (a ^ s 0 * b ^ s 1)

Evaluating the monomial c X₀ ^ s 0 X₁ ^ s 1 at (a, b) gives c a ^ s 0 b ^ s 1.

@[simp]

theorem MvPolynomial.coeff_X_zero_pow_mul_X_one_pow {R : Type u_1} [CommSemiring R] (i j r m : ℕ) : (X 0 ^ r * X 1 ^ m).coeff (Finsupp.single 0 i + Finsupp.single 1 j) = if r = i ∧ m = j then 1 else 0

The coefficient of X₀ ^ i X₁ ^ j in the monomial X₀ ^ r X₁ ^ m is 1 when r = i and m = j, and 0 otherwise.

theorem MvPolynomial.IsHomogeneous.add_eq_of_mem_support {R : Type u_1} [CommSemiring R] {φ : MvPolynomial (Fin 2) R} {n : ℕ} (hφ : φ.IsHomogeneous n) {s : Fin 2 →₀ ℕ} (hs : s ∈ φ.support) : s 0 + s 1 = n

Every monomial of a homogeneous polynomial of degree n in two variables has degree n.

theorem MvPolynomial.add_le_totalDegree_of_mem_support {R : Type u_1} [CommSemiring R] {φ : MvPolynomial (Fin 2) R} {s : Fin 2 →₀ ℕ} (hs : s ∈ φ.support) : s 0 + s 1 ≤ φ.totalDegree

Every monomial of a polynomial in two variables has degree at most its total degree.

theorem MvPolynomial.exists_mem_support_add_eq_totalDegree {R : Type u_1} [CommSemiring R] {φ : MvPolynomial (Fin 2) R} (hφ : φ ≠ 0) : ∃ s ∈ φ.support, s 0 + s 1 = φ.totalDegree

A nonzero polynomial in two variables has a monomial whose degree is its total degree.

theorem MvPolynomial.eq_single_one_of_mem_support {R : Type u_1} [CommSemiring R] {φ : MvPolynomial (Fin 2) R} {n : ℕ} (hφ : φ.totalDegree ≤ n) {s : Fin 2 →₀ ℕ} (hs : s ∈ φ.support) (h1 : s 1 = n) : s = Finsupp.single 1 n

A monomial of a polynomial in two variables of total degree at most n whose exponent of X₁ is n is X₁ ^ n.

theorem MvPolynomial.totalDegree_pos_of_aeval_eq_zero {R : Type u_1} [CommSemiring R] {φ : MvPolynomial (Fin 2) R} (hc : φ.coeff (Finsupp.single 1 φ.totalDegree) = 1) {A : Type u_2} [CommSemiring A] [Nontrivial A] [Algebra R A] {v : Fin 2 → A} (hv : (aeval v) φ = 0) : 0 < φ.totalDegree

If the coefficient of X₁ ^ n in a polynomial in two variables of total degree n is 1, and the polynomial has a zero, then n is positive.

The chart at infinity

noncomputable def MvPolynomial.inftyChart {R : Type u_1} [CommSemiring R] (n : ℕ) (φ : MvPolynomial (Fin 2) R) : MvPolynomial (Fin 2) R

The equation of a plane curve in the chart at infinity: for φ = ∑ₛ cₛ X₀ ^ s 0 X₁ ^ s 1, inftyChart n φ = ∑ₛ cₛ X₀ ^ (n - s 0 - s 1) X₁ ^ s 1, which is X₀ ^ n φ(1 / X₀, X₁ / X₀) when n is at least the total degree of φ. It is the degree-n homogenization of φ, dehomogenized in the affine chart where the first homogeneous coordinate does not vanish; when n = φ.totalDegree this is the equation of the projective closure of φ = 0 in that chart.

theorem MvPolynomial.inftyChart_add {R : Type u_1} [CommSemiring R] (n : ℕ) (φ ψ : MvPolynomial (Fin 2) R) : inftyChart n (φ + ψ) = inftyChart n φ + inftyChart n ψ

Passing to the chart at infinity is additive.

@[simp]

theorem MvPolynomial.inftyChart_monomial {R : Type u_1} [CommSemiring R] (n : ℕ) (s : Fin 2 →₀ ℕ) (c : R) : inftyChart n ((monomial s) c) = (monomial (Finsupp.single 0 (n - (s 0 + s 1)) + Finsupp.single 1 (s 1))) c

The chart equation at infinity of the monomial c X₀ ^ s 0 X₁ ^ s 1 is c X₀ ^ (n - s 0 - s 1) X₁ ^ s 1.

theorem MvPolynomial.coeff_inftyChart {R : Type u_1} [CommSemiring R] {φ : MvPolynomial (Fin 2) R} {n : ℕ} (hφ : φ.totalDegree ≤ n) (s : Fin 2 →₀ ℕ) : (inftyChart n φ).coeff s = if s 0 + s 1 ≤ n then φ.coeff (Finsupp.single 0 (n - (s 0 + s 1)) + Finsupp.single 1 (s 1)) else 0

The coefficients of the chart equation at infinity: for φ of total degree at most n, the coefficient of X₀ ^ a X₁ ^ b in inftyChart n φ is the coefficient of X₀ ^ (n - a - b) X₁ ^ b in φ if a + b ≤ n, and 0 otherwise.

theorem MvPolynomial.inftyChart_dehomogenize {R : Type u_1} [CommSemiring R] {G : MvPolynomial (Fin 3) R} {n : ℕ} (hG : G.IsHomogeneous n) : inftyChart n ((TauCeti.dehomogenize 2) G) = (rename ⇑(Equiv.swap 0 1)) ((TauCeti.dehomogenize 0) G)

The chart at infinity as a dehomogenization: let G be homogeneous of degree n in the homogeneous coordinates (X₀ : X₁ : X₂). The chart at infinity of the affine equation G(X₀, X₁, 1) is G(1, X₁, X₀), that is the dehomogenization of G at the first coordinate with its two remaining coordinates swapped.

theorem MvPolynomial.totalDegree_inftyChart_le {R : Type u_1} [CommSemiring R] {φ : MvPolynomial (Fin 2) R} {n : ℕ} (hφ : φ.totalDegree ≤ n) : (inftyChart n φ).totalDegree ≤ n

The chart equation at infinity of a polynomial of total degree at most n again has total degree at most n.

@[simp]

theorem MvPolynomial.coeff_single_one_inftyChart {R : Type u_1} [CommSemiring R] {φ : MvPolynomial (Fin 2) R} {n : ℕ} (hφ : φ.totalDegree ≤ n) : (inftyChart n φ).coeff (Finsupp.single 1 n) = φ.coeff (Finsupp.single 1 n)

Passing to the chart at infinity keeps the coefficient of X₁ ^ n.

theorem MvPolynomial.sum_coeff_mul_div_pow_mul_inv_pow_eq_zero {R : Type u_1} [CommSemiring R] {F : Type u_2} [Semifield F] [Algebra R F] {φ : MvPolynomial (Fin 2) R} {x y : F} (hφxy : (aeval ![x, y]) φ = 0) (hy0 : y ≠ 0) : ∑ s ∈ φ.support, (algebraMap R F) (φ.coeff s) * (x / y) ^ s 0 * y⁻¹ ^ (φ.totalDegree - (s 0 + s 1)) = 0

Dividing a plane relation φ(x, y) = 0 by y ^ totalDegree φ gives a vanishing sum in the variables x / y and y⁻¹.

theorem MvPolynomial.aeval_inftyChart {R : Type u_1} [CommSemiring R] {L : Type u_2} [Semifield L] [Algebra R L] {φ : MvPolynomial (Fin 2) R} {n : ℕ} (hφ : φ.totalDegree ≤ n) {x : L} (hx : x ≠ 0) (y : L) : (aeval ![x⁻¹, y * x⁻¹]) (inftyChart n φ) = x⁻¹ ^ n * (aeval ![x, y]) φ

Evaluating the chart equation at infinity: for x ≠ 0 and φ of total degree at most n, inftyChart n φ (x⁻¹, y x⁻¹) = x⁻ⁿ φ(x, y).

theorem MvPolynomial.aeval_pderiv_one_inftyChart {R : Type u_1} [CommSemiring R] {L : Type u_2} [Semifield L] [Algebra R L] {φ : MvPolynomial (Fin 2) R} {n : ℕ} (hφ : φ.totalDegree ≤ n) {x : L} (hx : x ≠ 0) (y : L) : (aeval ![x⁻¹, y * x⁻¹]) ((pderiv 1) (inftyChart n φ)) = x⁻¹ ^ (n - 1) * (aeval ![x, y]) ((pderiv 1) φ)

The partial derivative in X₁ in the chart at infinity: for x ≠ 0 and φ of total degree at most n, ∂(inftyChart n φ)/∂X₁ (x⁻¹, y x⁻¹) = x^(1 - n) ∂φ/∂X₁ (x, y).

theorem MvPolynomial.exists_sum_coeff_mul_pow_ne_zero {k : Type u_2} [CommRing k] [IsDomain k] {φ : MvPolynomial (Fin 2) k} (hφ : φ ≠ 0) (hcard : ↑φ.totalDegree < ENat.card k) : ∃ (c : k), ∑ s ∈ φ.support with s 0 + s 1 = φ.totalDegree, φ.coeff s * c ^ s 0 ≠ 0

Over a domain with more than n elements, the leading form φ_n of a nonzero polynomial φ of total degree n satisfies φ_n(c, 1) ≠ 0 for some c.

theorem MvPolynomial.natDegree_minpoly_le_totalDegree {k : Type u_2} [CommSemiring k] {K : Type u_3} {F : Type u_4} [Field K] [CommRing F] [Algebra k K] [FaithfulSMul k K] [Algebra K F] [Algebra k F] [IsScalarTower k K F] {φ : MvPolynomial (Fin 2) k} {u : K} {y : F} {c : k} (hφ : (aeval ![(algebraMap K F) u + (algebraMap k F) c * y, y]) φ = 0) (hc : ∑ s ∈ φ.support with s 0 + s 1 = φ.totalDegree, φ.coeff s * c ^ s 0 ≠ 0) : (minpoly K y).natDegree ≤ φ.totalDegree

If φ(u + c y, y) = 0 with u ∈ K and the leading form of φ does not vanish at (c, 1), then y has degree at most deg φ over K: it is a root of φ(u + c Y, Y), whose coefficient of Y ^ n is φ_n(c, 1). The coefficients may lie in any commutative semiring mapping faithfully into K, and y may lie in any commutative K-algebra.

theorem MvPolynomial.exists_eval_ne_zero_and_div_notMem {K : Type u_2} [Field K] [Infinite K] {H : MvPolynomial (Fin 2) K} (hH : H ≠ 0) (s : Finset K) : ∃ (v : Fin 2 → K), (eval v) H ≠ 0 ∧ v 0 ≠ 0 ∧ v 1 / v 0 ∉ s

A nonzero plane polynomial does not vanish at some point whose first coordinate is nonzero and whose slope v 1 / v 0 avoids a given finite set.

@[simp]

theorem Polynomial.Bivariate.aeval_equivMvPolynomial {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] [Algebra (Polynomial R) A] [IsScalarTower R (Polynomial R) A] (y : A) (p : Polynomial (Polynomial R)) : (MvPolynomial.aeval ![(algebraMap (Polynomial R) A) X, y]) ((equivMvPolynomial R) p) = (aeval y) p

Evaluating p ∈ R[X][Y] at y in an R[X]-algebra A is evaluating the corresponding polynomial in two variables at the image of X and at y.

theorem Polynomial.Bivariate.aeval_map_eq_aeval_equivMvPolynomial {R : Type u_1} [CommSemiring R] {K : Type u_3} {F : Type u_4} [CommSemiring K] [CommSemiring F] [Algebra R K] [Algebra (Polynomial R) K] [IsScalarTower R (Polynomial R) K] [Algebra K F] [Algebra R F] [IsScalarTower R K F] (p : Polynomial (Polynomial R)) (y : F) : (aeval y) (map (algebraMap (Polynomial R) K) p) = (MvPolynomial.aeval ![(algebraMap K F) ((algebraMap (Polynomial R) K) X), y]) ((equivMvPolynomial R) p)

Evaluating p ∈ R[X][Y], mapped to K[Y] for an R[X]-algebra K, at y in a K-algebra F is evaluating the corresponding polynomial in two variables at the image of X and at y.

@[simp]

theorem Polynomial.Bivariate.equivMvPolynomial_symm_monomial {R : Type u_3} [CommSemiring R] (s : Fin 2 →₀ ℕ) (c : R) : (equivMvPolynomial R).symm ((MvPolynomial.monomial s) c) = C (C c * X ^ s 0) * X ^ s 1

The monomial c X₀ ^ s 0 X₁ ^ s 1, read as a polynomial in X₁ over R[X₀].

theorem Polynomial.Bivariate.natDegree_equivMvPolynomial_symm_le {R : Type u_3} [CommSemiring R] {φ : MvPolynomial (Fin 2) R} {n : ℕ} (hφ : φ.totalDegree ≤ n) : ((equivMvPolynomial R).symm φ).natDegree ≤ n

A polynomial in two variables of total degree at most n has degree at most n in X₁.

theorem Polynomial.Bivariate.coeff_equivMvPolynomial_symm_of_totalDegree_le {R : Type u_3} [CommSemiring R] {φ : MvPolynomial (Fin 2) R} {n : ℕ} (hφ : φ.totalDegree ≤ n) : ((equivMvPolynomial R).symm φ).coeff n = C (φ.coeff (Finsupp.single 1 n))

For a polynomial in two variables of total degree at most n, the coefficient of X₁ ^ n over R[X₀] is the constant polynomial given by the coefficient of X₁ ^ n.

theorem Polynomial.Bivariate.monic_equivMvPolynomial_symm {R : Type u_3} [CommSemiring R] {φ : MvPolynomial (Fin 2) R} {n : ℕ} (hφ : φ.totalDegree ≤ n) (hc : φ.coeff (Finsupp.single 1 n) = 1) : ((equivMvPolynomial R).symm φ).Monic

A polynomial in two variables of total degree at most n in which X₁ ^ n has coefficient 1 is monic as a polynomial in X₁ over R[X₀].

theorem Polynomial.Bivariate.natDegree_equivMvPolynomial_symm {R : Type u_3} [CommSemiring R] [Nontrivial R] {φ : MvPolynomial (Fin 2) R} {n : ℕ} (hφ : φ.totalDegree ≤ n) (hc : φ.coeff (Finsupp.single 1 n) = 1) : ((equivMvPolynomial R).symm φ).natDegree = n

A polynomial in two variables of total degree at most n in which X₁ ^ n has coefficient 1 has degree n as a polynomial in X₁ over R[X₀].

theorem Polynomial.Bivariate.isAlgebraic_of_aeval_algebraMap_eq_zero {k : Type u_3} {F : Type u_4} [CommRing k] [CommRing F] [Algebra k F] {φ : MvPolynomial (Fin 2) k} {a : k} (hq : map (evalRingHom a) ((equivMvPolynomial k).symm φ) ≠ 0) {y : F} (hy : (MvPolynomial.aeval ![(algebraMap k F) a, y]) φ = 0) : IsAlgebraic k y

If φ ∈ k[X₀, X₁] and a ∈ k are such that φ(a, T) ≠ 0 and φ(a, y) = 0, then y is algebraic over k: it is a root of the nonzero polynomial φ(a, T). This applies in particular when φ is monic in X₁ over k[X₀] and k is nontrivial.

theorem Polynomial.Bivariate.isAlgebraic_of_isAlgebraic_of_aeval_eq_zero {k : Type u_3} {F : Type u_4} [Field k] [Field F] [Algebra k F] {φ : MvPolynomial (Fin 2) k} (hlead : φ.coeff (Finsupp.single 1 φ.totalDegree) = 1) {u y : F} (hu : IsAlgebraic k u) (hroot : (MvPolynomial.aeval ![u, y]) φ = 0) : IsAlgebraic k y

If φ ∈ k[X₀, X₁] has coefficient 1 on X₁ ^ φ.totalDegree (so it is monic in X₁ over k[X₀]), φ(u, y) = 0 and u is algebraic over k, then y is algebraic over k.