Singling out an arbitrary variable of a polynomial ring in n + 1 variables

Mathlib's MvPolynomial.finSuccEquiv identifies R[X₀, …, Xₙ] with the polynomial ring in the variable X₀ over R[X₁, …, Xₙ]. This file does the same with an arbitrary variable Xₚ singled out: the remaining variables are indexed by Fin n through p.succAbove, as in the equivalence finSuccEquiv' p : Fin (n + 1) ≃ Option (Fin n).

This is the form in which a polynomial ring acquires one new variable in the middle of its list, as happens to the coefficient ring of a grid complex when a grid diagram is stabilized.

Main definitions

• MvPolynomial.finSuccEquiv': the R-algebra isomorphism R[X₀, …, Xₙ] ≃ R[X_{p.succAbove 0}, …, X_{p.succAbove (n-1)}][Xₚ].

Main results

• MvPolynomial.finSuccEquiv'_X_self, MvPolynomial.finSuccEquiv'_rename_succAbove: the singled-out variable goes to the polynomial variable, and the others are constants.
• MvPolynomial.polynomial_eval_finSuccEquiv': evaluating the polynomial variable at a substitutes a for X p.
• MvPolynomial.finSuccEquiv'_zero: for p = 0 this is Mathlib's MvPolynomial.finSuccEquiv.
• MvPolynomial.finSuccEquiv'_map, MvPolynomial.finSuccEquiv_map: singling out a variable commutes with mapping the coefficients along a ring homomorphism.
• MvPolynomial.polynomial_eval_map_finSuccEquiv', MvPolynomial.polynomial_eval_map_finSuccEquiv: specializing the other variables to a point s and then evaluating the polynomial variable at y is evaluating at the point obtained by inserting y into s at position p.

The last two results are the compatibility of this equivalence with coefficient maps and with evaluation. They let a polynomial in n + 1 variables be treated as a family of univariate polynomials in X p parametrized by the other coordinates, with integer input mapped to the reals either before or after the variable is singled out.

Dually, the last variable Xₙ can be moved into the coefficients instead, through Mathlib's MvPolynomial.optionEquivRight after renaming along finSuccEquivLast. This identifies R[X₀, …, Xₙ] with the polynomials in X₀, …, Xₙ₋₁ whose coefficients are polynomials in Xₙ. The coefficient of Xᵘ then has as its coefficient of Xₙ ^ k the coefficient of f at the exponent Finsupp.snoc u k (MvPolynomial.optionEquivRight_rename_finSuccEquivLast_coeff_coeff). This is the form used for Lazard evaluation, where the base variables are eliminated first and the last variable is kept.

noncomputable def MvPolynomial.finSuccEquiv' (R : Type u_1) [CommSemiring R] {n : ℕ} (p : Fin (n + 1)) : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] Polynomial (MvPolynomial (Fin n) R)

The R-algebra isomorphism between polynomials in the variables Fin (n + 1) and polynomials in the variable X p over the polynomials in the other variables, which are indexed by Fin n through p.succAbove.

Equations

• MvPolynomial.finSuccEquiv' R p = (MvPolynomial.renameEquiv R (finSuccEquiv' p)).trans (MvPolynomial.optionEquivLeft R (Fin n))

@[simp]

theorem MvPolynomial.finSuccEquiv'_X_self {R : Type u_1} [CommSemiring R] {n : ℕ} (p : Fin (n + 1)) : (finSuccEquiv' R p) (X p) = Polynomial.X

The singled-out variable becomes the polynomial variable.

@[simp]

theorem MvPolynomial.finSuccEquiv'_X_succAbove {R : Type u_1} [CommSemiring R] {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : (finSuccEquiv' R p) (X (p.succAbove i)) = Polynomial.C (X i)

A variable other than the singled-out one becomes a constant.

@[simp]

theorem MvPolynomial.finSuccEquiv'_rename_succAbove {R : Type u_1} [CommSemiring R] {n : ℕ} (p : Fin (n + 1)) (f : MvPolynomial (Fin n) R) : (finSuccEquiv' R p) ((rename p.succAbove) f) = Polynomial.C f

Polynomials not involving the singled-out variable become constants.

@[simp]

theorem MvPolynomial.finSuccEquiv'_C {R : Type u_1} [CommSemiring R] {n : ℕ} (p : Fin (n + 1)) (r : R) : (finSuccEquiv' R p) (C r) = Polynomial.C (C r)

Constants stay constant.

@[simp]

theorem MvPolynomial.finSuccEquiv'_symm_X {R : Type u_1} [CommSemiring R] {n : ℕ} (p : Fin (n + 1)) : (finSuccEquiv' R p).symm Polynomial.X = X p

The polynomial variable comes from the singled-out variable.

@[simp]

