Bivariate polynomials

This file introduces the notation R[X][Y] for the polynomial ring R[X][X] in two variables, and the notation Y for the second variable, in the Polynomial.Bivariate scope.

It also defines Polynomial.evalEval for the evaluation of a bivariate polynomial at a point on the affine plane, which is a ring homomorphism (Polynomial.evalEvalRingHom), as well as the abbreviation CC to view a constant in the base ring R as a bivariate polynomial.

def Polynomial.Bivariate.termY : Lean.ParserDescr

The notation Y for X in the Polynomial scope.

def Polynomial.Bivariate.«term_[X][Y]» : Lean.TrailingParserDescr

The notation R[X][Y] for R[X][X] in the Polynomial scope.

@[reducible, inline]

abbrev Polynomial.evalEval {R : Type u_1} [Semiring R] (x y : R) (p : Polynomial (Polynomial R)) : R

evalEval x y p is the evaluation p(x,y) of a two-variable polynomial p : R[X][Y].

@[reducible, inline]

abbrev Polynomial.CC {R : Type u_1} [Semiring R] (r : R) : Polynomial (Polynomial R)

A constant viewed as a polynomial in two variables.

theorem Polynomial.evalEval_C {R : Type u_1} [Semiring R] (x y : R) (p : Polynomial R) : evalEval x y (C p) = eval x p

theorem Polynomial.evalEval_map_C {R : Type u_1} [Semiring R] (x y : R) (p : Polynomial R) : evalEval x y (map C p) = eval y p

@[simp]

theorem Polynomial.evalEval_CC {R : Type u_1} [Semiring R] (x y p : R) : evalEval x y (CC p) = p

@[simp]

theorem Polynomial.evalEval_zero {R : Type u_1} [Semiring R] (x y : R) : evalEval x y 0 = 0

@[simp]

theorem Polynomial.evalEval_one {R : Type u_1} [Semiring R] (x y : R) : evalEval x y 1 = 1

@[simp]

theorem Polynomial.evalEval_natCast {R : Type u_1} [Semiring R] (x y : R) (n : ℕ) : evalEval x y ↑n = ↑n

@[simp]

theorem Polynomial.evalEval_X {R : Type u_1} [Semiring R] (x y : R) : evalEval x y X = y

@[simp]

theorem Polynomial.evalEval_add {R : Type u_1} [Semiring R] (x y : R) (p q : Polynomial (Polynomial R)) : evalEval x y (p + q) = evalEval x y p + evalEval x y q

theorem Polynomial.evalEval_sum {R : Type u_1} [Semiring R] (x y : R) (p : Polynomial R) (f : ℕ → R → Polynomial (Polynomial R)) : evalEval x y (p.sum f) = p.sum fun (n : ℕ) (a : R) => evalEval x y (f n a)

theorem Polynomial.evalEval_finset_sum {R : Type u_1} [Semiring R] {ι : Type u_3} (s : Finset ι) (x y : R) (f : ι → Polynomial (Polynomial R)) : evalEval x y (∑ i ∈ s, f i) = ∑ i ∈ s, evalEval x y (f i)

@[simp]

theorem Polynomial.evalEval_smul {R : Type u_1} {S : Type u_2} [Semiring R] [DistribSMul S R] [IsScalarTower S R R] (x y : R) (s : S) (p : Polynomial (Polynomial R)) : evalEval x y (s • p) = s • evalEval x y p

theorem Polynomial.evalEval_surjective {R : Type u_1} [Semiring R] (x y : R) : Function.Surjective (evalEval x y)

@[simp]

theorem Polynomial.evalEval_neg {R : Type u_1} [Ring R] (x y : R) (p : Polynomial (Polynomial R)) : evalEval x y (-p) = -evalEval x y p

@[simp]

theorem Polynomial.evalEval_sub {R : Type u_1} [Ring R] (x y : R) (p q : Polynomial (Polynomial R)) : evalEval x y (p - q) = evalEval x y p - evalEval x y q

