refactor(data/equiv/algebra): mv_polynomial mv_polynomial (β ⊕ γ) α ≃…

…r mv_polynomial β (mv_polynomial γ α)

src/data/equiv/algebra.lean

@@ -5,8 +5,8 @@ Authors: Johannes Hölzl
 -/
 import data.equiv.basic data.polynomial linear_algebra.multivariate_polynomial
 
-universes u v w
-variables {α : Type u} {β : Type v} {γ : Type w}
+universes u v w x
+variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 
 namespace equiv
 
@@ -219,101 +219,197 @@ end ring_equiv
 namespace mv_polynomial
 
 variables (α) [comm_ring α]
-variables [decidable_eq α] [decidable_eq β] [decidable_eq γ]
+variables [decidable_eq α] [decidable_eq β] [decidable_eq γ] [decidable_eq δ]
+
+section
+variable {α}
+
+def rename (f : β → γ) : mv_polynomial β α → mv_polynomial γ α :=
+eval₂ C (X ∘ f)
+
+instance is_ring_hom_rename (f : β → γ) :
+  is_ring_hom (rename f : mv_polynomial β α → mv_polynomial γ α) :=
+by unfold rename; apply_instance
+
+@[simp] lemma rename_C (f : β → γ) (a : α) : rename f (C a) = C a :=
+eval₂_C _ _ _
+
+@[simp] lemma rename_X (f : β → γ) (b : β) : rename f (X b : mv_polynomial β α) = X (f b) :=
+eval₂_X _ _ _
+
+lemma rename_rename (f : β → γ) (g : γ → δ) (p : mv_polynomial β α) :
+  rename g (rename f p) = rename (g ∘ f) p :=
+show rename g (eval₂ C (X ∘ f) p) = _,
+  by simp only [eval₂_comp_left (rename g) C (X ∘ f) p, (∘), rename_C, rename_X]; refl
+
+lemma rename_id (p : mv_polynomial β α) : rename id p = p :=
+eval₂_eta p
+
+lemma hom_eq_hom [semiring γ]
+  (f g : mv_polynomial β α → γ) (hf : is_semiring_hom f) (hg : is_semiring_hom g)
+  (hC : ∀a:α, f (C a) = g (C a)) (hX : ∀n:β, f (X n) = g (X n)) (p : mv_polynomial β α) :
+  f p = g p :=
+mv_polynomial.induction_on p hC
+  begin assume p q hp hq, rw [is_semiring_hom.map_add f, is_semiring_hom.map_add g, hp, hq] end
+  begin assume p n hp, rw [is_semiring_hom.map_mul f, is_semiring_hom.map_mul g, hp, hX] end
+
+lemma is_id (f : mv_polynomial β α → mv_polynomial β α) (hf : is_semiring_hom f)
+  (hC : ∀a:α, f (C a) = (C a)) (hX : ∀n:β, f (X n) = (X n)) (p : mv_polynomial β α) :
+  f p = p :=
+mv_polynomial.induction_on p hC
+  begin assume p q hp hq, rw [is_semiring_hom.map_add f, hp, hq] end
+  begin assume p n hp, rw [is_semiring_hom.map_mul f, hp, hX] end
+
+end
+
+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 := eval₂ C (X ∘ e),
-  inv_fun := eval₂ C (X ∘ e.symm),
-  left_inv := λ f, induction_on f
-    (λ r, by rw [eval₂_C, eval₂_C])
-    (λ p q hp hq, by rw [eval₂_add, eval₂_add, hp, hq])
-    (λ p s hp, by simp only [eval₂_mul, eval₂_X, hp, (∘), equiv.inverse_apply_apply]),
-  right_inv := λ f, induction_on f
-    (λ r, by rw [eval₂_C, eval₂_C])
-    (λ p q hp hq, by rw [eval₂_add, eval₂_add, hp, hq])
-    (λ p s hp, by simp only [eval₂_mul, eval₂_X, hp, (∘), equiv.apply_inverse_apply]),
-  hom := by apply eval₂.is_ring_hom }
-
-variables (β)
-set_option class.instance_max_depth 10
-def of_option : mv_polynomial (option β) α → polynomial (mv_polynomial β α) :=
-eval₂ (polynomial.C ∘ C) (λ x, option.rec_on x polynomial.X (polynomial.C ∘ X))
-
-def to_option : polynomial (mv_polynomial β α) → mv_polynomial (option β) α :=
-polynomial.eval₂ (eval₂ C (X ∘ some)) (X none)
-
-variables {α β}
-theorem of_option_C (r : α) : of_option α β (C r) = polynomial.C (C r) :=
-by convert eval₂_C _ _ _; convert is_semiring_hom.comp _ _; apply_instance
-
-theorem of_option_X_none : of_option α β (X none) = polynomial.X :=
-by convert eval₂_X _ _ _; convert is_semiring_hom.comp _ _; apply_instance
-
-theorem of_option_X_some (n : β) : of_option α β (X (some n)) = polynomial.C (X n) :=
-by convert eval₂_X _ _ _; convert is_semiring_hom.comp _ _; apply_instance
-
-theorem of_option_add (p q) : of_option α β (p + q) = of_option α β p + of_option α β q :=
-by convert eval₂_add _ _; convert is_semiring_hom.comp _ _; apply_instance
-
-theorem of_option_mul (p q) : of_option α β (p * q) = of_option α β p * of_option α β q :=
-by convert eval₂_mul _ _; convert is_semiring_hom.comp _ _; apply_instance
-
-theorem to_option_C (g) : to_option α β (polynomial.C g) = eval₂ C (X ∘ some) g :=
-by apply polynomial.eval₂_C _ _; apply eval₂.is_semiring_hom _ _; convert is_ring_hom.is_semiring_hom C; apply C.is_ring_hom
-
-theorem to_option_C_C (r : α) : to_option α β (polynomial.C (C r)) = C r :=
-by rw to_option_C; apply eval₂_C _ _ _; convert is_ring_hom.is_semiring_hom C; apply C.is_ring_hom
-
-theorem to_option_C_X (n : β) : to_option α β (polynomial.C (X n)) = X (some n) :=
-by rw to_option_C; apply eval₂_X _ _ _; convert is_ring_hom.is_semiring_hom C; apply C.is_ring_hom
-
-theorem to_option_X : to_option α β (polynomial.X) = X none :=
-by apply polynomial.eval₂_X _ _; apply eval₂.is_semiring_hom _ _; convert is_ring_hom.is_semiring_hom C; apply C.is_ring_hom
-
-theorem to_option_add (p q) : to_option α β (p + q) = to_option α β p + to_option α β q :=
-by apply polynomial.eval₂_add _ _; apply eval₂.is_semiring_hom _ _; convert is_ring_hom.is_semiring_hom C; apply C.is_ring_hom
-
-theorem to_option_mul (p q) : to_option α β (p * q) = to_option α β p * to_option α β q :=
-by apply polynomial.eval₂_mul _ _; apply eval₂.is_semiring_hom _ _; convert is_ring_hom.is_semiring_hom C; apply C.is_ring_hom
-
-set_option class.instance_max_depth 15
-theorem to_option_of_option (f) : to_option α β (of_option α β f) = f :=
-induction_on f
-  (λ r, by rw [of_option_C, to_option_C_C])
-  (λ p q hp hq, by rw [of_option_add, to_option_add, hp, hq])
-  (λ p n h, option.rec_on n (by rw [of_option_mul, to_option_mul, h, of_option_X_none, to_option_X]) $ λ n,
-    by rw [of_option_mul, to_option_mul, h, of_option_X_some, to_option_C_X])
-
-theorem of_option_to_option (f : polynomial (mv_polynomial β α)) : of_option α β (to_option α β f) = f :=
-polynomial.induction_on f
-  (λ g, induction_on g
-    (λ r, by rw [to_option_C_C, of_option_C])
-    (λ p q hp hq, by rw [polynomial.C_add, to_option_add, of_option_add, hp, hq])
-    (λ p n h, by rw [polynomial.C_mul, to_option_mul, of_option_mul, h, to_option_C_X, of_option_X_some]))
-  (λ p q hp hq, by rw [to_option_add, of_option_add, hp, hq])
-  (λ n g h, by rw [to_option_mul, of_option_mul, pow_succ', to_option_mul, of_option_mul,
-    ← mul_assoc, ← of_option_mul, ← to_option_mul, h, to_option_X, of_option_X_none, mul_assoc])
+{ 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       := mv_polynomial.is_ring_hom_rename _ }
+
+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_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
 
