feat(Algebra/Polynomial/Roots): Action of group on rootSet (#33919)

This PR adds an instance for `MulAction G (f.rootSet R)` whenever a `MulSemiringAction G R` satisfies `SMulCommClass G S R`.

Co-authored-by: tb65536 <[email protected]>

Author: tb65536

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -400,7 +400,7 @@ theorem aeval_algHom_apply {F : Type*} [FunLike F A B] [AlgHomClass F R A B]
     (by simp [AlgHomClass.commutes])
   rw [map_add, hp, hq, ← map_add, ← map_add]
 
-theorem aeval_smul (f : R[X]) {G : Type*} [Group G] [MulSemiringAction G A] [SMulCommClass G R A]
+theorem aeval_smul (f : R[X]) {G : Type*} [Monoid G] [MulSemiringAction G A] [SMulCommClass G R A]
     (g : G) (x : A) : f.aeval (g • x) = g • (f.aeval x) := by
   rw [← MulSemiringAction.toAlgHom_apply R, aeval_algHom_apply, MulSemiringAction.toAlgHom_apply]
 

Mathlib/Algebra/Polynomial/Roots.lean

@@ -637,6 +637,48 @@ theorem nthRootsFinset_toSet {n : ℕ} (h : 0 < n) (a : R) :
   ext x
   simp_all
 
+theorem smul_mem_rootSet [CommRing S] [Algebra S R] {G : Type*}
+    [Monoid G] [MulSemiringAction G R] [SMulCommClass G S R] {f : S[X]}
+    (g : G) {x : R} (hx : x ∈ f.rootSet R) : g • x ∈ f.rootSet R := by
+  simp [mem_rootSet', aeval_smul, aeval_eq_zero_of_mem_rootSet hx, (mem_rootSet'.mp hx).1]
+
+theorem smul_mem_rootSet_iff_of_isUnit [CommRing S] [Algebra S R] {G : Type*}
+    [Monoid G] [MulSemiringAction G R] [SMulCommClass G S R] {f : S[X]}
+    {g : G} (hg : IsUnit g) {x : R} : g • x ∈ f.rootSet R ↔ x ∈ f.rootSet R := by
+  refine ⟨?_, smul_mem_rootSet g⟩
+  obtain ⟨g, rfl⟩ := hg
+  exact fun hx ↦ inv_smul_smul g x ▸ smul_mem_rootSet _ hx
+
+theorem smul_mem_rootSet_iff [CommRing S] [Algebra S R] {G : Type*}
+    [Group G] [MulSemiringAction G R] [SMulCommClass G S R] {f : S[X]}
+    {g : G} {x : R} : g • x ∈ f.rootSet R ↔ x ∈ f.rootSet R :=
+  smul_mem_rootSet_iff_of_isUnit (Group.isUnit g)
+
+instance [CommRing S] [Algebra S R] (G : Type*)
+    [Monoid G] [MulSemiringAction G R] [SMulCommClass G S R] (f : S[X]) :
+    MulAction G (f.rootSet R) where
+  smul g x := ⟨g • x.1, smul_mem_rootSet g x.2⟩
+  one_smul x := Subtype.ext (one_smul G x.1)
+  mul_smul g h x := Subtype.ext (mul_smul g h x.1)
+
+@[simp]
+theorem rootSet.coe_smul [CommRing S] [Algebra S R] {G : Type*}
+    [Monoid G] [MulSemiringAction G R] [SMulCommClass G S R] {f : S[X]}
+    (g : G) (x : f.rootSet R) : (g • x : f.rootSet R) = g • (x : R) :=
+  rfl
+
+instance [CommRing S] [Algebra S R] (G H : Type*)
+    [Monoid G] [MulSemiringAction G R] [SMulCommClass G S R]
+    [Monoid H] [MulSemiringAction H R] [SMulCommClass H S R]
+    [SMulCommClass G H R] (f : S[X]) : SMulCommClass G H (f.rootSet R) where
+  smul_comm _ _ _ := Subtype.ext <| smul_comm _ _ _
+
+instance [CommRing S] [Algebra S R] (G H : Type*)
+    [Monoid G] [MulSemiringAction G R] [SMulCommClass G S R]
+    [Monoid H] [MulSemiringAction H R] [SMulCommClass H S R]
+    [SMul G H] [IsScalarTower G H R] (f : S[X]) : IsScalarTower G H (f.rootSet R) where
+  smul_assoc _ _ _ := Subtype.ext <| smul_assoc _ _ _
+
 end Roots
 
 lemma eq_zero_of_natDegree_lt_card_of_eval_eq_zero {R} [CommRing R] [IsDomain R]