refactor(data/equiv/algebra): move polynomial lemmas from equiv/alge…

…bra to mv_polynomial (#731)

* refactor(data/equiv/algebra): move polynomial lemma from equiv/algebra to mv_polynomial

* remove update-mathlib.py

src/category_theory/instances/rings.lean

@@ -108,7 +108,7 @@ noncomputable def polynomial : Type u ⥤ CommRing.{u} :=
   (polynomial.obj α).α = mv_polynomial α ℤ := rfl
 
 @[simp] lemma polynomial_map_val {α β : Type u} {f : α → β} :
-  (polynomial.map f).val = eval₂ C (X ∘ f) := rfl
+  (CommRing.polynomial.map f).val = eval₂ C (X ∘ f) := rfl
 
 noncomputable def adj : adjunction polynomial (forget : CommRing ⥤ Type u) :=
 adjunction.mk_of_hom_equiv _ _

src/data/equiv/algebra.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import data.equiv.basic data.polynomial linear_algebra.multivariate_polynomial
+import data.equiv.basic algebra.field
 
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
@@ -215,159 +215,3 @@ protected def trans {α β γ : Type*} [ring α] [ring β] [ring γ]
 { hom := is_ring_hom.comp _ _, .. e₁.1.trans e₂.1  }
 
 end ring_equiv
-
-namespace mv_polynomial
-
-variables (α) [comm_ring α]
-variables [decidable_eq α] [decidable_eq β] [decidable_eq γ] [decidable_eq δ]
-
-def pempty_ring_equiv : mv_polynomial pempty α ≃r α :=
-{ to_fun    := mv_polynomial.eval₂ id $ pempty.elim,
-  inv_fun   := C,
-  left_inv  := is_id _ (by apply_instance) (assume a, by rw [eval₂_C]; refl) (assume a, a.elim),
-  right_inv := λ r, eval₂_C _ _ _,
-  hom       := eval₂.is_ring_hom _ _ }
-
-def punit_ring_equiv : mv_polynomial punit α ≃r polynomial α :=
-{ to_fun    := eval₂ polynomial.C (λu:punit, polynomial.X),
-  inv_fun   := polynomial.eval₂ mv_polynomial.C (X punit.star),
-  left_inv  :=
-    begin
-      refine is_id _ _ _ _,
-      apply is_semiring_hom.comp (eval₂ polynomial.C (λu:punit, polynomial.X)) _; apply_instance,
-      { assume a, rw [eval₂_C, polynomial.eval₂_C] },
-      { rintros ⟨⟩, rw [eval₂_X, polynomial.eval₂_X] }
-    end,
-  right_inv := assume p, polynomial.induction_on p
-    (assume a, by rw [polynomial.eval₂_C, mv_polynomial.eval₂_C])
-    (assume p q hp hq, by rw [polynomial.eval₂_add, mv_polynomial.eval₂_add, hp, hq])
-    (assume p n hp,
-      by rw [polynomial.eval₂_mul, polynomial.eval₂_pow, polynomial.eval₂_X, polynomial.eval₂_C,
-        eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]),
-  hom       := eval₂.is_ring_hom _ _ }
-
-def ring_equiv_of_equiv (e : β ≃ γ) : mv_polynomial β α ≃r mv_polynomial γ α :=
-{ to_fun    := rename e,
-  inv_fun   := rename e.symm,
-  left_inv  := λ p, by simp only [rename_rename, (∘), e.inverse_apply_apply]; exact rename_id p,
-  right_inv := λ p, by simp only [rename_rename, (∘), e.apply_inverse_apply]; exact rename_id p,
-  hom       := rename.is_ring_hom e }
-
-def ring_equiv_congr [comm_ring γ] (e : α ≃r γ) : mv_polynomial β α ≃r mv_polynomial β γ :=
-{ to_fun    := map e.to_fun,
-  inv_fun   := map e.symm.to_fun,
-  left_inv  := assume p,
-    have (e.symm.to_equiv.to_fun ∘ e.to_equiv.to_fun) = id,
-    { ext a, exact e.to_equiv.inverse_apply_apply a },
-    by simp only [map_map, this, map_id],
-  right_inv := assume p,
-    have (e.to_equiv.to_fun ∘ e.symm.to_equiv.to_fun) = id,
-    { ext a, exact e.to_equiv.apply_inverse_apply a },
-    by simp only [map_map, this, map_id],
-  hom       := map.is_ring_hom e.to_fun }
-
-section
-variables (β γ δ)
-
-instance ring_on_sum : ring (mv_polynomial (β ⊕ γ) α) := by apply_instance
-instance ring_on_iter : ring (mv_polynomial β (mv_polynomial γ α)) := by apply_instance
-
-def sum_to_iter : mv_polynomial (β ⊕ γ) α → mv_polynomial β (mv_polynomial γ α) :=
-eval₂ (C ∘ C) (λbc, sum.rec_on bc X (C ∘ X))
-
-instance is_semiring_hom_C_C :
-  is_semiring_hom (C ∘ C : α → mv_polynomial β (mv_polynomial γ α)) :=
-@is_semiring_hom.comp _ _ _ _ C mv_polynomial.is_semiring_hom _ _ C mv_polynomial.is_semiring_hom
-
-instance is_semiring_hom_sum_to_iter : is_semiring_hom (sum_to_iter α β γ) :=
-eval₂.is_semiring_hom _ _
-
-lemma sum_to_iter_C (a : α) : sum_to_iter α β γ (C a) = C (C a) :=
-eval₂_C _ _ a
-
-lemma sum_to_iter_Xl (b : β) : sum_to_iter α β γ (X (sum.inl b)) = X b :=
-eval₂_X _ _ (sum.inl b)
-
-lemma sum_to_iter_Xr (c : γ) : sum_to_iter α β γ (X (sum.inr c)) = C (X c) :=
-eval₂_X _ _ (sum.inr c)
-
-def iter_to_sum : mv_polynomial β (mv_polynomial γ α) → mv_polynomial (β ⊕ γ) α :=
-eval₂ (eval₂ C (X ∘ sum.inr)) (X ∘ sum.inl)
-
-section
-
-instance is_semiring_hom_iter_to_sum : is_semiring_hom (iter_to_sum α β γ) :=
-eval₂.is_semiring_hom _ _
-
-end
-
-lemma iter_to_sum_C_C (a : α) : iter_to_sum α β γ (C (C a)) = C a :=
-eq.trans (eval₂_C _ _ (C a)) (eval₂_C _ _ _)
-
-lemma iter_to_sum_X (b : β) : iter_to_sum α β γ (X b) = X (sum.inl b) :=
-eval₂_X _ _ _
-
-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 _ _ _)
-
-def mv_polynomial_equiv_mv_polynomial [comm_ring δ]
-  (f : mv_polynomial β α → mv_polynomial γ δ) (hf : is_semiring_hom f)
-  (g : mv_polynomial γ δ → mv_polynomial β α) (hg : is_semiring_hom g)
-  (hfgC : ∀a, f (g (C a)) = C a)
-  (hfgX : ∀n, f (g (X n)) = X n)
-  (hgfC : ∀a, g (f (C a)) = C a)
-  (hgfX : ∀n, g (f (X n)) = X n) :
-  mv_polynomial β α ≃r mv_polynomial γ δ :=
-{ to_fun    := f, inv_fun := g,
-  left_inv  := is_id _ (is_semiring_hom.comp _ _) hgfC hgfX,
-  right_inv := is_id _ (is_semiring_hom.comp _ _) hfgC hfgX,
-  hom       := is_ring_hom.of_semiring f }
-
-def sum_ring_equiv : mv_polynomial (β ⊕ γ) α ≃r mv_polynomial β (mv_polynomial γ α) :=
-begin
-  apply @mv_polynomial_equiv_mv_polynomial α (β ⊕ γ) _ _ _ _ _ _ _ _
-    (sum_to_iter α β γ) _ (iter_to_sum α β γ) _,
-  { assume p,
-    apply @hom_eq_hom _ _ _ _ _ _ _ _ _ _ _ _ _ p,
-    apply_instance,
-    { apply @is_semiring_hom.comp _ _ _ _ _ _ _ _ _ _,
-      apply_instance,
-      apply @is_semiring_hom.comp _ _ _ _ _ _ _ _ _ _,
-      apply_instance,
-      { apply @mv_polynomial.is_semiring_hom },
-      { apply mv_polynomial.is_semiring_hom_iter_to_sum α β γ },
-      { apply mv_polynomial.is_semiring_hom_sum_to_iter α β γ } },
-    { apply mv_polynomial.is_semiring_hom },
-    { assume a, rw [iter_to_sum_C_C α β γ, sum_to_iter_C α β γ] },
-    { assume c, rw [iter_to_sum_C_X α β γ, sum_to_iter_Xr α β γ] } },
-  { assume b, rw [iter_to_sum_X α β γ, sum_to_iter_Xl α β γ] },
-  { assume a, rw [sum_to_iter_C α β γ, iter_to_sum_C_C α β γ] },
-  { assume n, cases n with b c,
-    { rw [sum_to_iter_Xl, iter_to_sum_X] },
-    { rw [sum_to_iter_Xr, iter_to_sum_C_X] } },
-  { apply mv_polynomial.is_semiring_hom_sum_to_iter α β γ },
-  { apply mv_polynomial.is_semiring_hom_iter_to_sum α β γ }
-end
-
-instance option_ring : ring (mv_polynomial (option β) α) :=
-mv_polynomial.ring
-
-instance polynomial_ring : ring (polynomial (mv_polynomial β α)) :=
-@comm_ring.to_ring _ polynomial.comm_ring
-
-instance polynomial_ring2 : ring (mv_polynomial β (polynomial α)) :=
-by apply_instance
-
-def option_equiv_left : mv_polynomial (option β) α ≃r polynomial (mv_polynomial β α) :=
-(ring_equiv_of_equiv α $ (equiv.option_equiv_sum_punit β).trans (equiv.sum_comm _ _)).trans $
-(sum_ring_equiv α _ _).trans $
-punit_ring_equiv _
-
-def option_equiv_right : mv_polynomial (option β) α ≃r mv_polynomial β (polynomial α) :=
-(ring_equiv_of_equiv α $ equiv.option_equiv_sum_punit.{0} β).trans $
-(sum_ring_equiv α β unit).trans $
-ring_equiv_congr (mv_polynomial unit α) (punit_ring_equiv α)
-
-end
-
-end mv_polynomial

