[Merged by Bors] - feat(data/mv_polynomial/funext): function extensionality for polynomials

src/data/equiv/ring.lean

@@ -84,6 +84,10 @@ variables {R}
 @[trans] protected def trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') : R ≃+* S' :=
 { .. (e₁.to_mul_equiv.trans e₂.to_mul_equiv), .. (e₁.to_add_equiv.trans e₂.to_add_equiv) }
 
+@[simp] lemma trans_apply {A B C : Type*}
+  [semiring A] [semiring B] [semiring C] (e : A ≃+* B) (f : B ≃+* C) (a : A) :
+  e.trans f a = f (e a) := rfl
+
 protected lemma bijective (e : R ≃+* S) : function.bijective e := e.to_equiv.bijective
 protected lemma injective (e : R ≃+* S) : function.injective e := e.to_equiv.injective
 protected lemma surjective (e : R ≃+* S) : function.surjective e := e.to_equiv.surjective

src/data/mv_polynomial/basic.lean

@@ -140,14 +140,30 @@ by simp [C, monomial, single_mul_single]
 @[simp] lemma C_pow (a : α) (n : ℕ) : (C (a^n) : mv_polynomial σ α) = (C a)^n :=
 by induction n; simp [pow_succ, *]
 
-lemma C_injective (σ : Type*) (R : Type*) [comm_ring R] :
+lemma C_injective (σ : Type*) (R : Type*) [comm_semiring R] :
   function.injective (C : R → mv_polynomial σ R) :=
 finsupp.single_injective _
 
-@[simp] lemma C_inj {σ : Type*} (R : Type*) [comm_ring R] (r s : R) :
+@[simp] lemma C_inj {σ : Type*} (R : Type*) [comm_semiring R] (r s : R) :
   (C r : mv_polynomial σ R) = C s ↔ r = s :=
 (C_injective σ R).eq_iff
 
+instance infinite_of_infinite_right (σ : Type*) (R : Type*) [comm_semiring R] [infinite R] :
+  infinite (mv_polynomial σ R) :=
+infinite.of_injective C (C_injective _ _)
+
+instance infinite_of_nonempty_left (σ : Type*) (R : Type*) [nonempty σ] [comm_semiring R] [nontrivial R] :
+  infinite (mv_polynomial σ R) :=
+infinite.of_injective (λ i : ℕ, monomial (single (classical.arbitrary σ) i) 1)
+begin
+  intros m n h,
+  have := (single_eq_single_iff _ _ _ _).mp h,
+  simp only [and_true, eq_self_iff_true, or_false, one_ne_zero, and_self] at this,
+  replace := (single_eq_single_iff _ _ _ _).mp this,
+  simp only [eq_self_iff_true, true_and] at this,
+  rcases this with (rfl|⟨rfl, rfl⟩); refl
+end
+
 lemma C_eq_coe_nat (n : ℕ) : (C ↑n : mv_polynomial σ α) = n :=
 by induction n; simp [nat.succ_eq_add_one, *]
 

src/data/mv_polynomial/equiv.lean

@@ -54,6 +54,7 @@ section equiv
 variables (α) [comm_semiring α]
 
 /-- The ring isomorphism between multivariable polynomials in no variables and the ground ring. -/