theorem MvPolynomial.finSuccEquiv'_symm_C {R : Type u_1} [CommSemiring R] {n : ℕ} (p : Fin (n + 1)) (f : MvPolynomial (Fin n) R) : (finSuccEquiv' R p).symm (Polynomial.C f) = (rename p.succAbove) f

The constants come from the polynomials in the other variables.

theorem MvPolynomial.polynomial_eval_finSuccEquiv' {R : Type u_1} [CommSemiring R] {n : ℕ} (p : Fin (n + 1)) (a : MvPolynomial (Fin n) R) (f : MvPolynomial (Fin (n + 1)) R) : Polynomial.eval a ((finSuccEquiv' R p) f) = (aeval (p.insertNth a X)) f

Evaluating the singled-out variable at a is substituting a for X p and keeping the other variables.

theorem MvPolynomial.finSuccEquiv'_zero {R : Type u_1} [CommSemiring R] {n : ℕ} : finSuccEquiv' R 0 = finSuccEquiv R n

Singling out the variable X 0 is MvPolynomial.finSuccEquiv.

theorem MvPolynomial.finSuccEquiv'_map {R : Type u_1} [CommSemiring R] {n : ℕ} {S : Type u_2} [CommSemiring S] (φ : R →+* S) (p : Fin (n + 1)) (f : MvPolynomial (Fin (n + 1)) R) : (finSuccEquiv' S p) ((map φ) f) = Polynomial.map (map φ) ((finSuccEquiv' R p) f)

Singling out a variable commutes with mapping the coefficients along φ.

theorem MvPolynomial.finSuccEquiv'_symm_map {R : Type u_1} [CommSemiring R] {n : ℕ} {S : Type u_2} [CommSemiring S] (φ : R →+* S) (p : Fin (n + 1)) (f : Polynomial (MvPolynomial (Fin n) R)) : (finSuccEquiv' S p).symm (Polynomial.map (map φ) f) = (map φ) ((finSuccEquiv' R p).symm f)

Mapping the coefficients along φ commutes with the inverse of finSuccEquiv' R p.

theorem MvPolynomial.finSuccEquiv_map {R : Type u_1} [CommSemiring R] {n : ℕ} {S : Type u_2} [CommSemiring S] (φ : R →+* S) (f : MvPolynomial (Fin (n + 1)) R) : (finSuccEquiv S n) ((map φ) f) = Polynomial.map (map φ) ((finSuccEquiv R n) f)

Singling out the variable X 0 commutes with mapping the coefficients along φ.

theorem MvPolynomial.polynomial_eval_map_finSuccEquiv' {R : Type u_1} [CommSemiring R] {n : ℕ} {S : Type u_2} [CommSemiring S] (φ : R →+* S) (p : Fin (n + 1)) (s : Fin n → S) (y : S) (f : MvPolynomial (Fin (n + 1)) R) : Polynomial.eval y (Polynomial.map (eval₂Hom φ s) ((finSuccEquiv' R p) f)) = eval₂ φ (p.insertNth y s) f

Specializing the variables other than X p along φ at the point s, and then evaluating the polynomial variable at y, is evaluating along φ at the point obtained by inserting y into s at position p.

theorem MvPolynomial.polynomial_eval_map_finSuccEquiv {R : Type u_1} [CommSemiring R] {n : ℕ} {S : Type u_2} [CommSemiring S] (φ : R →+* S) (s : Fin n → S) (y : S) (f : MvPolynomial (Fin (n + 1)) R) : Polynomial.eval y (Polynomial.map (eval₂Hom φ s) ((finSuccEquiv R n) f)) = eval₂ φ (Fin.cons y s) f

Specializing the variables X 1, …, X n along φ at the point s, and then evaluating the polynomial variable at y, is evaluating along φ at the point Fin.cons y s.

theorem MvPolynomial.optionEquivRight_rename_finSuccEquivLast_monomial {R : Type u_1} [CommSemiring R] {n : ℕ} (d : Fin (n + 1) →₀ ℕ) (r : R) : (optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) ((monomial d) r)) = (monomial d.init) ((Polynomial.monomial (d (Fin.last n))) r)

Moving the last variable into the coefficients sends the monomial r • X ^ d to the monomial in the first n variables with exponent init d whose coefficient is r • Xₙ ^ d (Fin.last n).

theorem MvPolynomial.optionEquivRight_rename_finSuccEquivLast_coeff_coeff {R : Type u_1} [CommSemiring R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) (u : Fin n →₀ ℕ) (k : ℕ) : (((optionEquivRight R (Fin n)) ((rename ⇑finSuccEquivLast) f)).coeff u).coeff k = f.coeff (u.snoc k)

After moving the last variable into the coefficients, the coefficient of Xₙ ^ k in the coefficient of Xᵘ is the coefficient of f at the exponent Finsupp.snoc u k.