src/linear_algebra/multivariate_polynomial.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 
 Multivariate Polynomial
 -/
-import data.finsupp linear_algebra.basic algebra.ring
+import data.finsupp linear_algebra.basic algebra.ring data.polynomial data.equiv.algebra
 
 open set function finsupp lattice
 
@@ -412,4 +412,160 @@ instance rename.is_ring_hom
 @is_ring_hom.of_semiring (mv_polynomial β α) (mv_polynomial γ α) _ _ (rename f)
   (rename.is_semiring_hom f)
 
+section equiv
+
+variables (α) [comm_ring α]
+variables [decidable_eq β] [decidable_eq γ] [decidable_eq δ]
+
+def pempty_ring_equiv : mv_polynomial pempty α ≃r α :=
+{ to_fun    := mv_polynomial.eval₂ id $ pempty.elim,
+  inv_fun   := C,
+  left_inv  := is_id _ (by apply_instance) (assume a, by rw [eval₂_C]; refl) (assume a, a.elim),
+  right_inv := λ r, eval₂_C _ _ _,
+  hom       := eval₂.is_ring_hom _ _ }
+
+def punit_ring_equiv : mv_polynomial punit α ≃r polynomial α :=
+{ to_fun    := eval₂ polynomial.C (λu:punit, polynomial.X),
+  inv_fun   := polynomial.eval₂ mv_polynomial.C (X punit.star),
+  left_inv  :=
+    begin
+      refine is_id _ _ _ _,
+      apply is_semiring_hom.comp (eval₂ polynomial.C (λu:punit, polynomial.X)) _; apply_instance,
+      { assume a, rw [eval₂_C, polynomial.eval₂_C] },
+      { rintros ⟨⟩, rw [eval₂_X, polynomial.eval₂_X] }
+    end,
+  right_inv := assume p, polynomial.induction_on p
+    (assume a, by rw [polynomial.eval₂_C, mv_polynomial.eval₂_C])
+    (assume p q hp hq, by rw [polynomial.eval₂_add, mv_polynomial.eval₂_add, hp, hq])
+    (assume p n hp,
+      by rw [polynomial.eval₂_mul, polynomial.eval₂_pow, polynomial.eval₂_X, polynomial.eval₂_C,
+        eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]),
+  hom       := eval₂.is_ring_hom _ _ }
+
+def ring_equiv_of_equiv (e : β ≃ γ) : mv_polynomial β α ≃r mv_polynomial γ α :=
+{ to_fun    := rename e,
+  inv_fun   := rename e.symm,
+  left_inv  := λ p, by simp only [rename_rename, (∘), e.inverse_apply_apply]; exact rename_id p,
+  right_inv := λ p, by simp only [rename_rename, (∘), e.apply_inverse_apply]; exact rename_id p,
+  hom       := rename.is_ring_hom e }
+
+def ring_equiv_congr [comm_ring γ] (e : α ≃r γ) : mv_polynomial β α ≃r mv_polynomial β γ :=
+{ to_fun    := map e.to_fun,
+  inv_fun   := map e.symm.to_fun,
+  left_inv  := assume p,
+    have (e.symm.to_equiv.to_fun ∘ e.to_equiv.to_fun) = id,
+    { ext a, exact e.to_equiv.inverse_apply_apply a },
+    by simp only [map_map, this, map_id],
+  right_inv := assume p,
+    have (e.to_equiv.to_fun ∘ e.symm.to_equiv.to_fun) = id,
+    { ext a, exact e.to_equiv.apply_inverse_apply a },
+    by simp only [map_map, this, map_id],
+  hom       := map.is_ring_hom e.to_fun }
+
+section
+variables (β γ δ)
+
+instance ring_on_sum : ring (mv_polynomial (β ⊕ γ) α) := by apply_instance
+instance ring_on_iter : ring (mv_polynomial β (mv_polynomial γ α)) := by apply_instance
+
+def sum_to_iter : mv_polynomial (β ⊕ γ) α → mv_polynomial β (mv_polynomial γ α) :=
+eval₂ (C ∘ C) (λbc, sum.rec_on bc X (C ∘ X))
+
+instance is_semiring_hom_C_C :
+  is_semiring_hom (C ∘ C : α → mv_polynomial β (mv_polynomial γ α)) :=
+@is_semiring_hom.comp _ _ _ _ C mv_polynomial.is_semiring_hom _ _ C mv_polynomial.is_semiring_hom
+
+instance is_semiring_hom_sum_to_iter : is_semiring_hom (sum_to_iter α β γ) :=
+eval₂.is_semiring_hom _ _
+
+lemma sum_to_iter_C (a : α) : sum_to_iter α β γ (C a) = C (C a) :=
+eval₂_C _ _ a
+
+lemma sum_to_iter_Xl (b : β) : sum_to_iter α β γ (X (sum.inl b)) = X b :=
+eval₂_X _ _ (sum.inl b)
+
+lemma sum_to_iter_Xr (c : γ) : sum_to_iter α β γ (X (sum.inr c)) = C (X c) :=
+eval₂_X _ _ (sum.inr c)
+
+def iter_to_sum : mv_polynomial β (mv_polynomial γ α) → mv_polynomial (β ⊕ γ) α :=
+eval₂ (eval₂ C (X ∘ sum.inr)) (X ∘ sum.inl)
+
+section
+
+instance is_semiring_hom_iter_to_sum : is_semiring_hom (iter_to_sum α β γ) :=
+eval₂.is_semiring_hom _ _
+
+end
+
+lemma iter_to_sum_C_C (a : α) : iter_to_sum α β γ (C (C a)) = C a :=
+eq.trans (eval₂_C _ _ (C a)) (eval₂_C _ _ _)
+
+lemma iter_to_sum_X (b : β) : iter_to_sum α β γ (X b) = X (sum.inl b) :=
+eval₂_X _ _ _
+
+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 _ _ _)
+
+def mv_polynomial_equiv_mv_polynomial [comm_ring δ]
+  (f : mv_polynomial β α → mv_polynomial γ δ) (hf : is_semiring_hom f)
+  (g : mv_polynomial γ δ → mv_polynomial β α) (hg : is_semiring_hom g)
+  (hfgC : ∀a, f (g (C a)) = C a)
+  (hfgX : ∀n, f (g (X n)) = X n)
+  (hgfC : ∀a, g (f (C a)) = C a)
+  (hgfX : ∀n, g (f (X n)) = X n) :
+  mv_polynomial β α ≃r mv_polynomial γ δ :=
+{ to_fun    := f, inv_fun := g,
+  left_inv  := is_id _ (is_semiring_hom.comp _ _) hgfC hgfX,
+  right_inv := is_id _ (is_semiring_hom.comp _ _) hfgC hfgX,
+  hom       := is_ring_hom.of_semiring f }
+
+def sum_ring_equiv : mv_polynomial (β ⊕ γ) α ≃r mv_polynomial β (mv_polynomial γ α) :=
+begin
+  apply @mv_polynomial_equiv_mv_polynomial α (β ⊕ γ) _ _ _ _ _ _ _ _
+    (sum_to_iter α β γ) _ (iter_to_sum α β γ) _,
+  { assume p,
+    apply @hom_eq_hom _ _ _ _ _ _ _ _ _ _ _ _ _ p,
+    apply_instance,
+    { apply @is_semiring_hom.comp _ _ _ _ _ _ _ _ _ _,
+      apply_instance,
+      apply @is_semiring_hom.comp _ _ _ _ _ _ _ _ _ _,
+      apply_instance,
+      { apply @mv_polynomial.is_semiring_hom },
+      { apply mv_polynomial.is_semiring_hom_iter_to_sum α β γ },
+      { apply mv_polynomial.is_semiring_hom_sum_to_iter α β γ } },
+    { apply mv_polynomial.is_semiring_hom },
+    { assume a, rw [iter_to_sum_C_C α β γ, sum_to_iter_C α β γ] },
+    { assume c, rw [iter_to_sum_C_X α β γ, sum_to_iter_Xr α β γ] } },
+  { assume b, rw [iter_to_sum_X α β γ, sum_to_iter_Xl α β γ] },
+  { assume a, rw [sum_to_iter_C α β γ, iter_to_sum_C_C α β γ] },
+  { assume n, cases n with b c,
+    { rw [sum_to_iter_Xl, iter_to_sum_X] },
+    { rw [sum_to_iter_Xr, iter_to_sum_C_X] } },
+  { apply mv_polynomial.is_semiring_hom_sum_to_iter α β γ },
+  { apply mv_polynomial.is_semiring_hom_iter_to_sum α β γ }
+end
+
+instance option_ring : ring (mv_polynomial (option β) α) :=
+mv_polynomial.ring
+
+instance polynomial_ring : ring (polynomial (mv_polynomial β α)) :=
+@comm_ring.to_ring _ polynomial.comm_ring
+
+instance polynomial_ring2 : ring (mv_polynomial β (polynomial α)) :=
+by apply_instance
+
+def option_equiv_left : mv_polynomial (option β) α ≃r polynomial (mv_polynomial β α) :=
+(ring_equiv_of_equiv α $ (equiv.option_equiv_sum_punit β).trans (equiv.sum_comm _ _)).trans $
+(sum_ring_equiv α _ _).trans $
+punit_ring_equiv _
+
+def option_equiv_right : mv_polynomial (option β) α ≃r mv_polynomial β (polynomial α) :=
+(ring_equiv_of_equiv α $ equiv.option_equiv_sum_punit.{0} β).trans $
+(sum_ring_equiv α β unit).trans $
+ring_equiv_congr (mv_polynomial unit α) (punit_ring_equiv α)
+
+end
+
+end equiv
+
 end mv_polynomial

src/ring_theory/noetherian.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Kevin Buzzard
 -/
 
 import data.equiv.algebra
-import data.polynomial
 import linear_algebra.linear_combination
 import ring_theory.ideal_operations
 import ring_theory.subring