chore(field_theory/splitting_field): refactor splitting_field (#19178)

We refactor the definition of `splitting_field`. The main motivation is to backport [!4#4891](leanprover-community/mathlib4#4891) since the is seems very problematic to port the current design.


Zulip discussion relevant to this PR: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234891.20.20FieldTheory.2ESplittingField

src/field_theory/abel_ruffini.lean

@@ -344,8 +344,8 @@ begin
       exact minpoly.aeval F γ,
     end (minpoly.monic (is_integral γ)),
   rw [P, key],
-  exact gal_is_solvable_of_splits ⟨normal.splits (splitting_field.normal _) _⟩
-    (gal_mul_is_solvable hα hβ),
+  refine gal_is_solvable_of_splits ⟨_⟩ (gal_mul_is_solvable hα hβ),
+  exact normal.splits (splitting_field.normal _) (f ⟨γ, hγ⟩),
 end
 
 /-- An auxiliary induction lemma, which is generalized by `solvable_by_rad.is_solvable`. -/

src/field_theory/finite/galois_field.lean

@@ -152,13 +152,15 @@ begin
   rw [splits_iff_card_roots, h1, ←finset.card_def, finset.card_univ, h2, zmod.card],
 end
 
+local attribute [-instance] splitting_field.algebra'
+
 /-- A Galois field with exponent 1 is equivalent to `zmod` -/
 def equiv_zmod_p : galois_field p 1 ≃ₐ[zmod p] (zmod p) :=
-have h : (X ^ p ^ 1 : (zmod p)[X]) = X ^ (fintype.card (zmod p)),
-  by rw [pow_one, zmod.card p],
-have inst : is_splitting_field (zmod p) (zmod p) (X ^ p ^ 1 - X),
-  by { rw h, apply_instance },
-by exactI (is_splitting_field.alg_equiv (zmod p) (X ^ (p ^ 1) - X : (zmod p)[X])).symm
+let h : (X ^ p ^ 1 : (zmod p)[X]) = X ^ (fintype.card (zmod p)) :=
+  by rw [pow_one, zmod.card p] in
+let inst : is_splitting_field (zmod p) (zmod p) (X ^ p ^ 1 - X) :=
+  by { rw h, apply_instance } in
+(@is_splitting_field.alg_equiv _ (zmod p) _ _ _ (X ^ (p ^ 1) - X : (zmod p)[X]) inst).symm
 
 variables {K : Type*} [field K] [fintype K] [algebra (zmod p) K]
 

src/field_theory/polynomial_galois_group.lean

@@ -139,8 +139,7 @@ begin
     have hy := subtype.mem y,
     simp only [root_set, finset.mem_coe, multiset.mem_to_finset, key, multiset.mem_map] at hy,
     rcases hy with ⟨x, hx1, hx2⟩,
-    classical,
-    exact ⟨⟨x, multiset.mem_to_finset.mpr hx1⟩, subtype.ext hx2⟩ }
+    exact ⟨⟨x, (@multiset.mem_to_finset _ (classical.dec_eq _) _ _).mpr hx1⟩, subtype.ext hx2⟩ }
 end
 
 /-- The bijection between `root_set p p.splitting_field` and `root_set p E`. -/
@@ -237,14 +236,16 @@ begin
   { haveI : fact (p.splits (algebra_map F (p * q).splitting_field)) :=
       ⟨splits_of_splits_of_dvd _ hpq (splitting_field.splits (p * q)) (dvd_mul_right p q)⟩,
     have key : x = algebra_map (p.splitting_field) (p * q).splitting_field
-      ((roots_equiv_roots p _).inv_fun ⟨x, multiset.mem_to_finset.mpr h⟩) :=
+      ((roots_equiv_roots p _).inv_fun ⟨x,
+        (@multiset.mem_to_finset _ (classical.dec_eq _) _ _).mpr h⟩) :=
       subtype.ext_iff.mp (equiv.apply_symm_apply (roots_equiv_roots p _) ⟨x, _⟩).symm,
     rw [key, ←alg_equiv.restrict_normal_commutes, ←alg_equiv.restrict_normal_commutes],
     exact congr_arg _ (alg_equiv.ext_iff.mp hfg.1 _) },
   { haveI : fact (q.splits (algebra_map F (p * q).splitting_field)) :=
       ⟨splits_of_splits_of_dvd _ hpq (splitting_field.splits (p * q)) (dvd_mul_left q p)⟩,
     have key : x = algebra_map (q.splitting_field) (p * q).splitting_field
-      ((roots_equiv_roots q _).inv_fun ⟨x, multiset.mem_to_finset.mpr h⟩) :=
+      ((roots_equiv_roots q _).inv_fun ⟨x,
+        (@multiset.mem_to_finset _ (classical.dec_eq _) _ _).mpr h⟩) :=
       subtype.ext_iff.mp (equiv.apply_symm_apply (roots_equiv_roots q _) ⟨x, _⟩).symm,
     rw [key, ←alg_equiv.restrict_normal_commutes, ←alg_equiv.restrict_normal_commutes],
     exact congr_arg _ (alg_equiv.ext_iff.mp hfg.2 _) },
@@ -257,12 +258,12 @@ lemma mul_splits_in_splitting_field_of_mul {p₁ q₁ p₂ q₂ : F[X]}
   (p₁ * p₂).splits (algebra_map F (q₁ * q₂).splitting_field) :=
 begin
   apply splits_mul,
-  { rw ← (splitting_field.lift q₁ (splits_of_splits_of_dvd _
-      (mul_ne_zero hq₁ hq₂) (splitting_field.splits _) (dvd_mul_right q₁ q₂))).comp_algebra_map,
-    exact splits_comp_of_splits _ _ h₁, },
-  { rw ← (splitting_field.lift q₂ (splits_of_splits_of_dvd _
-      (mul_ne_zero hq₁ hq₂) (splitting_field.splits _) (dvd_mul_left q₂ q₁))).comp_algebra_map,
-    exact splits_comp_of_splits _ _ h₂, },
+  { rw ← (splitting_field.lift q₁ (splits_of_splits_of_dvd (algebra_map F (q₁ * q₂).splitting_field)
+     (mul_ne_zero hq₁ hq₂) (splitting_field.splits _) (dvd_mul_right q₁ q₂))).comp_algebra_map,
+    exact splits_comp_of_splits _ _ h₁ },
+  { rw ← (splitting_field.lift q₂ (splits_of_splits_of_dvd (algebra_map F (q₁ * q₂).splitting_field)
+     (mul_ne_zero hq₁ hq₂) (splitting_field.splits _) (dvd_mul_left q₂ q₁))).comp_algebra_map,
+    exact splits_comp_of_splits _ _ h₂ },
 end
 
 /-- `p` splits in the splitting field of `p ∘ q`, for `q` non-constant. -/
@@ -304,7 +305,9 @@ end
 
 /-- `polynomial.gal.restrict` for the composition of polynomials. -/
 def restrict_comp (hq : q.nat_degree ≠ 0) : (p.comp q).gal →* p.gal :=
-@restrict F _ p _ _ _ ⟨splits_in_splitting_field_of_comp p q hq⟩
+let h : fact (splits (algebra_map F (p.comp q).splitting_field) p) :=
+    ⟨splits_in_splitting_field_of_comp p q hq⟩ in
+@restrict F _ p _ _ _ h
 
 lemma restrict_comp_surjective (hq : q.nat_degree ≠ 0) :
   function.surjective (restrict_comp p q hq) :=