feat(data/mv_polynomial/rename): coeff_rename (#4203)

Also, use the opportunity to use R as variable for the coefficient ring
throughout the file.

Author: jcommelin

src/data/mv_polynomial/rename.lean

@@ -20,14 +20,14 @@ which modifies the set of variables.
 
 As in other polynomial files we typically use the notation:
 
-+ `σ : Type*` (indexing the variables)
++ `σ τ α : Type*` (indexing the variables)
 
-+ `α : Type*` `[comm_semiring α]` (the coefficients)
++ `R S : Type*` `[comm_semiring R]` `[comm_semiring S]` (the coefficients)
 
 + `s : σ →₀ ℕ`, a function from `σ` to `ℕ` which is zero away from a finite set.
 This will give rise to a monomial in `mv_polynomial σ R` which mathematicians might call `X^s`
 
-+ `a : α`
++ `r : R` elements of the coefficient ring
 
 + `i : σ`, with corresponding monomial `X i`, often denoted `X_i` by mathematicians
 
@@ -42,35 +42,33 @@ open_locale classical big_operators
 open set function finsupp add_monoid_algebra
 open_locale big_operators
 
-universes u v w x
-variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
+variables {σ τ α R S : Type*} [comm_semiring R] [comm_semiring S]
 
 namespace mv_polynomial
-variables {σ : Type*} {a a' a₁ a₂ : α} {e : ℕ} {n m : σ} {s : σ →₀ ℕ}
+
+-- variables {a : R} {e : ℕ} {n m : σ} {s : σ →₀ ℕ}
 
 
 section rename
-variables {α} [comm_semiring α]
 
 /-- Rename all the variables in a multivariable polynomial. -/
-def rename (f : β → γ) : mv_polynomial β α →ₐ[α] mv_polynomial γ α :=
+def rename (f : σ → τ) : mv_polynomial σ R →ₐ[R] mv_polynomial τ R :=
 aeval (X ∘ f)
 
-@[simp] lemma rename_C (f : β → γ) (a : α) : rename f (C a) = C a :=
+@[simp] lemma rename_C (f : σ → τ) (r : R) : rename f (C r) = C r :=
 eval₂_C _ _ _
 
-@[simp] lemma rename_X (f : β → γ) (b : β) : rename f (X b : mv_polynomial β α) = X (f b) :=
+@[simp] lemma rename_X (f : σ → τ) (i : σ) : rename f (X i : mv_polynomial σ R) = X (f i) :=
 eval₂_X _ _ _
 
-lemma map_rename [comm_semiring β] (f : α →+* β)
-  (g : γ → δ) (p : mv_polynomial γ α) :
+lemma map_rename (f : R →+* S) (g : σ → τ) (p : mv_polynomial σ R) :
   map f (rename g p) = rename g (map f p) :=
 mv_polynomial.induction_on p
-  (λ a, by simp)
-  (λ p q hp hq, by simp [hp, hq])
-  (λ p n hp, by simp [hp])
+  (λ a, by simp only [map_C, rename_C])
+  (λ p q hp hq, by simp only [hp, hq, alg_hom.map_add, ring_hom.map_add])
+  (λ p n hp, by simp only [hp, rename_X, map_X, ring_hom.map_mul, alg_hom.map_mul])
 
-@[simp] lemma rename_rename (f : β → γ) (g : γ → δ) (p : mv_polynomial β α) :
+@[simp] lemma rename_rename (f : σ → τ) (g : τ → α) (p : mv_polynomial σ R) :
   rename g (rename f p) = rename (g ∘ f) p :=
 show rename g (eval₂ C (X ∘ f) p) = _,
 begin
@@ -80,19 +78,19 @@ begin
   ext1, simp only [comp_app, ring_hom.coe_comp, eval₂_hom_C],
 end
 
-@[simp] lemma rename_id (p : mv_polynomial β α) : rename id p = p :=
+@[simp] lemma rename_id (p : mv_polynomial σ R) : rename id p = p :=
 eval₂_eta p
 
-lemma rename_monomial (f : β → γ) (p : β →₀ ℕ) (a : α) :
-  rename f (monomial p a) = monomial (p.map_domain f) a :=
+lemma rename_monomial (f : σ → τ) (d : σ →₀ ℕ) (r : R) :
+  rename f (monomial d r) = monomial (d.map_domain f) r :=
 begin
   rw [rename, aeval_monomial, monomial_eq, finsupp.prod_map_domain_index],
   { refl },
   { exact assume n, pow_zero _ },
   { exact assume n i₁ i₂, pow_add _ _ _ }
 end
 
-lemma rename_eq (f : β → γ) (p : mv_polynomial β α) :
+lemma rename_eq (f : σ → τ) (p : mv_polynomial σ R) :
   rename f p = finsupp.map_domain (finsupp.map_domain f) p :=
 begin
   simp only [rename, aeval_def, eval₂, finsupp.map_domain, ring_hom.coe_of],
@@ -105,16 +103,16 @@ begin
   exact assume a b c, pow_add _ _ _
 end
 
-lemma rename_injective (f : β → γ) (hf : function.injective f) :
-  function.injective (rename f : mv_polynomial β α → mv_polynomial γ α) :=
-have (rename f : mv_polynomial β α → mv_polynomial γ α) =
+lemma rename_injective (f : σ → τ) (hf : function.injective f) :
+  function.injective (rename f : mv_polynomial σ R → mv_polynomial τ R) :=
+have (rename f : mv_polynomial σ R → mv_polynomial τ R) =
   finsupp.map_domain (finsupp.map_domain f) := funext (rename_eq f),
 begin
   rw this,
   exact finsupp.map_domain_injective (finsupp.map_domain_injective hf)
 end
 
-lemma total_degree_rename_le (f : β → γ) (p : mv_polynomial β α) :
+lemma total_degree_rename_le (f : σ → τ) (p : mv_polynomial σ R) :
   (rename f p).total_degree ≤ p.total_degree :=
 finset.sup_le $ assume b,
   begin
@@ -130,36 +128,35 @@ finset.sup_le $ assume b,
   end
 
 section
-variables [comm_semiring β] (f : α →+* β)
-variables (k : γ → δ) (g : δ → β) (p : mv_polynomial γ α)
+variables (f : R →+* S) (k : σ → τ) (g : τ → S) (p : mv_polynomial σ R)
 
 lemma eval₂_rename : (rename k p).eval₂ f g = p.eval₂ f (g ∘ k) :=
 by apply mv_polynomial.induction_on p; { intros, simp [*] }
 
 lemma eval₂_hom_rename : eval₂_hom f g (rename k p) = eval₂_hom f (g ∘ k) p :=
 eval₂_rename _ _ _ _
 
-lemma rename_eval₂ (g : δ → mv_polynomial γ α) :
+lemma rename_eval₂ (g : τ → mv_polynomial σ R) :
   rename k (p.eval₂ C (g ∘ k)) = (rename k p).eval₂ C (rename k ∘ g) :=
 by apply mv_polynomial.induction_on p; { intros, simp [*] }
 
-lemma rename_prodmk_eval₂ (d : δ) (g : γ → mv_polynomial γ α) :
-  rename (prod.mk d) (p.eval₂ C g) = p.eval₂ C (λ x, rename (prod.mk d) (g x)) :=
+lemma rename_prodmk_eval₂ (j : τ) (g : σ → mv_polynomial σ R) :
+  rename (prod.mk j) (p.eval₂ C g) = p.eval₂ C (λ x, rename (prod.mk j) (g x)) :=
 by apply mv_polynomial.induction_on p; { intros, simp [*] }
 
-lemma eval₂_rename_prodmk (g : δ × γ → β) (d : δ) :
-  (rename (prod.mk d) p).eval₂ f g = eval₂ f (λ i, g (d, i)) p :=
+lemma eval₂_rename_prodmk (g : σ × τ → S) (i : σ) (p : mv_polynomial τ R) :
+  (rename (prod.mk i) p).eval₂ f g = eval₂ f (λ j, g (i, j)) p :=
 by apply mv_polynomial.induction_on p; { intros, simp [*] }
 
-lemma eval_rename_prodmk (g : δ × γ → α) (d : δ) :
-  eval g (rename (prod.mk d) p) = eval (λ i, g (d, i)) p :=
+lemma eval_rename_prodmk (g : σ × τ → R) (i : σ) (p : mv_polynomial τ R) :
+  eval g (rename (prod.mk i) p) = eval (λ j, g (i, j)) p :=
 eval₂_rename_prodmk (ring_hom.id _) _ _ _
 
 end
 
 /-- Every polynomial is a polynomial in finitely many variables. -/
-theorem exists_finset_rename (p : mv_polynomial γ α) :
-  ∃ (s : finset γ) (q : mv_polynomial {x // x ∈ s} α), p = rename coe q :=
+theorem exists_finset_rename (p : mv_polynomial σ R) :
+  ∃ (s : finset σ) (q : mv_polynomial {x // x ∈ s} R), p = rename coe q :=
 begin
   apply induction_on p,
   { intro r, exact ⟨∅, C r, by rw rename_C⟩ },
@@ -176,8 +173,8 @@ begin
 end
 
 /-- Every polynomial is a polynomial in finitely many variables. -/
-theorem exists_fin_rename (p : mv_polynomial γ α) :
-  ∃ (n : ℕ) (f : fin n → γ) (hf : injective f) (q : mv_polynomial (fin n) α), p = rename f q :=
+theorem exists_fin_rename (p : mv_polynomial σ R) :
+  ∃ (n : ℕ) (f : fin n → σ) (hf : injective f) (q : mv_polynomial (fin n) R), p = rename f q :=
 begin
   obtain ⟨s, q, rfl⟩ := exists_finset_rename p,
   obtain ⟨n, ⟨e⟩⟩ := fintype.exists_equiv_fin {x // x ∈ s},
@@ -188,12 +185,46 @@ end
 
 end rename
 
-lemma eval₂_cast_comp {β : Type u} {γ : Type v} (f : γ → β)
-  {α : Type w} [comm_ring α] (c : ℤ →+* α) (g : β → α) (x : mv_polynomial γ ℤ) :
-  eval₂ c (g ∘ f) x = eval₂ c g (rename f x) :=
-mv_polynomial.induction_on x
+lemma eval₂_cast_comp (f : σ → τ) (c : ℤ →+* R) (g : τ → R) (p : mv_polynomial σ ℤ) :
+  eval₂ c (g ∘ f) p = eval₂ c g (rename f p) :=
+mv_polynomial.induction_on p
 (λ n, by simp only [eval₂_C, rename_C])
 (λ p q hp hq, by simp only [hp, hq, rename, eval₂_add, alg_hom.map_add])
 (λ p n hp, by simp only [hp, rename, aeval_def, eval₂_X, eval₂_mul])
 
+section coeff
+
+@[simp]
+lemma coeff_rename_map_domain (f : σ → τ) (hf : injective f) (φ : mv_polynomial σ R) (d : σ →₀ ℕ) :
+  (rename f φ).coeff (d.map_domain f) = φ.coeff d :=
+begin
+  apply induction_on' φ,
+  { intros u r,
+    rw [rename_monomial, coeff_monomial, coeff_monomial],
+    simp only [(finsupp.map_domain_injective hf).eq_iff],
+    split_ifs; refl, },
+  { intros, simp only [*, alg_hom.map_add, coeff_add], }
+end
+
+lemma coeff_rename_eq_zero (f : σ → τ) (φ : mv_polynomial σ R) (d : τ →₀ ℕ)
+  (h : ∀ u : σ →₀ ℕ, u.map_domain f = d → φ.coeff u = 0) :
+  (rename f φ).coeff d = 0 :=
+begin
+  rw [rename_eq, coeff, ← not_mem_support_iff],
+  intro H,
+  replace H := map_domain_support H,
+  rw [finset.mem_image] at H,
+  obtain ⟨u, hu, rfl⟩ := H,
+  specialize h u rfl,
+  simp [mem_support_iff, coeff] at h hu,
+  contradiction
+end
+
+lemma coeff_rename_ne_zero (f : σ → τ) (φ : mv_polynomial σ R) (d : τ →₀ ℕ)
+  (h : (rename f φ).coeff d ≠ 0) :
+  ∃ u : σ →₀ ℕ, u.map_domain f = d ∧ φ.coeff u ≠ 0 :=
+by { contrapose! h, apply coeff_rename_eq_zero _ _ _ h }
+
+end coeff
+
 end mv_polynomial