From e66e136f48e48c97f953f103d598522abeac481c Mon Sep 17 00:00:00 2001
From: Riccardo Brasca <riccardo.brasca@gmail.com>
Date: Wed, 24 Feb 2021 22:06:41 +0000
Subject: [PATCH] feat(data/mv_polynomial/basic): add two equivs (#6324)

Two small lemma about `mv_polynomial` as `R`-algebra.
---
 src/data/mv_polynomial/equiv.lean | 60 +++++++++++++++++++++++++------
 src/ring_theory/finiteness.lean   |  4 +--
 2 files changed, 51 insertions(+), 13 deletions(-)

diff --git a/src/data/mv_polynomial/equiv.lean b/src/data/mv_polynomial/equiv.lean
index 25df8784f3f9c..820fa86ca3088 100644
--- a/src/data/mv_polynomial/equiv.lean
+++ b/src/data/mv_polynomial/equiv.lean
@@ -115,17 +115,6 @@ def ring_equiv_of_equiv (e : S₁ ≃ S₂) : mv_polynomial S₁ R ≃+* mv_poly
   map_mul'  := (rename e).map_mul,
   map_add'  := (rename e).map_add }
 
-/-- The algebra isomorphism between multivariable polynomials induced by an equivalence
-of the variables.  -/
-@[simps]
-def alg_equiv_of_equiv (e : S₁ ≃ S₂) : mv_polynomial S₁ R ≃ₐ[R] mv_polynomial S₂ R :=
-{ to_fun    := rename e,
-  inv_fun   := rename e.symm,
-  left_inv  := λ p, by simp only [rename_rename, (∘), e.symm_apply_apply]; exact rename_id p,
-  right_inv := λ p, by simp only [rename_rename, (∘), e.apply_symm_apply]; exact rename_id p,
-  commutes' := λ p, by simp only [alg_hom.commutes],
-  .. rename e }
-
 /-- The ring isomorphism between multivariable polynomials induced by a ring isomorphism
 of the ground ring. -/
 @[simps]
@@ -144,6 +133,37 @@ def ring_equiv_congr [comm_semiring S₂] (e : R ≃+* S₂) :
   map_mul'  := ring_hom.map_mul _,
   map_add'  := ring_hom.map_add _ }
 
+/-- If `e : A ≃ₐ[R] B` is an isomorphism of `R`-algebas and `e_var : S₁ ≃ S₂` is an isomorphism of
+types, the induced isomorphism `mv_polynomial S₁ A ≃ₐ[R] mv_polynomial S₂ B`. -/
+def alg_equiv_congr {A B : Type*} [comm_semiring A] [comm_semiring B] [algebra R A] [algebra R B]
+  (e : A ≃ₐ[R] B) (e_var : S₁ ≃ S₂) :
+  algebra.comap R A (mv_polynomial S₁ A) ≃ₐ[R] algebra.comap R B (mv_polynomial S₂ B) :=
+{ commutes' := begin
+  intro r,
+  dsimp,
+  have h₁ : algebra_map R (algebra.comap R A (mv_polynomial S₁ A)) r =
+    C (algebra_map R A r) := rfl,
+  have h₂ : algebra_map R (algebra.comap R B (mv_polynomial S₂ B)) r =
+    C (algebra_map R B r) := rfl,
+  have h : (↑(e.to_ring_equiv) : A →+* B) ((algebra_map R A) r) = e ((algebra_map R A) r) := rfl,
+  rw [h₁, h₂, map, rename_C, eval₂_hom_C, ring_hom.comp_apply, h, alg_equiv.commutes],
+  end,
+  .. (ring_equiv_of_equiv A e_var).trans (ring_equiv_congr A e.to_ring_equiv)
+}
+
+/-- The algebra isomorphism between multivariable polynomials induced by an equivalence
+of the variables.  -/
+@[simps]
+def alg_equiv_congr_left (e : S₁ ≃ S₂) : mv_polynomial S₁ R ≃ₐ[R] mv_polynomial S₂ R :=
+alg_equiv_congr R alg_equiv.refl e
+
+/-- If `e : A ≃ₐ[R] B` is an isomorphism of `R`-algebas, the induced isomorphism
+`mv_polynomial S₁ A ≃ₐ[R] mv_polynomial S₁ B`. -/
+def alg_equiv_congr_right {A B : Type*} [comm_semiring A] [comm_semiring B] [algebra R A]
+  [algebra R B] (e : A ≃ₐ[R] B) :
+  algebra.comap R A (mv_polynomial S₁ A) ≃ₐ[R] algebra.comap R B (mv_polynomial S₁ B) :=
+alg_equiv_congr R e (equiv.cast rfl)
+
 section
 variables (S₁ S₂ S₃)
 
@@ -227,6 +247,24 @@ begin
     { rw [sum_to_iter_Xr, iter_to_sum_C_X] } },
 end
 
+/--
+The algebra isomorphism between multivariable polynomials in a sum of two types,
+and multivariable polynomials in one of the types,
+with coefficents in multivariable polynomials in the other type.
+-/
+def sum_alg_equiv : mv_polynomial (S₁ ⊕ S₂) R ≃ₐ[R]
+  algebra.comap R (mv_polynomial S₂ R) (mv_polynomial S₁ (mv_polynomial S₂ R)) :=
+{ commutes' := begin
+    intro r,
+    change algebra_map R (algebra.comap R (mv_polynomial S₂ R)
+      (mv_polynomial S₁ (mv_polynomial S₂ R))) r with C (C r),
+    change algebra_map R (mv_polynomial (S₁ ⊕ S₂) R) r with C r,
+    simp only [sum_ring_equiv, sum_to_iter_C, mv_polynomial_equiv_mv_polynomial_apply,
+      ring_equiv.to_fun_eq_coe]
+  end,
+  ..sum_ring_equiv R S₁ S₂
+}
+
 /--
 The ring isomorphism between multivariable polynomials in `option S₁` and
 polynomials with coefficients in `mv_polynomial S₁ R`.
diff --git a/src/ring_theory/finiteness.lean b/src/ring_theory/finiteness.lean
index d91e332e979fc..25158db47708f 100644
--- a/src/ring_theory/finiteness.lean
+++ b/src/ring_theory/finiteness.lean
@@ -181,7 +181,7 @@ begin
   { rw iff_quotient_mv_polynomial',
     rintro ⟨ι, hfintype, ⟨f, hsur⟩⟩,
     obtain ⟨n, equiv⟩ := @fintype.exists_equiv_fin ι hfintype,
-    replace equiv := mv_polynomial.alg_equiv_of_equiv R (nonempty.some equiv),
+    replace equiv := mv_polynomial.alg_equiv_congr_left R (nonempty.some equiv),
     use [n, alg_hom.comp f equiv.symm, function.surjective.comp hsur
       (alg_equiv.symm equiv).surjective] },
   { rintro ⟨n, ⟨f, hsur⟩⟩,
@@ -225,7 +225,7 @@ variable (R)
 lemma mv_polynomial (ι : Type u_2) [fintype ι] : finitely_presented R (mv_polynomial ι R) :=
 begin
   obtain ⟨n, equiv⟩ := @fintype.exists_equiv_fin ι _,
-  replace equiv := mv_polynomial.alg_equiv_of_equiv R (nonempty.some equiv),
+  replace equiv := mv_polynomial.alg_equiv_congr_left R (nonempty.some equiv),
   use [n, alg_equiv.to_alg_hom equiv.symm],
   split,
   { exact (alg_equiv.symm equiv).surjective },