Factorisation of Computable Bivariate Polynomials

Defines evalYPoly (substitute Y ↦ f(X)), isLinearYFactor (test divisibility by Y - f(X)), and divByLinearY (synthetic division of a bivariate polynomial by the monic linear factor Y - f(X)).

divByLinearY is the computable factor theorem for the nested representation CBivariate R = CPolynomial (CPolynomial R): given a root f(X), it deflates Q by Y - f(X) over an arbitrary commutative ring. It is the degree-one special case of monic Euclidean division; division by an arbitrary monic divisor in Y is available generically through CPolynomial.divByMonic / CPolynomial.modByMonic over the coefficient ring CPolynomial R (see CPolynomial.modByMonic_add_mul_divByMonic).

def CompPoly.CBivariate.evalYPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (f : CPolynomial R) (Q : CBivariate R) : CPolynomial R

Substitute Y ↦ f(X) into a bivariate polynomial Q, i.e. evaluate Q at f in the Y variable. The result is the univariate polynomial Q(X, f(X)).

def CompPoly.CBivariate.isLinearYFactor {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (f : CPolynomial R) : Bool

Decide whether Y - f(X) divides Q, i.e. whether Q(X, f(X)) = 0. By the factor theorem this is exactly the test for f(X) being a Y-root of Q.

theorem CompPoly.CBivariate.evalYPoly_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (f : CPolynomial R) : evalYPoly f 0 = 0

evalYPoly sends the zero polynomial to 0.

theorem CompPoly.CBivariate.evalYPoly_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (f : CPolynomial R) (P Q : CBivariate R) : evalYPoly f (P + Q) = evalYPoly f P + evalYPoly f Q

evalYPoly is additive in the polynomial being evaluated.

theorem CompPoly.CBivariate.isLinearYFactor_iff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (f : CPolynomial R) : Q.isLinearYFactor f = true ↔ evalYPoly f Q = 0

The isLinearYFactor boolean test agrees with the proposition Q(X, f(X)) = 0.

theorem CompPoly.CBivariate.evalYPoly_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CPolynomial R) (Q : CBivariate R) : (evalYPoly f Q).toPoly = Polynomial.eval f.toPoly Q.toPoly

Bridge to Mathlib: evaluating Q at f and mapping to Polynomial R agrees with evaluating the mapped toPoly Q : R[X][Y] at f.toPoly.

def CompPoly.CBivariate.divByLinearY {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (Q : CBivariate R) (f : CPolynomial R) : CBivariate R × CPolynomial R

Synthetic (Horner) division of a bivariate polynomial Q by the linear factor Y - f(X), performed in the Y variable. Returns the pair (quotient, remainder) where the quotient is a CBivariate R and the remainder is a CPolynomial R.

Writing Q = Σ_{j=0}^n aⱼ Yʲ with aⱼ = coeff Q j, the quotient coefficients bⱼ and the remainder r satisfy the synthetic-division recurrence b_{n-1} = aₙ, b_{j-1} = aⱼ + f · bⱼ, r = a₀ + f · b₀, so that Q = quotient · (Y - f) + r. See divByLinearY_spec.

theorem CompPoly.CBivariate.divByLinearY_const {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (a f : CPolynomial R) : divByLinearY (CPolynomial.C a) f = (0, a)

theorem CompPoly.CBivariate.divByLinearY_zero {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (f : CPolynomial R) : divByLinearY 0 f = (0, 0)

theorem CompPoly.CBivariate.divByLinearY_spec {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (f : CPolynomial R) : have quot := (Q.divByLinearY f).1; have rem := (Q.divByLinearY f).2; Q.toPoly = quot.toPoly * (Polynomial.X - Polynomial.C f.toPoly) + Polynomial.C rem.toPoly

Correctness of divByLinearY: in R[X][Y] the computed quotient and remainder satisfy the Euclidean division identity Q = quotient · (Y - f) + remainder, over any commutative ring.

theorem CompPoly.CBivariate.divByLinearY_rem_eq_eval {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (f : CPolynomial R) : (Q.divByLinearY f).2 = evalYPoly f Q

The remainder of dividing Q by Y - f is the substitution Q(X, f(X)) (evalYPoly f Q), by the factor/remainder theorem.

theorem CompPoly.CBivariate.divByLinearY_exact {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] [DecidableEq R] (Q : CBivariate R) (f : CPolynomial R) (h : Q.isLinearYFactor f = true) : (Q.divByLinearY f).2 = 0

If Y - f divides Q (isLinearYFactor Q f), the division is exact: the remainder is 0.