@[simp]

theorem Polynomial.evalEval_intCast {R : Type u_1} [Ring R] (x y : R) (n : ℤ) : evalEval x y ↑n = ↑n

@[simp]

theorem Polynomial.evalEval_mul {R : Type u_1} [CommSemiring R] (x y : R) (p q : Polynomial (Polynomial R)) : evalEval x y (p * q) = evalEval x y p * evalEval x y q

theorem Polynomial.evalEval_prod {R : Type u_1} [CommSemiring R] {ι : Type u_3} (s : Finset ι) (x y : R) (p : ι → Polynomial (Polynomial R)) : evalEval x y (∏ j ∈ s, p j) = ∏ j ∈ s, evalEval x y (p j)

theorem Polynomial.evalEval_list_prod {R : Type u_1} [CommSemiring R] (x y : R) (l : List (Polynomial (Polynomial R))) : evalEval x y l.prod = (List.map (evalEval x y) l).prod

theorem Polynomial.evalEval_multiset_prod {R : Type u_1} [CommSemiring R] (x y : R) (l : Multiset (Polynomial (Polynomial R))) : evalEval x y l.prod = (Multiset.map (evalEval x y) l).prod

@[simp]

theorem Polynomial.evalEval_pow {R : Type u_1} [CommSemiring R] (x y : R) (p : Polynomial (Polynomial R)) (n : ℕ) : evalEval x y (p ^ n) = evalEval x y p ^ n

theorem Polynomial.evalEval_dvd {R : Type u_1} [CommSemiring R] (x y : R) {p q : Polynomial (Polynomial R)} : p ∣ q → evalEval x y p ∣ evalEval x y q

theorem Polynomial.coe_algebraMap_eq_CC {R : Type u_1} [CommSemiring R] : ⇑(algebraMap R (Polynomial (Polynomial R))) = CC

@[reducible, inline]

abbrev Polynomial.evalEvalRingHom {R : Type u_1} [CommSemiring R] (x y : R) : Polynomial (Polynomial R) →+* R

evalEval x y as a ring homomorphism.

@[simp]

theorem Polynomial.evalEvalRingHom_apply {R : Type u_1} [CommSemiring R] (x y : R) (a✝ : Polynomial (Polynomial R)) : (evalEvalRingHom x y) a✝ = eval x (eval (C y) a✝)

theorem Polynomial.coe_evalEvalRingHom {R : Type u_1} [CommSemiring R] (x y : R) : ⇑(evalEvalRingHom x y) = evalEval x y

theorem Polynomial.evalEvalRingHom_eq {R : Type u_1} [CommSemiring R] (x : R) : evalEvalRingHom x = eval₂RingHom (evalRingHom x)

theorem Polynomial.eval₂_evalRingHom {R : Type u_1} [CommSemiring R] (x : R) : eval₂ (evalRingHom x) = evalEval x

theorem Polynomial.map_evalRingHom_eval {R : Type u_1} [CommSemiring R] (x y : R) (p : Polynomial (Polynomial R)) : eval y (map (evalRingHom x) p) = evalEval x y p

theorem Polynomial.map_mapRingHom_eval_map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial (Polynomial R)) (q : Polynomial R) : eval (map f q) (map (mapRingHom f) p) = map f (eval q p)

theorem Polynomial.map_mapRingHom_eval_map_eval {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial (Polynomial R)) (q : Polynomial R) (r : R) : eval (f r) (eval (map f q) (map (mapRingHom f) p)) = f (eval r (eval q p))

theorem Polynomial.map_mapRingHom_evalEval {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial (Polynomial R)) (x y : R) : evalEval (f x) (f y) (map (mapRingHom f) p) = f (evalEval x y p)

theorem Polynomial.eval₂RingHom_eval₂RingHom {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x y : S) : eval₂RingHom (eval₂RingHom f x) y = (evalEvalRingHom x y).comp (mapRingHom (mapRingHom f))

