Equivalence with Mathlib Bivariate Polynomials #

This file establishes the conversion from CBivariate R to Mathlib's R[X][Y] (Polynomial (Polynomial R)).

Main definitions:

toPoly: converts CBivariate R to R[X][Y]
ofPoly: converts R[X][Y] back to CBivariate R

Main results:

round-trip identities: ofPoly_toPoly, toPoly_ofPoly
ring equivalence: ringEquiv
API correctness lemmas for evaluation, coefficients, support, and degrees

Core conversion lemmas between CBivariate R and R[X][Y].

source

noncomputable def CompPoly.CBivariate.toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Semiring R] (p : CBivariate R) :

Polynomial (Polynomial R)

Convert CBivariate R to Mathlib's bivariate polynomial R[X][Y].

Maps each Y-coefficient through CPolynomial.toPoly, then builds Polynomial (Polynomial R) as the sum of monomials.

Instances For

source

def CompPoly.CBivariate.ofPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] [Semiring (Polynomial R)] (p : Polynomial (Polynomial R)) :

CBivariate R

Convert Mathlib's R[X][Y] to CBivariate R (inverse of toPoly).

Extracts each Y-coefficient via p.coeff, converts to CPolynomial R via toImpl and trimming, then builds the canonical bivariate sum.

Instances For

source