-def option_ring_equiv : mv_polynomial (option β) α ≃r polynomial (mv_polynomial β α) :=
-{ to_fun := of_option α β,
-  inv_fun := to_option α β,
-  left_inv := to_option_of_option,
-  right_inv := of_option_to_option,
-  hom := ⟨of_option_C 1, of_option_mul, of_option_add⟩ }
+instance polynomial_ring2 : ring (mv_polynomial β (polynomial α)) :=
+by apply_instance
 
-def pempty_ring_equiv : mv_polynomial pempty α ≃r α :=
-{ to_fun := mv_polynomial.eval₂ id $ pempty.rec _,
-  inv_fun := C,
-  left_inv := λ f, induction_on f (λ r, congr_arg _ $ eval₂_C _ _ _)
-    (λ p q hp hq, by rw [eval₂_add, C_add, hp, hq])
-    (λ p, pempty.rec _),
-  right_inv := λ r, eval₂_C _ _ _,
-  hom := eval₂.is_ring_hom _ _ }
+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

@@ -155,6 +155,10 @@ begin
   { simp [X, eval₂_monomial, eval₂_mul_monomial, (mul_assoc _ _ _).symm] { contextual := tt} }
 end
 
+lemma eval₂_pow {p:mv_polynomial σ α} : ∀{n:ℕ}, (p ^ n).eval₂ f g = (p.eval₂ f g)^n
+| 0       := eval₂_one _ _
+| (n + 1) := by rw [pow_add, pow_one, pow_add, pow_one, eval₂_mul, eval₂_pow]
+
 instance eval₂.is_semiring_hom : is_semiring_hom (eval₂ f g) :=
 { map_zero := eval₂_zero _ _,
   map_one := eval₂_one _ _,