+@[simps]
 def pempty_ring_equiv : mv_polynomial pempty α ≃+* α :=
 { to_fun    := mv_polynomial.eval₂ (ring_hom.id _) $ pempty.elim,
   inv_fun   := C,
@@ -67,6 +68,7 @@ def pempty_ring_equiv : mv_polynomial pempty α ≃+* α :=
 The ring isomorphism between multivariable polynomials in a single variable and
 polynomials over the ground ring.
 -/
+@[simps]
 def punit_ring_equiv : mv_polynomial punit α ≃+* polynomial α :=
 { to_fun    := eval₂ polynomial.C (λu:punit, polynomial.X),
   inv_fun   := polynomial.eval₂ mv_polynomial.C (X punit.star),
@@ -91,6 +93,7 @@ def punit_ring_equiv : mv_polynomial punit α ≃+* polynomial α :=
   map_add'  := λ _ _, eval₂_add _ _ }
 
 /-- The ring isomorphism between multivariable polynomials induced by an equivalence of the variables.  -/
+@[simps]
 def ring_equiv_of_equiv (e : β ≃ γ) : mv_polynomial β α ≃+* mv_polynomial γ α :=
 { to_fun    := rename e,
   inv_fun   := rename e.symm,
@@ -100,6 +103,7 @@ def ring_equiv_of_equiv (e : β ≃ γ) : mv_polynomial β α ≃+* mv_polynomia
   map_add'  := (rename e).map_add }
 
 /-- The ring isomorphism between multivariable polynomials induced by a ring isomorphism of the ground ring. -/
+@[simps]
 def ring_equiv_congr [comm_semiring γ] (e : α ≃+* γ) : mv_polynomial β α ≃+* mv_polynomial β γ :=
 { to_fun    := map (e : α →+* γ),
   inv_fun   := map (e.symm : γ →+* α),
@@ -130,12 +134,15 @@ eval₂_hom (C.comp C) (λbc, sum.rec_on bc X (C ∘ X))
 instance is_semiring_hom_sum_to_iter : is_semiring_hom (sum_to_iter α β γ) :=
 eval₂.is_semiring_hom _ _
 
+@[simp]
 lemma sum_to_iter_C (a : α) : sum_to_iter α β γ (C a) = C (C a) :=
 eval₂_C _ _ a
 
+@[simp]
 lemma sum_to_iter_Xl (b : β) : sum_to_iter α β γ (X (sum.inl b)) = X b :=
 eval₂_X _ _ (sum.inl b)
 
+@[simp]
 lemma sum_to_iter_Xr (c : γ) : sum_to_iter α β γ (X (sum.inr c)) = C (X c) :=
 eval₂_X _ _ (sum.inr c)
 
@@ -159,6 +166,7 @@ lemma iter_to_sum_C_X (c : γ) : iter_to_sum α β γ (C (X c)) = X (sum.inr c)
 eq.trans (eval₂_C _ _ (X c)) (eval₂_X _ _ _)
 
 /-- A helper function for `sum_ring_equiv`. -/
+@[simps]
 def mv_polynomial_equiv_mv_polynomial [comm_semiring δ]
   (f : mv_polynomial β α →+* mv_polynomial γ δ)
   (g : mv_polynomial γ δ →+* mv_polynomial β α)
@@ -198,7 +206,7 @@ The ring isomorphism between multivariable polynomials in `option β` and
 polynomials with coefficients in `mv_polynomial β α`.
 -/
 def option_equiv_left : mv_polynomial (option β) α ≃+* polynomial (mv_polynomial β α) :=
-(ring_equiv_of_equiv α $ (equiv.option_equiv_sum_punit β).trans (equiv.sum_comm _ _)).trans $
+(ring_equiv_of_equiv α $ (equiv.option_equiv_sum_punit.{0} β).trans (equiv.sum_comm _ _)).trans $
 (sum_ring_equiv α _ _).trans $
 punit_ring_equiv _
 
@@ -220,6 +228,28 @@ def fin_succ_equiv (n : ℕ) :
 (ring_equiv_of_equiv α (fin_succ_equiv n)).trans
   (option_equiv_left α (fin n))
 
+@[simp] lemma fin_succ_equiv_apply (n : ℕ) (p : mv_polynomial (fin (n + 1)) α) :
+  fin_succ_equiv α n p =
+  eval₂_hom (polynomial.C.comp (C : α →+* mv_polynomial (fin n) α))
+    (λ i : fin (n+1), fin.cases polynomial.X (λ k, polynomial.C (X k)) i) p :=
+begin
+  apply induction_on p,
+  { intro r,
+    dsimp [fin_succ_equiv, option_equiv_left, sum_ring_equiv],
+    simp only [sum_to_iter_C, eval₂_C, rename_C, ring_hom.coe_comp], },
+  { intros, simp only [*, ring_equiv.map_add, ring_hom.map_add] },
+  { intros q i h,
+    dsimp at h,
+    rw [ring_equiv.map_mul, h],
+    dsimp [fin_succ_equiv, option_equiv_left, sum_ring_equiv, _root_.fin_succ_equiv],
+    simp only [rename_X, equiv.sum_comm_apply, function.comp_app, eval₂_mul, eval₂_X],
+    by_cases hi : i = 0,
+    { subst hi,
+      simp only [fin.cases_zero, sum.swap, equiv.option_equiv_sum_punit_none, sum_to_iter_Xl, eval₂_X] },
+    { rw [← fin.succ_pred i hi],
+      simp only [equiv.option_equiv_sum_punit_some, sum.swap, fin.cases_succ, sum_to_iter_Xr, eval₂_C] } }
+end
+
 end
 
 end equiv

src/data/mv_polynomial/funext.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2020 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+import data.polynomial.ring_division
+import data.mv_polynomial.rename
+import ring_theory.polynomial.basic
+
+/-!
+## Function extensionality for multivariate polynomials
+
+In this file we show that two multivariate polynomials over an infinite integral domain are equal
+if they are equal upon evaluating them on an arbitrary assignment of the variables.
+
+# Main declaration
+
+* `mv_polynomial.funext`: two polynomials `φ ψ : mv_polynomial σ R`
+  over an infinite integral domain `R` are equal if `eval x φ = eval x ψ` for all `x : σ → R`.
+
+-/
+
+namespace mv_polynomial
+
+variables {R : Type*} [integral_domain R] [infinite R]
+
+private lemma funext_fin {n : ℕ} {p : mv_polynomial (fin n) R}
+  (h : ∀ x : fin n → R, eval x p = 0) : p = 0 :=
+begin
+  unfreezingI { revert R },
+  induction n with n ih,
+  { introsI R _ _ p h,
+    let e := (ring_equiv_of_equiv R fin_zero_equiv').trans (mv_polynomial.pempty_ring_equiv R),
+    apply e.injective,
+    rw ring_equiv.map_zero,
+    convert h fin_zero_elim,
+    show (eval₂_hom (ring_hom.id _) pempty.elim) (rename fin_zero_equiv' p) = _,
+    rw [eval₂_hom_rename],
+    exact eval₂_hom_congr rfl (subsingleton.elim _ _) rfl },
+  { introsI R _ _ p h,
+    let e := fin_succ_equiv R n,
+    apply e.injective,
+    simp only [ring_equiv.map_zero],
+    apply polynomial.funext,
+    intro q,
+    rw [polynomial.eval_zero],
+    apply ih, swap, { apply_instance },
+    intro x,
+    dsimp [e],
+    rw [fin_succ_equiv_apply],
+    calc _ = eval _ p : _
+       ... = 0 : h _,
+    { intro i, exact fin.cases (eval x q) x i },
+    apply induction_on p,
+    { intro r,
+      simp only [eval_C, polynomial.eval_C, ring_hom.coe_comp, eval₂_hom_C], },
+    { intros, simp only [*, ring_hom.map_add, polynomial.eval_add] },
+    { intros φ i hφ, simp only [*, eval_X, polynomial.eval_mul, ring_hom.map_mul, eval₂_hom_X'],
+      congr' 1,
+      by_cases hi : i = 0,
+      { subst hi, simp only [polynomial.eval_X, fin.cases_zero] },
+      { rw [← fin.succ_pred i hi], simp only [eval_X, polynomial.eval_C, fin.cases_succ] } } }
+end
+
+/-- Two multivariate polynomials over an infinite integral domain are equal
+if they are equal upon evaluating them on an arbitrary assignment of the variables. -/
+lemma funext {σ : Type*} {p q : mv_polynomial σ R}
+  (h : ∀ x : σ → R, eval x p = eval x q) : p = q :=
+begin
+  suffices : ∀ p, (∀ (x : σ → R), eval x p = 0) → p = 0,
+  { rw [← sub_eq_zero, this (p - q)], simp only [h, ring_hom.map_sub, forall_const, sub_self] },
+  clear h p q,
+  intros p h,
+  obtain ⟨s, p, rfl⟩ := exists_finset_rename p,
+  suffices : p = 0, { rw [this, alg_hom.map_zero] },
+  classical,
+  obtain ⟨e⟩ := (fintype.equiv_fin {x // x ∈ s}),
+  apply rename_injective e e.injective,
+  rw [alg_hom.map_zero],
+  apply funext_fin,
+  intro x,
+  show eval₂_hom _ x (rename e p) = 0,
+  rw [eval₂_hom_rename],
+  let y : σ → R := λ i, if h : i ∈ s then x (e ⟨i, h⟩) else 0,
+  convert h y,
+  show _ = eval₂_hom _ _ (rename _ p),
+  rw [eval₂_hom_rename],
+  apply eval₂_hom_congr rfl _ rfl,
+  ext ⟨i, hi⟩,
+  exact (dif_pos hi).symm,
+end
+
+lemma funext_iff {σ : Type*} {p q : mv_polynomial σ R} :
+  p = q ↔ (∀ x : σ → R, eval x p = eval x q) :=
+⟨by rintro rfl; simp only [forall_const, eq_self_iff_true], funext⟩
+
+end mv_polynomial

src/data/polynomial/monomial.lean

@@ -71,4 +71,12 @@ lemma single_eq_C_mul_X : ∀{n}, monomial n a = C a * X^n
 lemma C_inj : C a = C b ↔ a = b :=
 ⟨λ h, coeff_C_zero.symm.trans (h.symm ▸ coeff_C_zero), congr_arg C⟩
 
+instance [nontrivial R] : infinite (polynomial R) :=
+infinite.of_injective (λ i, monomial i 1)
+begin
+  intros m n h,
+  have := (single_eq_single_iff _ _ _ _).mp h,
+  simpa only [and_true, eq_self_iff_true, or_false, one_ne_zero, and_self],
+end
+
 end polynomial

src/data/polynomial/ring_division.lean

@@ -406,6 +406,18 @@ by rw [←polynomial.C_mul', ←polynomial.eq_C_of_degree_eq_zero (degree_coe_un
   nat_degree (u : polynomial R) = 0 :=
 nat_degree_eq_of_degree_eq_some (degree_coe_units u)
 
+lemma zero_of_eval_zero [infinite R] (p : polynomial R) (h : ∀ x, p.eval x = 0) : p = 0 :=
+by classical; by_contradiction hp; exact
+infinite.not_fintype ⟨p.roots.to_finset, λ x, multiset.mem_to_finset.mpr ((mem_roots hp).mpr (h _))⟩
+
+lemma funext [infinite R] {p q : polynomial R} (ext : ∀ r : R, p.eval r = q.eval r) : p = q :=
+begin
+  rw ← sub_eq_zero,
+  apply zero_of_eval_zero,
+  intro x,
+  rw [eval_sub, sub_eq_zero, ext],
+end
+
 end roots
 
 theorem is_unit_iff {f : polynomial R} : is_unit f ↔ ∃ r : R, is_unit r ∧ C r = f :=