feat(Algebra/Polynomial/Splits): remove the RingHom argument of Splits (#31631)

Author: SnirBroshi

Mathlib/Algebra/CubicDiscriminant.lean

@@ -413,14 +413,14 @@ variable {P : Cubic F} [Field F] [Field K] {φ : F →+* K} {x y z : K}
 section Split
 
 theorem splits_iff_card_roots (ha : P.a ≠ 0) :
-    Splits φ P.toPoly ↔ Multiset.card (map φ P).roots = 3 := by
+    Splits (P.toPoly.map φ) ↔ Multiset.card (map φ P).roots = 3 := by
   replace ha : (map φ P).a ≠ 0 := (_root_.map_ne_zero φ).mpr ha
   nth_rw 1 [← RingHom.id_comp φ]
   rw [roots, ← splits_map_iff, ← map_toPoly, Polynomial.splits_iff_card_roots,
     ← ((degree_eq_iff_natDegree_eq <| ne_zero_of_a_ne_zero ha).1 <| degree_of_a_ne_zero ha : _ = 3)]
 
 theorem splits_iff_roots_eq_three (ha : P.a ≠ 0) :
-    Splits φ P.toPoly ↔ ∃ x y z : K, (map φ P).roots = {x, y, z} := by
+    Splits (P.toPoly.map φ) ↔ ∃ x y z : K, (map φ P).roots = {x, y, z} := by
   rw [splits_iff_card_roots ha, card_eq_three]
 
 theorem eq_prod_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :

Mathlib/Algebra/Polynomial/Splits.lean

@@ -61,7 +61,7 @@ namespace Polynomial.Gal
 
 section Rationals
 
-theorem splits_ℚ_ℂ {p : ℚ[X]} : Fact (p.Splits (algebraMap ℚ ℂ)) :=
+theorem splits_ℚ_ℂ {p : ℚ[X]} : Fact ((p.map (algebraMap ℚ ℂ)).Splits) :=
   ⟨IsAlgClosed.splits_codomain p⟩
 
 attribute [local instance] splits_ℚ_ℂ

Mathlib/Analysis/Complex/Polynomial/Basic.lean

@@ -182,7 +182,7 @@ lemma eigenvalues_eq_eigenvalues_iff :
   · suffices hA.eigenvalues₀ = hB.eigenvalues₀ by unfold eigenvalues; rw [this]
     simp_rw [← List.ofFn_inj, ← sort_roots_charpoly_eq_eigenvalues₀, h]
 
-theorem splits_charpoly (hA : A.IsHermitian) : A.charpoly.Splits (RingHom.id 𝕜) :=
+theorem splits_charpoly (hA : A.IsHermitian) : (A.charpoly.map (RingHom.id 𝕜)).Splits :=
   Polynomial.splits_iff_card_roots.mpr (by simp [hA.roots_charpoly_eq_eigenvalues])
 
 /-- The determinant of a Hermitian matrix is the product of its eigenvalues. -/

Mathlib/Analysis/Matrix/Spectrum.lean

@@ -483,7 +483,7 @@ theorem spectralNorm_eq_iSup_of_finiteDimensional_normal
     norm_root_le_spectralValue hf_pm hf_na
       (minpoly.monic (hn.isIntegral x)) (minpoly.aeval_algHom _ σ.toAlgHom _))
   · set p := minpoly K x
-    have hp_sp : Splits (algebraMap K L) (minpoly K x) := hn.splits x
+    have hp_sp : Splits ((minpoly K x).map (algebraMap K L)) := hn.splits x
     obtain ⟨s, hs⟩ := (splits_iff_exists_multiset _).mp hp_sp
     have h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1 := by
       rw [minpoly.monic (hn.isIntegral x), map_one]