Two equivalent ways to express the evaluation of a bivariate polynomial over R at a point in the affine plane over an R-algebra S.

theorem Polynomial.eval₂_eval₂RingHom_apply {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x y : S) (p : Polynomial (Polynomial R)) : eval₂ (eval₂RingHom f x) y p = evalEval x y (map (mapRingHom f) p)

theorem Polynomial.eval_C_X_comp_eval₂_map_C_X {R : Type u_1} [CommSemiring R] : (evalRingHom (C X)).comp (eval₂RingHom (mapRingHom (algebraMap R (Polynomial (Polynomial R)))) (C X)) = RingHom.id (Polynomial (Polynomial R))

theorem Polynomial.eval_C_X_eval₂_map_C_X {R : Type u_1} [CommSemiring R] {p : Polynomial (Polynomial R)} : eval (C X) (eval₂ (mapRingHom (algebraMap R (Polynomial (Polynomial R)))) (C X) p) = p

Viewing R[X,Y,X'] as an R[X']-algebra, a polynomial p : R[X',Y'] can be evaluated at Y : R[X,Y,X'] (substitution of Y' by Y), obtaining another polynomial in R[X,Y,X']. When this polynomial is then evaluated at X' = X, the original polynomial p is recovered.

@[reducible, inline]

abbrev Polynomial.aevalAeval {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (x y : A) : Polynomial (Polynomial R) →ₐ[R] A

aevalAeval x y is the R-algebra evaluation morphism sending a two-variable polynomial p : R[X][Y] to p(x,y).

theorem Polynomial.coe_aevalAeval_eq_evalEval {A : Type u_2} [CommSemiring A] (x y : A) : ⇑(aevalAeval x y) = evalEval x y

def Polynomial.Bivariate.swap {R : Type u_1} [CommSemiring R] : Polynomial (Polynomial R) ≃ₐ[R] Polynomial (Polynomial R)

The R-algebra automorphism given by X ↦ Y and Y ↦ X.

@[simp]

theorem Polynomial.Bivariate.swap_apply {R : Type u_1} [CommSemiring R] (p : Polynomial (Polynomial R)) : swap p = (aevalAeval X (C X)) p

theorem Polynomial.Bivariate.swap_X {R : Type u_1} [CommSemiring R] : swap (C X) = X

theorem Polynomial.Bivariate.swap_Y {R : Type u_1} [CommSemiring R] : swap X = C X

theorem Polynomial.Bivariate.swap_C_C {R : Type u_1} [CommSemiring R] (r : R) : swap (C (C r)) = C (C r)

theorem Polynomial.Bivariate.swap_C {R : Type u_1} [CommSemiring R] (f : Polynomial R) : swap (C f) = map C f

theorem Polynomial.Bivariate.swap_map_C {R : Type u_1} [CommSemiring R] (f : Polynomial R) : swap (map C f) = C f

theorem Polynomial.Bivariate.swap_monomial_monomial {R : Type u_1} [CommSemiring R] (n m : ℕ) (r : R) : swap ((monomial n) ((monomial m) r)) = (monomial m) ((monomial n) r)

theorem Polynomial.Bivariate.aevalAeval_swap {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (x y : A) (p : Polynomial (Polynomial R)) : (aevalAeval x y) (swap p) = (aevalAeval y x) p

Evaluating swap p at x, y is the same as evaluating p at y x.

theorem Polynomial.Bivariate.aveal_eq_map_swap {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (x : A) (p : Polynomial (Polynomial R)) : (aeval (C x)) p = (mapAlgHom (aeval x)) (swap p)

noncomputable def Polynomial.Bivariate.equivMvPolynomial (R : Type u_1) [CommSemiring R] : Polynomial (Polynomial R) ≃ₐ[R] MvPolynomial (Fin 2) R

The equiv between R[X][Y] and R[X, Y].

@[simp]

theorem Polynomial.Bivariate.equivMvPolynomial_C_C {R : Type u_1} [CommSemiring R] {a : R} : (equivMvPolynomial R) (C (C a)) = MvPolynomial.C a

@[simp]

theorem Polynomial.Bivariate.equivMvPolynomial_C_X {R : Type u_1} [CommSemiring R] : (equivMvPolynomial R) (C X) = MvPolynomial.X 0

@[simp]

theorem Polynomial.Bivariate.equivMvPolynomial_X {R : Type u_1} [CommSemiring R] : (equivMvPolynomial R) X = MvPolynomial.X 1

@[simp]

theorem Polynomial.Bivariate.equivMvPolynomial_symm_X_0 {R : Type u_1} [CommSemiring R] : (equivMvPolynomial R).symm (MvPolynomial.X 0) = C X

@[simp]

theorem Polynomial.Bivariate.equivMvPolynomial_symm_X_1 {R : Type u_1} [CommSemiring R] : (equivMvPolynomial R).symm (MvPolynomial.X 1) = X

@[simp]

theorem Polynomial.Bivariate.equivMvPolynomial_symm_C {R : Type u_1} [CommSemiring R] (a : R) : (equivMvPolynomial R).symm (MvPolynomial.C a) = C (C a)

theorem Polynomial.Bivariate.pderiv_zero_equivMvPolynomial {R : Type u_2} [CommRing R] (p : Polynomial (Polynomial R)) : (MvPolynomial.pderiv 0) ((equivMvPolynomial R) p) = (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs p))

@[deprecated Polynomial.Bivariate.pderiv_zero_equivMvPolynomial (since := "2025-12-09")]

theorem Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial {R : Type u_2} [CommRing R] (p : Polynomial (Polynomial R)) : (MvPolynomial.pderiv 0) ((equivMvPolynomial R) p) = (equivMvPolynomial R) (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs p))

Alias of Polynomial.Bivariate.pderiv_zero_equivMvPolynomial.

theorem Polynomial.Bivariate.pderiv_one_equivMvPolynomial {R : Type u_1} [CommSemiring R] (p : Polynomial (Polynomial R)) : (MvPolynomial.pderiv 1) ((equivMvPolynomial R) p) = (equivMvPolynomial R) (derivative p)

@[deprecated Polynomial.Bivariate.pderiv_one_equivMvPolynomial (since := "2025-12-09")]

theorem Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial {R : Type u_1} [CommSemiring R] (p : Polynomial (Polynomial R)) : (MvPolynomial.pderiv 1) ((equivMvPolynomial R) p) = (equivMvPolynomial R) (derivative p)

Alias of Polynomial.Bivariate.pderiv_one_equivMvPolynomial.

noncomputable def AdjoinRoot.evalEval {R : Type u_1} [CommRing R] {x y : R} {p : Polynomial (Polynomial R)} (h : Polynomial.evalEval x y p = 0) : AdjoinRoot p →+* R

If the evaluation (evalEval) of a bivariate polynomial p : R[X][Y] at a point (x,y) is zero, then Polynomial.evalEval x y factors through AdjoinRoot.evalEval, a ring homomorphism from AdjoinRoot p to R.

@[simp]

theorem AdjoinRoot.evalEval_apply {R : Type u_1} [CommRing R] {x y : R} {p : Polynomial (Polynomial R)} (h : Polynomial.evalEval x y p = 0) (a✝ : Polynomial (Polynomial R) ⧸ Submodule.toAddSubgroup (Ideal.span {p})) : (evalEval h) a✝ = (QuotientAddGroup.lift (Submodule.toAddSubgroup (Ideal.span {p})) ↑(Polynomial.eval₂RingHom (Polynomial.evalRingHom x) y) ⋯) a✝

theorem AdjoinRoot.evalEval_mk {R : Type u_1} [CommRing R] {x y : R} {p : Polynomial (Polynomial R)} (h : Polynomial.evalEval x y p = 0) (g : Polynomial (Polynomial R)) : (evalEval h) ((mk p) g) = Polynomial.evalEval x y g