MvPolynomial Equiv

Equivalences for multivariable polynomials, including finSuccEquivNth.

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

The algebra isomorphism between multivariable polynomials in Fin (n + 1) and polynomials over multivariable polynomials in Fin n, where the p-th (pivot) variable is the indeterminate X.

finSuccEquiv is the special case when p = 0.

theorem MvPolynomial.finSuccEquivNth_eq {n : ℕ} (R : Type u_2) [CommSemiring R] (p : Fin (n + 1)) : ↑(finSuccEquivNth R p) = eval₂Hom (Polynomial.C.comp C) (p.insertNth Polynomial.X (⇑Polynomial.C ∘ X))

theorem MvPolynomial.finSuccEquivNth_apply {n : ℕ} (R : Type u_2) [CommSemiring R] (p : Fin (n + 1)) (f : MvPolynomial (Fin (n + 1)) R) : (finSuccEquivNth R p) f = (eval₂Hom (Polynomial.C.comp C) (p.insertNth Polynomial.X (⇑Polynomial.C ∘ X))) f

theorem MvPolynomial.finSuccEquivNth_comp_C_eq_C {n : ℕ} (R : Type u_2) [CommSemiring R] (p : Fin (n + 1)) : (↑(finSuccEquivNth R p).symm).comp (Polynomial.C.comp C) = C

@[simp]

theorem MvPolynomial.finSuccEquivNth_X_same {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} : (finSuccEquivNth R p) (X p) = Polynomial.X

@[simp]

theorem MvPolynomial.finSuccEquivNth_X_above {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} {i : Fin n} (h : p < i.succ) : (finSuccEquivNth R p) (X i.succ) = Polynomial.C (X i)

@[simp]

theorem MvPolynomial.finSuccEquivNth_X_below {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} {i : Fin n} (h : i.castSucc < p) : (finSuccEquivNth R p) (X i.castSucc) = Polynomial.C (X i)

theorem MvPolynomial.finSuccEquivNth_coeff_coeff {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} (m : Fin n →₀ ℕ) (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ) : coeff m (((finSuccEquivNth R p) f).coeff i) = coeff (Finsupp.insertNth p i m) f

The coefficient of m in the i-th coefficient of finSuccEquivNth R p f equals the coefficient of m.insertNth p i in f.

theorem MvPolynomial.eval_eq_eval_mv_eval_finSuccEquivNth {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} (s : Fin n → R) (y : R) (f : MvPolynomial (Fin (n + 1)) R) : (eval (p.insertNth y s)) f = Polynomial.eval y (Polynomial.map (eval s) ((finSuccEquivNth R p) f))

The evaluation of f at Fin.insertNth p y s equals the evaluation at y of the polynomial obtained by partially evaluating finSuccEquivNth R p f at s.

theorem MvPolynomial.support_coeff_finSuccEquivNth {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {m : Fin n →₀ ℕ} : m ∈ (((finSuccEquivNth R p) f).coeff i).support ↔ Finsupp.insertNth p i m ∈ f.support

A monomial index m is in the support of the i-th coefficient of finSuccEquivNth R p f if and only if m.insertNth p i is in the support of f.

theorem MvPolynomial.totalDegree_coeff_finSuccEquivNth_add_le {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ) (hi : ((finSuccEquivNth R p) f).coeff i ≠ 0) : (((finSuccEquivNth R p) f).coeff i).totalDegree + i ≤ f.totalDegree

The totalDegree of a multivariable polynomial f is at least i more than the totalDegree of the ith coefficient of finSuccEquivNth R p applied to f, if this is nonzero.

theorem MvPolynomial.support_finSuccEquivNth {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} (f : MvPolynomial (Fin (n + 1)) R) : ((finSuccEquivNth R p) f).support = Finset.image (fun (m : Fin (n + 1) →₀ ℕ) => m p) f.support

The support of finSuccEquivNth R p f equals the support of f projected onto the p-th variable.

theorem MvPolynomial.mem_support_finSuccEquivNth {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} {f : MvPolynomial (Fin (n + 1)) R} {x : ℕ} : x ∈ ((finSuccEquivNth R p) f).support ↔ x ∈ (fun (m : Fin (n + 1) →₀ ℕ) => m p) '' ↑f.support

theorem MvPolynomial.image_support_finSuccEquivNth {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} : Finset.image (Finsupp.insertNth p i) (((finSuccEquivNth R p) f).coeff i).support = {m ∈ f.support | m p = i}

theorem MvPolynomial.mem_image_support_coeff_finSuccEquivNth {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x : Fin (n + 1) →₀ ℕ} : x ∈ Finsupp.insertNth p i '' ↑(((finSuccEquivNth R p) f).coeff i).support ↔ x ∈ f.support ∧ x p = i

theorem MvPolynomial.mem_support_coeff_finSuccEquivNth {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x : Fin n →₀ ℕ} : x ∈ (((finSuccEquivNth R p) f).coeff i).support ↔ Finsupp.insertNth p i x ∈ f.support

theorem MvPolynomial.support_finSuccEquivNth_nonempty {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) : ((finSuccEquivNth R p) f).support.Nonempty

theorem MvPolynomial.degree_finSuccEquivNth {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) : ((finSuccEquivNth R p) f).degree = ↑(degreeOf p f)

The degree of finSuccEquivNth R p f equals the p-th degree of f.

theorem MvPolynomial.natDegree_finSuccEquivNth {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} (f : MvPolynomial (Fin (n + 1)) R) : ((finSuccEquivNth R p) f).natDegree = degreeOf p f

The natDegree of finSuccEquivNth R p f equals the p-th natDegree of f.

theorem MvPolynomial.degreeOf_coeff_finSuccEquivNth {n : ℕ} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} (f : MvPolynomial (Fin (n + 1)) R) (j : Fin n) (i : ℕ) : degreeOf j (((finSuccEquivNth R p) f).coeff i) ≤ degreeOf (p.succAbove j) f

The degree of j in the ith coefficient of finSuccEquivNth R p f is at most the degree of j.succ in f.

theorem MvPolynomial.finSuccEquivNth_rename_finSuccEquivNth {n : ℕ} {σ : Type u_1} {R : Type u_2} [CommSemiring R] {p : Fin (n + 1)} (e : σ ≃ Fin n) (φ : MvPolynomial (Option σ) R) : (finSuccEquivNth R p) ((rename ⇑(e.optionCongr.trans (finSuccEquiv' p).symm)) φ) = Polynomial.map (rename ⇑e).toRingHom ((optionEquivLeft R σ) φ)

Consider a multivariate polynomial φ whose variables are indexed by Option σ, and suppose that σ ≃ Fin n. Then one may view φ as a polynomial over MvPolynomial (Fin n) R, by

1. renaming the variables via Option σ ≃ Fin (n+1), and then singling out the p-th variable via MvPolynomial.finSuccEquivNth R p;
2. first viewing it as polynomial over MvPolynomial σ R via MvPolynomial.optionEquivLeft, and then renaming the variables.

This theorem shows that both constructions are the same.