feat(data/mv_polynomial/equiv): API for mv_polynomial.fin_succ_equiv (#10812)

This PR provides API for `mv_polynomial.fin_succ_equiv`: coefficients, degree, coefficientes of coefficients, degree_of of coefficients, etc.

To state and prove these lemmas I had to define `cons` and `tail` for maps `fin (n+1) →₀ M` and prove the usual properties for these. I'm not sure if this is necessary or the correct approach to do this.



Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: isadofschi

src/data/finsupp/fin.lean

@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2021 Ivan Sadofschi Costa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ivan Sadofschi Costa
+-/
+import data.fin.tuple
+import data.finsupp.basic
+/-!
+# `cons` and `tail` for maps `fin n →₀ M`
+
+We interpret maps `fin n →₀ M` as `n`-tuples of elements of `M`,
+We define the following operations:
+* `finsupp.tail` : the tail of a map `fin (n + 1) →₀ M`, i.e., its last `n` entries;
+* `finsupp.cons` : adding an element at the beginning of an `n`-tuple, to get an `n + 1`-tuple;
+
+In this context, we prove some usual properties of `tail` and `cons`, analogous to those of
+`data.fin.tuple.basic`.
+-/
+
+noncomputable theory
+
+namespace finsupp
+
+variables {n : ℕ} (i : fin n) {M : Type*} [has_zero M] (y : M)
+  (t : fin (n + 1) →₀ M) (s : fin n →₀ M)
+
+
+/-- `tail` for maps `fin (n + 1) →₀ M`. See `fin.tail` for more details. -/
+def tail (s : fin (n + 1) →₀ M) : fin n →₀ M :=
+finsupp.equiv_fun_on_fintype.inv_fun (fin.tail s.to_fun)
+
+/-- `cons` for maps `fin n →₀ M`. See `fin.cons` for more details. -/
+def cons (y : M) (s : fin n →₀ M) : fin (n + 1) →₀ M :=
+finsupp.equiv_fun_on_fintype.inv_fun (fin.cons y s.to_fun)
+
+lemma tail_apply : tail t i = t i.succ :=
+begin
+  simp only [tail, equiv_fun_on_fintype_symm_apply_to_fun, equiv.inv_fun_as_coe],
+  congr,
+end
+
+@[simp] lemma cons_zero : cons y s 0 = y :=
+by simp [cons, finsupp.equiv_fun_on_fintype]
+
+@[simp] lemma cons_succ : cons y s i.succ = s i :=
+begin
+  simp only [finsupp.cons, fin.cons, finsupp.equiv_fun_on_fintype, fin.cases_succ, finsupp.coe_mk],
+  refl,
+end
+
+@[simp] lemma tail_cons : tail (cons y s) = s :=
+begin
+  simp only [finsupp.cons, fin.cons, finsupp.tail, fin.tail],
+  ext,
+  simp only [equiv_fun_on_fintype_symm_apply_to_fun, equiv.inv_fun_as_coe,
+  finsupp.coe_mk, fin.cases_succ, equiv_fun_on_fintype],
+  refl,
+end
+
+@[simp] lemma cons_tail : cons (t 0) (tail t) = t :=
+begin
+  ext,
+  by_cases c_a : a = 0,
+  { rw [c_a, cons_zero] },
+  { rw [←fin.succ_pred a c_a, cons_succ, ←tail_apply] },
+end
+
+@[simp] lemma cons_zero_zero : cons 0 (0 : fin n →₀ M) = 0 :=
+begin
+  ext,
+  by_cases c : a ≠ 0,
+  { rw [←fin.succ_pred a c, cons_succ],
+    simp },
+  { simp only [not_not] at c,
+    simp [c] },
+end
+
+variables {s} {y}
+
+lemma cons_ne_zero_of_left (h : y ≠ 0) : cons y s ≠ 0 :=
+begin
+  by_contradiction c,
+  have h1 : cons y s 0 = 0 := by simp [c],
+  rw cons_zero at h1,
+  cc,
+end
+
+lemma cons_ne_zero_of_right (h : s ≠ 0) : cons y s ≠ 0 :=
+begin
+  by_contradiction c,
+  have h' : s = 0,
+  { ext,
+    simp [ ← cons_succ a y s, c] },
+  cc,
+end
+
+lemma cons_ne_zero_iff : cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0 :=
+begin
+  apply iff.intro,
+  { intro h,
+    apply or_iff_not_imp_left.2,
+    intro h',
+    simp only [not_not] at h',
+    by_contra c,
+    rw [h', c] at h,
+    simpa using h },
+  { intro h,
+    cases h,
+    { exact cons_ne_zero_of_left h },
+    { exact cons_ne_zero_of_right h } },
+end
+
+end finsupp

src/data/mv_polynomial/equiv.lean

@@ -6,7 +6,12 @@ Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 
 import data.mv_polynomial.rename
 import data.polynomial.algebra_map
+import data.polynomial.lifts
+import data.mv_polynomial.variables
+import data.finsupp.fin
 import logic.equiv.fin
+import algebra.big_operators.fin
+
 
 /-!
 # Equivalences between polynomial rings
@@ -47,7 +52,7 @@ universes u v w x
 variables {R : Type u} {S₁ : Type v} {S₂ : Type w} {S₃ : Type x}
 
 namespace mv_polynomial
-variables {σ : Type*} {a a' a₁ a₂ : R} {e : ℕ} {n m : σ} {s : σ →₀ ℕ}
+variables {σ : Type*} {a a' a₁ a₂ : R} {e : ℕ} {s : σ →₀ ℕ}
 
 section equiv
 
@@ -274,19 +279,30 @@ def option_equiv_right : mv_polynomial (option S₁) R ≃ₐ[R] mv_polynomial S
 alg_equiv.of_alg_hom
   (mv_polynomial.aeval (λ o, o.elim (C polynomial.X) X))
   (mv_polynomial.aeval_tower (polynomial.aeval (X none)) (λ i, X (option.some i)))
-  (by ext : 2; simp [mv_polynomial.algebra_map_eq])
-  (by ext i : 2; cases i; simp)
+  begin
+    ext : 2;
+    simp only [mv_polynomial.algebra_map_eq, option.elim, alg_hom.coe_comp, alg_hom.id_comp,
+      is_scalar_tower.coe_to_alg_hom', comp_app, aeval_tower_C, polynomial.aeval_X, aeval_X,
+      option.elim, aeval_tower_X, alg_hom.coe_id, id.def, eq_self_iff_true, implies_true_iff],
+  end
+  begin
+    ext ⟨i⟩ : 2;
+    simp only [option.elim, alg_hom.coe_comp, comp_app, aeval_X, aeval_tower_C,
+      polynomial.aeval_X, alg_hom.coe_id, id.def, aeval_tower_X],
+  end
+
+variables (n : ℕ)
 
 /--
 The algebra isomorphism between multivariable polynomials in `fin (n + 1)` and
 polynomials over multivariable polynomials in `fin n`.
 -/
-def fin_succ_equiv (n : ℕ) :
+def fin_succ_equiv :
   mv_polynomial (fin (n + 1)) R ≃ₐ[R] polynomial (mv_polynomial (fin n) R) :=
 (rename_equiv R (fin_succ_equiv n)).trans
   (option_equiv_left R (fin n))
 
-lemma fin_succ_equiv_eq (n : ℕ) :
+lemma fin_succ_equiv_eq :
   (fin_succ_equiv R n : mv_polynomial (fin (n + 1)) R →+* polynomial (mv_polynomial (fin n) R)) =
   eval₂_hom (polynomial.C.comp (C : R →+* mv_polynomial (fin n) R))
     (λ i : fin (n+1), fin.cases polynomial.X (λ k, polynomial.C (X k)) i) :=
@@ -301,7 +317,7 @@ begin
     simp [fin_succ_equiv] }
 end
 
-@[simp] lemma fin_succ_equiv_apply (n : ℕ) (p : mv_polynomial (fin (n + 1)) R) :
+@[simp] lemma fin_succ_equiv_apply (p : mv_polynomial (fin (n + 1)) R) :
   fin_succ_equiv R n p =
   eval₂_hom (polynomial.C.comp (C : R →+* mv_polynomial (fin n) R))
     (λ i : fin (n+1), fin.cases polynomial.X (λ k, polynomial.C (X k)) i) p :=
@@ -319,6 +335,153 @@ begin
   simp only [mv_polynomial.fin_succ_equiv_apply, mv_polynomial.eval₂_hom_C],
 end
 
+variables {n} {R}
+
+lemma fin_succ_equiv_X_zero :
+  fin_succ_equiv R n (X 0) = polynomial.X := by simp
+
+lemma fin_succ_equiv_X_succ {j : fin n} :
+  fin_succ_equiv R n (X j.succ) = polynomial.C (X j) := by simp
+
+/-- The coefficient of `m` in the `i`-th coefficient of `fin_succ_equiv R n f` equals the
+    coefficient of `finsupp.cons i m` in `f`. -/
+lemma fin_succ_equiv_coeff_coeff (m : fin n →₀ ℕ)
+  (f : mv_polynomial (fin (n + 1)) R) (i : ℕ) :
+  coeff m (polynomial.coeff (fin_succ_equiv R n f) i) = coeff (m.cons i) f :=
+begin
+  induction f using mv_polynomial.induction_on' with j r p q hp hq generalizing i m,
+  swap,
+  { simp only [(fin_succ_equiv R n).map_add, polynomial.coeff_add, coeff_add, hp, hq] },
+  simp only [fin_succ_equiv_apply, coe_eval₂_hom, eval₂_monomial, ring_hom.coe_comp, prod_pow,
+    polynomial.coeff_C_mul, coeff_C_mul, coeff_monomial,
+    fin.prod_univ_succ, fin.cases_zero, fin.cases_succ, ← ring_hom.map_prod, ← ring_hom.map_pow],
+  rw [← mul_boole, mul_comm (polynomial.X ^ j 0), polynomial.coeff_C_mul_X_pow], congr' 1,
+  obtain rfl | hjmi := eq_or_ne j (m.cons i),
+  { simpa only [cons_zero, cons_succ, if_pos rfl, monomial_eq, C_1, one_mul, prod_pow]
+      using coeff_monomial m m (1:R), },
+  { simp only [hjmi, if_false],
+    obtain hij | rfl := ne_or_eq i (j 0),
+    { simp only [hij, if_false, coeff_zero] },
+    simp only [eq_self_iff_true, if_true],
+    have hmj : m ≠ j.tail, { rintro rfl, rw [cons_tail] at hjmi, contradiction },
+    simpa only [monomial_eq, C_1, one_mul, prod_pow, finsupp.tail_apply, if_neg hmj.symm]
+      using coeff_monomial m j.tail (1:R), }
+end
+
+lemma eval_eq_eval_mv_eval' (s : fin n → R) (y : R) (f : mv_polynomial (fin (n + 1)) R) :
+  eval (fin.cons y s : fin (n + 1) → R) f =
+    polynomial.eval y (polynomial.map (eval s) (fin_succ_equiv R n f)) :=
+begin
+  -- turn this into a def `polynomial.map_alg_hom`
+  let φ : (mv_polynomial (fin n) R)[X] →ₐ[R] R[X] :=
+  { commutes' := λ r, by { convert polynomial.map_C _, exact (eval_C _).symm },
+    .. polynomial.map_ring_hom (eval s) },
+  show aeval (fin.cons y s : fin (n + 1) → R) f =
+    (polynomial.aeval y).comp (φ.comp (fin_succ_equiv R n).to_alg_hom) f,
+  congr' 2,
+  apply mv_polynomial.alg_hom_ext,
+  rw fin.forall_fin_succ,
+  simp only [aeval_X, fin.cons_zero, alg_equiv.to_alg_hom_eq_coe, alg_hom.coe_comp,
+    polynomial.coe_aeval_eq_eval, polynomial.map_C, alg_hom.coe_mk, ring_hom.to_fun_eq_coe,
+    polynomial.coe_map_ring_hom, alg_equiv.coe_alg_hom, comp_app, fin_succ_equiv_apply,
+    eval₂_hom_X', fin.cases_zero, polynomial.map_X, polynomial.eval_X, eq_self_iff_true,
+  fin.cons_succ, fin.cases_succ, eval_X, polynomial.eval_C, implies_true_iff, and_self],
+end
+
+lemma coeff_eval_eq_eval_coeff (s' : fin n → R) (f : polynomial (mv_polynomial (fin n) R))
+  (i : ℕ) : polynomial.coeff (polynomial.map (eval s') f) i = eval s' (polynomial.coeff f i) :=
+by simp only [polynomial.coeff_map]
+
+lemma support_coeff_fin_succ_equiv {f : mv_polynomial (fin (n + 1)) R} {i : ℕ}
+  {m : fin n →₀ ℕ } : m ∈ (polynomial.coeff ((fin_succ_equiv R n) f) i).support
+   ↔ (finsupp.cons i m) ∈ f.support :=
+begin
+  apply iff.intro,
+  { intro h,
+    simpa [←fin_succ_equiv_coeff_coeff] using h },
+  { intro h,
+    simpa [mem_support_iff, ←fin_succ_equiv_coeff_coeff m f i] using h },
+end
+
+lemma fin_succ_equiv_support (f : mv_polynomial (fin (n + 1)) R) :
+  (fin_succ_equiv R n f).support = finset.image (λ m : fin (n + 1)→₀ ℕ, m 0) f.support :=
+begin
+  ext i,
+  rw [polynomial.mem_support_iff, finset.mem_image, nonzero_iff_exists],
+  split,
+  { rintro ⟨m, hm⟩,
+    refine ⟨cons i m, _, cons_zero _ _⟩,
+    rw ← support_coeff_fin_succ_equiv,
+    simpa using hm, },
+  { rintro ⟨m, h, rfl⟩,
+    refine ⟨tail m, _⟩,
+    rwa [← coeff, ← mem_support_iff, support_coeff_fin_succ_equiv, cons_tail] },
+end
+
+lemma fin_succ_equiv_support' {f : mv_polynomial (fin (n + 1)) R} {i : ℕ} :
+  finset.image (finsupp.cons i) (polynomial.coeff ((fin_succ_equiv R n) f) i).support
+   = f.support.filter(λ m, m 0 = i) :=
+begin
+  ext m,
+  rw [finset.mem_filter, finset.mem_image, mem_support_iff],
+  conv_lhs
+  { congr,
+    funext,
+    rw [mem_support_iff, fin_succ_equiv_coeff_coeff, ne.def] },
+  split,
+  { rintros ⟨m',⟨h, hm'⟩⟩,
+    simp only [←hm'],
+    exact ⟨h, by rw cons_zero⟩ },
+  { intro h,
+    use tail m,
+    rw [← h.2, cons_tail],
+    simp [h.1] }
+end
+
+lemma support_fin_succ_equiv_nonempty {f : mv_polynomial (fin (n + 1)) R} (h : f ≠ 0) :
+  (fin_succ_equiv R n f).support.nonempty :=
+begin
+  by_contradiction c,
+  simp only [finset.not_nonempty_iff_eq_empty, polynomial.support_eq_empty] at c,
+  have t'' : (fin_succ_equiv R n f) ≠ 0,
+  { let ii := (fin_succ_equiv R n).symm,
+    have h' : f = 0 :=
+      calc f = ii (fin_succ_equiv R n f) : by simpa only [ii, ←alg_equiv.inv_fun_eq_symm]
+                                             using ((fin_succ_equiv R n).left_inv f).symm
+      ...    = ii 0 : by rw c
+      ...    = 0 : by simp,
+    simpa [h'] using h },
+  simpa [c] using h,
+end
+
+lemma degree_fin_succ_equiv {f : mv_polynomial (fin (n + 1)) R} (h : f ≠ 0) :
+  (fin_succ_equiv R n f).degree = degree_of 0 f :=
+begin
+  have h' : (fin_succ_equiv R n f).support.sup (λ x , x)  = degree_of 0 f,
+  { rw [degree_of_eq_sup, fin_succ_equiv_support f, finset.sup_image] },
+  rw [polynomial.degree, ← h', finset.coe_sup_of_nonempty (support_fin_succ_equiv_nonempty h)],
+  congr,
+end
+
+lemma nat_degree_fin_succ_equiv (f : mv_polynomial (fin (n + 1)) R) :
+  (fin_succ_equiv R n f).nat_degree = degree_of 0 f :=
+begin
+  by_cases c : f = 0,
+  { rw [c, (fin_succ_equiv R n).map_zero, polynomial.nat_degree_zero, degree_of_zero] },
+  { rw [polynomial.nat_degree, degree_fin_succ_equiv (by simpa only [ne.def]) ],
+    simp },
+end
+
+lemma degree_of_coeff_fin_succ_equiv (p : mv_polynomial (fin (n + 1)) R) (j : fin n)
+  (i : ℕ) : degree_of j (polynomial.coeff (fin_succ_equiv R n p) i) ≤ degree_of j.succ p :=
+begin
+  rw [degree_of_eq_sup, degree_of_eq_sup, finset.sup_le_iff],
+  intros m hm,
+  rw ← finsupp.cons_succ j i m,
+  convert finset.le_sup (support_coeff_fin_succ_equiv.1 hm),
+  refl,
+end
+
 end
 
 end equiv