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 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.termY.delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def Polynomial.termY : Lean.ParserDescr

The notation Y for X in the Polynomial scope.

Equations

• Polynomial.termY = Lean.ParserDescr.node `Polynomial.termY 1024 (Lean.ParserDescr.symbol "Y")

def Polynomial.«term_[X][Y]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Polynomial.«term_[X][Y]» = Lean.ParserDescr.trailingNode `Polynomial.«term_[X][Y]» 1024 0 (Lean.ParserDescr.symbol "[X][Y]")

@[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].

Equations

• Polynomial.evalEval x y p = Polynomial.eval x (Polynomial.eval (Polynomial.C y) p)

@[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.

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Polynomial.evalEval_add {R : Type u_1} [Semiring R] (x y : R) (p q : Polynomial (Polynomial R)) : Polynomial.evalEval x y (p + q) = Polynomial.evalEval x y p + Polynomial.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)) : Polynomial.evalEval x y (p.sum f) = p.sum fun (n : ℕ) (a : R) => Polynomial.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)) : Polynomial.evalEval x y (∑ i ∈ s, f i) = ∑ i ∈ s, Polynomial.evalEval x y (f i)

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Polynomial.evalEval_mul {R : Type u_1} [CommSemiring R] (x y : R) (p q : Polynomial (Polynomial R)) : Polynomial.evalEval x y (p * q) = Polynomial.evalEval x y p * Polynomial.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)) : Polynomial.evalEval x y (∏ j ∈ s, p j) = ∏ j ∈ s, Polynomial.evalEval x y (p j)

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

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

@[simp]

theorem Polynomial.evalEval_pow {R : Type u_1} [CommSemiring R] (x y : R) (p : Polynomial (Polynomial R)) (n : ℕ) : Polynomial.evalEval x y (p ^ n) = Polynomial.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 → Polynomial.evalEval x y p ∣ Polynomial.evalEval x y q

theorem Polynomial.coe_algebraMap_eq_CC {R : Type u_1} [CommSemiring R] : ⇑(algebraMap R (Polynomial (Polynomial R))) = Polynomial.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.

Equations

• Polynomial.evalEvalRingHom x y = (Polynomial.evalRingHom x).comp (Polynomial.evalRingHom (Polynomial.C y))

@[simp]

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

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

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

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

theorem Polynomial.map_evalRingHom_eval {R : Type u_1} [CommSemiring R] (x y : R) (p : Polynomial (Polynomial R)) : Polynomial.eval y (Polynomial.map (Polynomial.evalRingHom x) p) = Polynomial.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) : Polynomial.eval (Polynomial.map f q) (Polynomial.map (Polynomial.mapRingHom f) p) = Polynomial.map f (Polynomial.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) : Polynomial.eval (f r) (Polynomial.eval (Polynomial.map f q) (Polynomial.map (Polynomial.mapRingHom f) p)) = f (Polynomial.eval r (Polynomial.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) : Polynomial.evalEval (f x) (f y) (Polynomial.map (Polynomial.mapRingHom f) p) = f (Polynomial.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) : Polynomial.eval₂RingHom (Polynomial.eval₂RingHom f x) y = (Polynomial.evalEvalRingHom x y).comp (Polynomial.mapRingHom (Polynomial.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)) : Polynomial.eval₂ (Polynomial.eval₂RingHom f x) y p = Polynomial.evalEval x y (Polynomial.map (Polynomial.mapRingHom f) p)

theorem Polynomial.eval_C_X_comp_eval₂_map_C_X {R : Type u_1} [CommSemiring R] : (Polynomial.evalRingHom (Polynomial.C Polynomial.X)).comp (Polynomial.eval₂RingHom (Polynomial.mapRingHom (algebraMap R (Polynomial (Polynomial R)))) (Polynomial.C Polynomial.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)} : Polynomial.eval (Polynomial.C Polynomial.X) (Polynomial.eval₂ (Polynomial.mapRingHom (algebraMap R (Polynomial (Polynomial R)))) (Polynomial.C Polynomial.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.

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.

Equations

• AdjoinRoot.evalEval h = AdjoinRoot.lift (Polynomial.evalRingHom x) y ⋯

@[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})) : (AdjoinRoot.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)) : (AdjoinRoot.evalEval h) ((AdjoinRoot.mk p) g) = Polynomial.evalEval x y g