theorem CompPoly.CBivariate.toPoly_add {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (p q : CBivariate R) :

(p + q).toPoly = p.toPoly + q.toPoly

toPoly preserves addition.

source

theorem CompPoly.CBivariate.toPoly_monomial {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (n : ℕ) (c : CPolynomial R) :

toPoly (CPolynomial.monomial n c) = (Polynomial.monomial n) c.toPoly

toPoly sends a Y-monomial to the corresponding monomial in R[X][Y].

source

theorem CompPoly.CBivariate.ofPoly_monomial {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (n : ℕ) (c : Polynomial R) :

ofPoly ((Polynomial.monomial n) c) = CPolynomial.monomial n ⟨c.toImpl, ⋯⟩

ofPoly sends a Y-monomial in R[X][Y] to a bivariate monomial.

source

theorem CompPoly.CBivariate.toImpl_add {R : Type u_1} [BEq R] [LawfulBEq R] [Semiring R] (p q : Polynomial R) :

p.toImpl + q.toImpl = (p + q).toImpl

Polynomial.toImpl preserves addition, accounting for trimming in the raw representation.

source

theorem CompPoly.CBivariate.ofPoly_add {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p q : Polynomial (Polynomial R)) :

ofPoly (p + q) = ofPoly p + ofPoly q

ofPoly preserves addition in R[X][Y].

source

theorem CompPoly.CBivariate.ofPoly_coeff {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p : Polynomial (Polynomial R)) (n : ℕ) :

(CPolynomial.coeff (ofPoly p) n).toPoly = p.coeff n

The outer coefficient of ofPoly p converts back to the corresponding R[X] coefficient.

source

theorem CompPoly.CBivariate.toPoly_coeff {R : Type u_1} [BEq R] [LawfulBEq R] [Semiring R] (p : CBivariate R) (n : ℕ) :

p.toPoly.coeff n = (CPolynomial.coeff p n).toPoly

The outer coefficient of toPoly p is CPolynomial.coeff p n converted to R[X].

source

theorem CompPoly.CBivariate.toPoly_eq_map {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (p : CBivariate R) :

p.toPoly = Polynomial.map (↑CPolynomial.ringEquiv) (CPolynomial.toPoly p)

toPoly is the map of the outer polynomial via CPolynomial.ringEquiv.

source

theorem CompPoly.CBivariate.toPoly_mul {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (p q : CBivariate R) :

(p * q).toPoly = p.toPoly * q.toPoly

toPoly preserves multiplication.

Ring equivalence between bivariate representations.

source

theorem CompPoly.CBivariate.ofPoly_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p : Polynomial (Polynomial R)) :

(ofPoly p).toPoly = p

Round-trip from Mathlib: converting a polynomial to CBivariate and back is the identity.

source

theorem CompPoly.CBivariate.toPoly_ofPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p : CBivariate R) :

ofPoly p.toPoly = p

Round-trip from CBivariate: converting to Mathlib and back is the identity.

source

noncomputable def CompPoly.CBivariate.ringEquiv {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :

CBivariate R ≃+* Polynomial (Polynomial R)

Ring equivalence between CBivariate R and Mathlib's R[X][Y].

Instances For

source

theorem CompPoly.CBivariate.toPoly_one {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :

toPoly 1 = 1

toPoly preserves 1.

source

theorem CompPoly.CBivariate.ofPoly_one {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :

ofPoly 1 = 1

ofPoly preserves 1.

source

theorem CompPoly.CBivariate.toPoly_zero {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] :

toPoly 0 = 0

toPoly maps the zero bivariate polynomial to 0.

source

theorem CompPoly.CBivariate.ofPoly_zero {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :

ofPoly 0 = 0

ofPoly maps 0 in R[X][Y] to the zero bivariate polynomial.

source

noncomputable def CompPoly.CBivariate.toPolyRingHom {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :

CBivariate R →+* Polynomial (Polynomial R)

Ring hom from computable bivariates to Mathlib bivariates.

Instances For

source

noncomputable def CompPoly.CBivariate.ofPolyRingHom {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :

Polynomial (Polynomial R) →+* CBivariate R

Ring hom from Mathlib bivariates to computable bivariates.

Instances For

source

theorem CompPoly.CBivariate.ofPoly_mul {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (p q : Polynomial (Polynomial R)) :

ofPoly (p * q) = ofPoly p * ofPoly q

ofPoly preserves multiplication.

Shared helper: foldl-to-Finset.sum equivalence #

Correctness lemmas for evaluation, coefficients, support, and degrees.

source

theorem CompPoly.CBivariate.evalEval_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (x y : R) (f : CBivariate R) :

evalEval x y f = Polynomial.evalEval x y f.toPoly

toPoly preserves full evaluation: evalEval x y f = (toPoly f).evalEval x y.

source

theorem CompPoly.CBivariate.coeff_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) (i j : ℕ) :

(f.toPoly.coeff j).coeff i = f.coeff i j

toPoly preserves coefficients: coefficient of X^i Y^j matches.

source

theorem CompPoly.CBivariate.support_toPoly_outer {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :

f.toPoly.support = f.supportY

The outer support of toPoly f equals the Y-support of f.

source

theorem CompPoly.CBivariate.natDegreeY_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :

f.toPoly.natDegree = f.natDegreeY

toPoly preserves Y-degree.

source

theorem CompPoly.CBivariate.coeff_toPoly_Y {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) (j : ℕ) :

f.toPoly.coeff j = ((↑f).coeff j).toPoly

The outer Y-coefficient formula used for X-degree transport.

source

theorem CompPoly.CBivariate.natDegreeX_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :

(f.toPoly.support.sup fun (j : ℕ) => (f.toPoly.coeff j).natDegree) = f.natDegreeX

toPoly preserves X-degree (max over Y-coefficients of their degree in X).

source

theorem CompPoly.CBivariate.CC_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (r : R) :

(CC r).toPoly = Polynomial.C (Polynomial.C r)

CC corresponds to the nested constant polynomial in R[X][Y].

source

theorem CompPoly.CBivariate.X_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] :

X.toPoly = Polynomial.C Polynomial.X

X (inner variable) corresponds to Polynomial.C Polynomial.X in R[X][Y].

source

theorem CompPoly.CBivariate.Y_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] :

Y.toPoly = Polynomial.X

Y (outer variable) corresponds to Polynomial.X in R[X][Y].

source

theorem CompPoly.CBivariate.monomialXY_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (n m : ℕ) (c : R) :

(monomialXY n m c).toPoly = (Polynomial.monomial m) ((Polynomial.monomial n) c)

monomialXY n m c corresponds to Y^m with inner coefficient X^n * c.

source

theorem CompPoly.CBivariate.supportX_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :

f.supportX = f.toPoly.support.biUnion fun (j : ℕ) => (f.toPoly.coeff j).support

supportX corresponds to the union of inner supports of outer coefficients.

source

theorem CompPoly.CBivariate.totalDegree_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :

f.totalDegree = f.toPoly.support.sup fun (j : ℕ) => (f.toPoly.coeff j).natDegree + j

totalDegree corresponds to the supremum over j of natDegree ((toPoly f).coeff j) + j.

source

theorem CompPoly.CBivariate.evalX_toPoly_coeff {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (a : R) (f : CBivariate R) (j : ℕ) :

(evalX a f).toPoly.coeff j = Polynomial.eval a (f.toPoly.coeff j)

evalX a evaluates each inner coefficient at a.

source

theorem CompPoly.CBivariate.evalX_toPoly_eval_commute {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (a y : R) (hc : Commute a y) (f : CBivariate R) :

CPolynomial.eval y (evalX a f) = Polynomial.evalEval a y f.toPoly

evalX is compatible with full bivariate evaluation when a and y commute.

source

theorem CompPoly.CBivariate.evalX_toPoly_eval {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [CommSemiring R] [DecidableEq R] (a y : R) (f : CBivariate R) :

CPolynomial.eval y (evalX a f) = Polynomial.evalEval a y f.toPoly

evalX_toPoly_eval_commute specialized to commutative rings.

source

theorem CompPoly.CBivariate.evalX_toPoly_eval_commute_converse {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (a y : R) (h : ∀ (f : CBivariate R), CPolynomial.eval y (evalX a f) = Polynomial.evalEval a y f.toPoly) :

Commute a y

The Commute hypothesis in evalX_toPoly_eval_commute is necessary: if the identity holds for every bivariate polynomial then a and y commute.

source

theorem CompPoly.CBivariate.evalY_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (a : R) (f : CBivariate R) :

(evalY a f).toPoly = Polynomial.eval (Polynomial.C a) f.toPoly

evalY a corresponds to outer evaluation at Polynomial.C a.

source

theorem CompPoly.CBivariate.leadingCoeffY_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] (f : CBivariate R) :

f.leadingCoeffY.toPoly = f.toPoly.leadingCoeff

leadingCoeffY corresponds to the leading coefficient in the outer variable.

source

theorem CompPoly.CBivariate.swap_toPoly_coeff {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (f : CBivariate R) (i j : ℕ) :

(f.swap.toPoly.coeff j).coeff i = (f.toPoly.coeff i).coeff j

swap exchanges X- and Y-exponents.

source

theorem CompPoly.CBivariate.leadingCoeffX_toPoly {R : Type u_1} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] [DecidableEq R] (f : CBivariate R) :

f.leadingCoeffX.toPoly = f.swap.toPoly.leadingCoeff

leadingCoeffX is the Y-leading coefficient of the swapped polynomial.

Documentation

CompPoly.Bivariate.ToPoly

Equivalence with Mathlib Bivariate Polynomials #

Shared helper: foldl-to-Finset.sum equivalence #