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 : 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.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.«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 : R) (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 : R) (y : R) (p : Polynomial R) : Polynomial.evalEval x y (Polynomial.C p) = Polynomial.eval x p

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

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

@[simp]

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

@[reducible, inline]

abbrev Polynomial.evalEvalRingHom {R : Type u_1} [CommSemiring R] (x : R) (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))

theorem Polynomial.coe_evalEvalRingHom {R : Type u_1} [CommSemiring R] (x : R) (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 : R) (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 : R) (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 : S) (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 : S) (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.

@[simp]

theorem AdjoinRoot.evalEval_apply {R : Type u_1} [CommRing R] {x : R} {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

def AdjoinRoot.evalEval {R : Type u_1} [CommRing R] {x : R} {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 ⋯

theorem AdjoinRoot.evalEval_mk {R : Type u_1} [CommRing R] {x : R} {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