@@ -953,7 +953,7 @@ theorem spectralNorm_pow_natDegree_eq_prod_roots (x : L) {E : Type*} [Field E] [
 theorem spectralNorm_eq_norm_coeff_zero_rpow (x : L) :
     spectralNorm K L x = ‖(minpoly K x).coeff 0‖ ^ (1 / (minpoly K x).natDegree : ℝ) := by
   set E := (mapAlg K L (minpoly K x)).SplittingField
-  have hspl : Splits (RingHom.id E) (mapAlg K E (minpoly K x)) :=
+  have hspl : Splits ((mapAlg K E (minpoly K x)).map (RingHom.id E)) :=
     IsSplittingField.IsScalarTower.splits (K := L) E (minpoly K x)
   have : Algebra.IsAlgebraic L E :=
     IsSplittingField.IsScalarTower.isAlgebraic E (mapAlg K L (minpoly K x))

Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

@@ -60,17 +60,17 @@ theorem gal_prod_isSolvable {s : Multiset F[X]} (hs : ∀ p ∈ s, IsSolvable (G
     exact gal_mul_isSolvable (hs p hps) ht
 
 theorem gal_isSolvable_of_splits {p q : F[X]}
-    (_ : Fact (p.Splits (algebraMap F q.SplittingField))) (hq : IsSolvable q.Gal) :
+    (_ : Fact ((p.map (algebraMap F q.SplittingField)).Splits)) (hq : IsSolvable q.Gal) :
     IsSolvable p.Gal :=
   haveI : IsSolvable (q.SplittingField ≃ₐ[F] q.SplittingField) := hq
   solvable_of_surjective (AlgEquiv.restrictNormalHom_surjective q.SplittingField)
 
-theorem gal_isSolvable_tower (p q : F[X]) (hpq : p.Splits (algebraMap F q.SplittingField))
+theorem gal_isSolvable_tower (p q : F[X]) (hpq : (p.map (algebraMap F q.SplittingField)).Splits)
     (hp : IsSolvable p.Gal) (hq : IsSolvable (q.map (algebraMap F p.SplittingField)).Gal) :
     IsSolvable q.Gal := by
   let K := p.SplittingField
   let L := q.SplittingField
-  haveI : Fact (p.Splits (algebraMap F L)) := ⟨hpq⟩
+  haveI : Fact ((p.map (algebraMap F L)).Splits) := ⟨hpq⟩
   let ϕ : Gal(L/K) ≃* (q.map (algebraMap F K)).Gal :=
     (IsSplittingField.algEquiv L (q.map (algebraMap F K))).autCongr
   have ϕ_inj : Function.Injective ϕ.toMonoidHom := ϕ.injective
@@ -99,7 +99,7 @@ theorem gal_X_pow_sub_one_isSolvable (n : ℕ) : IsSolvable (X ^ n - 1 : F[X]).G
   rw [σ.mul_apply, τ.mul_apply, hc, map_pow, hd, map_pow, hc, ← pow_mul, pow_mul']
 
 theorem gal_X_pow_sub_C_isSolvable_aux (n : ℕ) (a : F)
-    (h : (X ^ n - 1 : F[X]).Splits (RingHom.id F)) : IsSolvable (X ^ n - C a).Gal := by
+    (h : ((X ^ n - 1 : F[X]).map (RingHom.id F)).Splits) : IsSolvable (X ^ n - C a).Gal := by
   by_cases ha : a = 0
   · rw [ha, C_0, sub_zero]
     exact gal_X_pow_isSolvable n
@@ -136,12 +136,11 @@ theorem gal_X_pow_sub_C_isSolvable_aux (n : ℕ) (a : F)
     mul_assoc, mul_assoc, mul_right_inj' hb', mul_comm]
 
 theorem splits_X_pow_sub_one_of_X_pow_sub_C {F : Type*} [Field F] {E : Type*} [Field E]
-    (i : F →+* E) (n : ℕ) {a : F} (ha : a ≠ 0) (h : (X ^ n - C a).Splits i) :
-    (X ^ n - 1 : F[X]).Splits i := by
+    (i : F →+* E) (n : ℕ) {a : F} (ha : a ≠ 0) (h : ((X ^ n - C a).map i).Splits) :
+    ((X ^ n - 1 : F[X]).map i).Splits := by
   have ha' : i a ≠ 0 := mt ((injective_iff_map_eq_zero i).mp i.injective a) ha
   by_cases hn : n = 0
-  · rw [hn, pow_zero, sub_self]
-    exact splits_zero i
+  · simp [hn]
   have hn' : 0 < n := pos_iff_ne_zero.mpr hn
   have hn'' : (X ^ n - C a).degree ≠ 0 :=
     ne_of_eq_of_ne (degree_X_pow_sub_C hn' a) (mt WithBot.coe_eq_coe.mp hn)

Mathlib/FieldTheory/AbelRuffini.lean

@@ -217,6 +217,6 @@ variable {F}
 Let `E / F` be a field extension. If a polynomial `p`
 splits in `E`, then it splits in the relative algebraic closure of `F` in `E` already.
 -/
-theorem Splits.algebraicClosure {p : F[X]} (h : p.Splits (algebraMap F E)) :
-    p.Splits (algebraMap F (algebraicClosure F E)) :=
+theorem Splits.algebraicClosure {p : F[X]} (h : (p.map (algebraMap F E)).Splits) :
+    (p.map (algebraMap F (algebraicClosure F E))).Splits :=
   splits_of_splits h fun _ hx ↦ (isAlgebraic_of_mem_rootSet hx).isIntegral

Mathlib/FieldTheory/AlgebraicClosure.lean

@@ -205,7 +205,7 @@ theorem nonempty_algHom_of_exist_lifts_finset [alg : Algebra.IsAlgebraic F E]
 /-- Given a lift `x` and an integral element `s : E` over `x.carrier` whose conjugates over
 `x.carrier` are all in `K`, we can extend the lift to a lift whose carrier contains `s`. -/
 theorem exists_lift_of_splits' (x : Lifts F E K) {s : E} (h1 : IsIntegral x.carrier s)
-    (h2 : (minpoly x.carrier s).Splits x.emb.toRingHom) : ∃ y, x ≤ y ∧ s ∈ y.carrier :=
+    (h2 : ((minpoly x.carrier s).map x.emb.toRingHom).Splits) : ∃ y, x ≤ y ∧ s ∈ y.carrier :=
   have I2 := (minpoly.degree_pos h1).ne'
   letI : Algebra x.carrier K := x.emb.toRingHom.toAlgebra
   let carrier := x.carrier⟮s⟯.restrictScalars F
@@ -222,7 +222,7 @@ theorem exists_lift_of_splits' (x : Lifts F E K) {s : E} (h1 : IsIntegral x.carr
 /-- Given an integral element `s : E` over `F` whose `F`-conjugates are all in `K`,
 any lift can be extended to one whose carrier contains `s`. -/
 theorem exists_lift_of_splits (x : Lifts F E K) {s : E} (h1 : IsIntegral F s)
-    (h2 : (minpoly F s).Splits (algebraMap F K)) : ∃ y, x ≤ y ∧ s ∈ y.carrier :=
+    (h2 : ((minpoly F s).map (algebraMap F K)).Splits) : ∃ y, x ≤ y ∧ s ∈ y.carrier :=
   exists_lift_of_splits' x h1.tower_top <| h1.minpoly_splits_tower_top' <| by
     rwa [← x.emb.comp_algebraMap] at h2
 
@@ -231,7 +231,7 @@ end Lifts
 section
 
 private theorem exists_algHom_adjoin_of_splits'' {L : IntermediateField F E}
-    (f : L →ₐ[F] K) (hK : ∀ s ∈ S, IsIntegral L s ∧ (minpoly L s).Splits f.toRingHom) :
+    (f : L →ₐ[F] K) (hK : ∀ s ∈ S, IsIntegral L s ∧ ((minpoly L s).map f.toRingHom).Splits) :
     ∃ φ : adjoin L S →ₐ[F] K, φ.restrictDomain L = f := by
   obtain ⟨φ, hfφ, hφ⟩ := zorn_le_nonempty_Ici₀ _
     (fun c _ hc _ _ ↦ Lifts.exists_upper_bound c hc) ⟨L, f⟩ le_rfl
@@ -246,7 +246,7 @@ private theorem exists_algHom_adjoin_of_splits'' {L : IntermediateField F E}
   · convert (hK s h).2; ext; apply hfφ.2
 
 variable {L : Type*} [Field L] [Algebra F L] [Algebra L E] [IsScalarTower F L E]
-  (f : L →ₐ[F] K) (hK : ∀ s ∈ S, IsIntegral L s ∧ (minpoly L s).Splits f.toRingHom)
+  (f : L →ₐ[F] K) (hK : ∀ s ∈ S, IsIntegral L s ∧ ((minpoly L s).map f.toRingHom).Splits)
 
 include hK in
 theorem exists_algHom_adjoin_of_splits' :
@@ -278,14 +278,15 @@ theorem exists_algHom_of_adjoin_splits' (hS : adjoin L S = ⊤) :
   have ⟨φ, hφ⟩ := exists_algHom_adjoin_of_splits' f hK
   ⟨φ.comp (((equivOfEq hS).trans topEquiv).symm.toAlgHom.restrictScalars F), hφ⟩
 
-theorem exists_algHom_of_splits' (hK : ∀ s : E, IsIntegral L s ∧ (minpoly L s).Splits f.toRingHom) :
+theorem exists_algHom_of_splits'
+    (hK : ∀ s : E, IsIntegral L s ∧ ((minpoly L s).map f.toRingHom).Splits) :
     ∃ φ : E →ₐ[F] K, φ.restrictDomain L = f :=
   exists_algHom_of_adjoin_splits' f (fun x _ ↦ hK x) (adjoin_univ L E)
 
 end
 
-variable (hK : ∀ s ∈ S, IsIntegral F s ∧ (minpoly F s).Splits (algebraMap F K))
-  (hK' : ∀ s : E, IsIntegral F s ∧ (minpoly F s).Splits (algebraMap F K))
+variable (hK : ∀ s ∈ S, IsIntegral F s ∧ ((minpoly F s).map (algebraMap F K)).Splits)
+  (hK' : ∀ s : E, IsIntegral F s ∧ ((minpoly F s).map (algebraMap F K)).Splits)
   {L : IntermediateField F E} (f : L →ₐ[F] K) (hL : L ≤ adjoin F S) {x : E} {y : K}
 
 section
@@ -360,7 +361,7 @@ polynomial over `F` of elements of `K` splits. Then, for `x ∈ K`, the images o
 of `x` over `F`. -/
 theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits {F K : Type*} (L : Type*)
     [Field F] [Field K] [Field L] [Algebra F L] [Algebra F K]
-    (hA : ∀ x : K, (minpoly F x).Splits (algebraMap F L))
+    (hA : ∀ x : K, ((minpoly F x).map (algebraMap F L)).Splits)
     [Algebra.IsAlgebraic F K] (x : K) :
     (Set.range fun (ψ : K →ₐ[F] L) => ψ x) = (minpoly F x).rootSet L := by
   ext a

Mathlib/FieldTheory/Extension.lean

@@ -735,7 +735,7 @@ theorem Subfield.roots_X_pow_char_sub_X_bot :
   exact FiniteField.roots_X_pow_card_sub_X _
 
 theorem Subfield.splits_bot :
-    Splits (RingHom.id (⊥ : Subfield F)) (X ^ p - X) := by
+    Splits (Polynomial.map (RingHom.id (⊥ : Subfield F)) (X ^ p - X)) := by
   let _ := Subfield.fintypeBot F p
   rw [splits_iff_card_roots, roots_X_pow_char_sub_X_bot, ← Finset.card_def, Finset.card_univ,
     FiniteField.X_pow_card_sub_X_natDegree_eq _ (Fact.out (p := p.Prime)).one_lt,

Mathlib/FieldTheory/Finite/Basic.lean

@@ -133,7 +133,7 @@ theorem card (h : n ≠ 0) : Nat.card (GaloisField p n) = p ^ n := by
   rw [Nat.card_eq_fintype_card, Module.card_fintype b, ← Module.finrank_eq_card_basis b,
     ZMod.card, finrank p h]
 
-theorem splits_zmod_X_pow_sub_X : Splits (RingHom.id (ZMod p)) (X ^ p - X) := by
+theorem splits_zmod_X_pow_sub_X : Splits (map (RingHom.id (ZMod p)) (X ^ p - X)) := by
   have hp : 1 < p := h_prime.out.one_lt
   have h1 : roots (X ^ p - X : (ZMod p)[X]) = Finset.univ.val := by
     convert FiniteField.roots_X_pow_card_sub_X (ZMod p)
@@ -154,7 +154,7 @@ section Fintype
 variable {K : Type*} [Field K] [Fintype K] [Algebra (ZMod p) K]
 
 theorem _root_.FiniteField.splits_X_pow_card_sub_X :
-    Splits (algebraMap (ZMod p) K) (X ^ Fintype.card K - X) :=
+    Splits (map (algebraMap (ZMod p) K) (X ^ Fintype.card K - X)) :=
   (FiniteField.isSplittingField_sub K (ZMod p)).splits
 
 theorem _root_.FiniteField.isSplittingField_of_card_eq (h : Fintype.card K = p ^ n) :
@@ -173,7 +173,7 @@ section Finite
 variable {K : Type*} [Field K] [Algebra (ZMod p) K]
 
 theorem _root_.FiniteField.splits_X_pow_nat_card_sub_X [Finite K] :
-    Splits (algebraMap (ZMod p) K) (X ^ Nat.card K - X) := by
+    Splits (map (algebraMap (ZMod p) K) (X ^ Nat.card K - X)) := by
   haveI : Fintype K := Fintype.ofFinite K
   rw [Nat.card_eq_fintype_card]
   exact (FiniteField.isSplittingField_sub K (ZMod p)).splits