From 86444d8d24fc56165ba8549ae96b85e8905be8e7 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Sun, 24 Mar 2024 22:59:09 +0000
Subject: [PATCH] feat: renaming symmetric MvPolynomials (#11251)

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
---
 .../RingTheory/MvPolynomial/Symmetric.lean    | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/Mathlib/RingTheory/MvPolynomial/Symmetric.lean b/Mathlib/RingTheory/MvPolynomial/Symmetric.lean
index ec13ab3411d2a..173a9b11fdd01 100644
--- a/Mathlib/RingTheory/MvPolynomial/Symmetric.lean
+++ b/Mathlib/RingTheory/MvPolynomial/Symmetric.lean
@@ -138,6 +138,16 @@ theorem map (hφ : IsSymmetric φ) (f : R →+* S) : IsSymmetric (map f φ) := f
   rw [← map_rename, hφ]
 #align mv_polynomial.is_symmetric.map MvPolynomial.IsSymmetric.map
 
+protected theorem rename (hφ : φ.IsSymmetric) (e : σ ≃ τ) : (rename e φ).IsSymmetric := fun _ => by
+  apply rename_injective _ e.symm.injective
+  simp_rw [rename_rename, ← Equiv.coe_trans, Equiv.self_trans_symm, Equiv.coe_refl, rename_id]
+  rw [hφ]
+
+@[simp]
+theorem _root_.MvPolynomial.isSymmetric_rename {e : σ ≃ τ} :
+    (MvPolynomial.rename e φ).IsSymmetric ↔ φ.IsSymmetric :=
+  ⟨fun h => by simpa using (IsSymmetric.rename (R := R) h e.symm), (IsSymmetric.rename · e)⟩
+
 end CommSemiring
 
 section CommRing
@@ -156,6 +166,16 @@ end CommRing
 
 end IsSymmetric
 
+/-- `MvPolynomial.rename` induces an isomorphism between the symmetric subalgebras. -/
+@[simps!]
+def renameSymmetricSubalgebra [CommSemiring R] (e : σ ≃ τ) :
+    symmetricSubalgebra σ R ≃ₐ[R] symmetricSubalgebra τ R :=
+  AlgEquiv.ofAlgHom
+    (((rename e).comp (symmetricSubalgebra σ R).val).codRestrict _ <| fun x => x.2.rename e)
+    (((rename e.symm).comp <| Subalgebra.val _).codRestrict _ <| fun x => x.2.rename e.symm)
+    (AlgHom.ext <| fun p => Subtype.ext <| by simp)
+    (AlgHom.ext <| fun p => Subtype.ext <| by simp)
+
 section ElementarySymmetric
 
 open Finset