chore(Algebra/Polynomial/Splits): remove field hypothesis from map_aroots_algebraMap (#41056)

Currently `Polynomial.Splits.map_aroots_algebraMap` assumes that `A` is a field. But actually it is enough to assume that the map from `A` to `B` is injective. This PR also adds a `rootSet` version `Polynomial.Splits.image_rootSet_algebraMap`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/Algebra/Polynomial/Splits.lean

@@ -572,11 +572,6 @@ section
 variable {A B : Type*} [CommRing R] [Field A] [Algebra R A]
   [CommRing B] [IsDomain B] [Algebra R B] {f : R[X]}
 
-theorem Splits.map_aroots_algebraMap [Algebra A B] [IsScalarTower R A B]
-    (hf : (f.map (algebraMap R A)).Splits) :
-    (f.aroots A).map (algebraMap A B) = f.aroots B := by
-  rw [← aroots_map B A, aroots, aroots, hf.roots_map]
-
 theorem Splits.image_rootSet (hf : (f.map (algebraMap R A)).Splits)
     (g : A →ₐ[R] B) : g '' f.rootSet A = f.rootSet B := by
   classical
@@ -591,6 +586,23 @@ theorem Splits.adjoin_rootSet_eq_range
 
 end
 
+section
+
+variable {A B : Type*} [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] [CommRing B]
+  [IsDomain B] [Algebra R B] [Algebra A B] [FaithfulSMul A B] [IsScalarTower R A B] {f : R[X]}
+
+theorem Splits.map_aroots_algebraMap (hf : (f.map (algebraMap R A)).Splits) :
+    (f.aroots A).map (algebraMap A B) = f.aroots B := by
+  rw [← aroots_map B A, aroots, aroots,
+    hf.roots_map_of_injective (FaithfulSMul.algebraMap_injective A B)]
+
+theorem Splits.image_rootSet_algebraMap (hf : (f.map (algebraMap R A)).Splits) :
+    (algebraMap A B) '' f.rootSet A = f.rootSet B := by
+  classical
+  rw [rootSet, ← Finset.coe_image, ← Multiset.toFinset_map, hf.map_aroots_algebraMap, ← rootSet]
+
+end
+
 variable [Field R] {f g : R[X]}
 
 theorem Splits.dvd_of_roots_le_roots (hp : f.Splits) (hp0 : f ≠ 0) (hq : f.roots ≤ g.roots) :