chore(field_theory/splitting_field): split file (#19154)

We split `field_theory.splitting_field` into `field_theory.splitting_field.is_splitting_field` and `field_theory.splitting_field.construction`. This is useful for the port, but also quite a lot of Galois theory should not depend on the existence of splitting fields.

Author: riccardobrasca

src/field_theory/adjoin.lean

@@ -6,7 +6,7 @@ Authors: Thomas Browning, Patrick Lutz
 
 import field_theory.intermediate_field
 import field_theory.separable
-import field_theory.splitting_field
+import field_theory.splitting_field.is_splitting_field
 import ring_theory.tensor_product
 
 /-!

src/field_theory/finite/galois_field.lean

@@ -8,7 +8,7 @@ import algebra.char_p.algebra
 import data.zmod.algebra
 import field_theory.finite.basic
 import field_theory.galois
-import field_theory.splitting_field
+import field_theory.splitting_field.is_splitting_field
 
 /-!
 # Galois fields

src/field_theory/is_alg_closed/algebraic_closure.lean

@@ -6,6 +6,7 @@ Authors: Kenny Lau
 import algebra.direct_limit
 import algebra.char_p.algebra
 import field_theory.is_alg_closed.basic
+import field_theory.splitting_field.construction
 
 /-!
 # Algebraic Closure

src/field_theory/normal.lean

@@ -135,9 +135,11 @@ local attribute [-instance] adjoin_root.has_smul
 lemma normal.of_is_splitting_field (p : F[X]) [hFEp : is_splitting_field F E p] : normal F E :=
 begin
   unfreezingI { rcases eq_or_ne p 0 with rfl | hp },
-  { haveI : is_splitting_field F F 0 := ⟨splits_zero _, subsingleton.elim _ _⟩,
-    exact (alg_equiv.transfer_normal ((is_splitting_field.alg_equiv F 0).trans
-      (is_splitting_field.alg_equiv E 0).symm)).mp (normal_self F) },
+  { have := hFEp.adjoin_roots,
+    simp only [polynomial.map_zero, roots_zero, multiset.to_finset_zero, finset.coe_empty,
+      algebra.adjoin_empty] at this,
+    exact normal.of_alg_equiv (alg_equiv.of_bijective (algebra.of_id F E)
+      (algebra.bijective_algebra_map_iff.2 this.symm)) },
   refine normal_iff.2 (λ x, _),
   have hFE : finite_dimensional F E := is_splitting_field.finite_dimensional E p,
   have Hx : is_integral F x := is_integral_of_noetherian (is_noetherian.iff_fg.2 hFE) x,
@@ -196,8 +198,6 @@ begin
   rw [set.image_singleton, ring_hom.algebra_map_to_algebra, adjoin_root.lift_root]
 end
 
-instance (p : F[X]) : normal F p.splitting_field := normal.of_is_splitting_field p
-
 end normal_tower
 
 namespace intermediate_field

src/field_theory/primitive_element.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Patrick Lutz
 -/
 
-import field_theory.adjoin
+import field_theory.splitting_field.construction
 import field_theory.is_alg_closed.basic
 import field_theory.separable
 import ring_theory.integral_domain

src/field_theory/splitting_field.lean renamed to src/field_theory/splitting_field/construction.lean

@@ -3,29 +3,19 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import algebra.char_p.algebra
-import field_theory.intermediate_field
-import ring_theory.adjoin.field
+import field_theory.normal
 
 /-!
 # Splitting fields
 
-This file introduces the notion of a splitting field of a polynomial and provides an embedding from
-a splitting field to any field that splits the polynomial. A polynomial `f : K[X]` splits
-over a field extension `L` of `K` if it is zero or all of its irreducible factors over `L` have
-degree `1`. A field extension of `K` of a polynomial `f : K[X]` is called a splitting field
-if it is the smallest field extension of `K` such that `f` splits.
+In this file we prove the existence and uniqueness of splitting fields.
 
 ## Main definitions
 
 * `polynomial.splitting_field f`: A fixed splitting field of the polynomial `f`.
-* `polynomial.is_splitting_field`: A predicate on a field to be a splitting field of a polynomial
-  `f`.
 
 ## Main statements
 
-* `polynomial.is_splitting_field.lift`: An embedding of a splitting field of the polynomial `f` into
-  another field such that `f` splits.
 * `polynomial.is_splitting_field.alg_equiv`: Every splitting field of a polynomial `f` is isomorphic
   to `splitting_field f` and thus, being a splitting field is unique up to isomorphism.
 
@@ -484,81 +474,16 @@ adjoin_roots f
 
 end splitting_field
 
-variables (K L) [algebra K L]
-/-- Typeclass characterising splitting fields. -/
-class is_splitting_field (f : K[X]) : Prop :=
-(splits [] : splits (algebra_map K L) f)
-(adjoin_roots [] : algebra.adjoin K (↑(f.map (algebra_map K L)).roots.to_finset : set L) = ⊤)
+end splitting_field
 
 namespace is_splitting_field
 
+variables (K L) [algebra K L]
+
 variables {K}
 instance splitting_field (f : K[X]) : is_splitting_field K (splitting_field f) f :=
 ⟨splitting_field.splits f, splitting_field.adjoin_roots f⟩
 
-section scalar_tower
-
-variables {K L F} [algebra F K] [algebra F L] [is_scalar_tower F K L]
-
-variables {K}
-instance map (f : F[X]) [is_splitting_field F L f] :
-  is_splitting_field K L (f.map $ algebra_map F K) :=
-⟨by { rw [splits_map_iff, ← is_scalar_tower.algebra_map_eq], exact splits L f },
- subalgebra.restrict_scalars_injective F $
-  by { rw [map_map, ← is_scalar_tower.algebra_map_eq, subalgebra.restrict_scalars_top,
-    eq_top_iff, ← adjoin_roots L f, algebra.adjoin_le_iff],
-  exact λ x hx, @algebra.subset_adjoin K _ _ _ _ _ _ hx }⟩
-
-variables {K} (L)
-theorem splits_iff (f : K[X]) [is_splitting_field K L f] :
-  polynomial.splits (ring_hom.id K) f ↔ (⊤ : subalgebra K L) = ⊥ :=
-⟨λ h, eq_bot_iff.2 $ adjoin_roots L f ▸ (roots_map (algebra_map K L) h).symm ▸
-  algebra.adjoin_le_iff.2 (λ y hy,
-    let ⟨x, hxs, hxy⟩ := finset.mem_image.1 (by rwa multiset.to_finset_map at hy) in
-    hxy ▸ set_like.mem_coe.2 $ subalgebra.algebra_map_mem _ _),
- λ h, @ring_equiv.to_ring_hom_refl K _ ▸
-  ring_equiv.self_trans_symm (ring_equiv.of_bijective _ $ algebra.bijective_algebra_map_iff.2 h) ▸
-  by { rw ring_equiv.to_ring_hom_trans, exact splits_comp_of_splits _ _ (splits L f) }⟩
-
-theorem mul (f g : F[X]) (hf : f ≠ 0) (hg : g ≠ 0) [is_splitting_field F K f]
-  [is_splitting_field K L (g.map $ algebra_map F K)] :
-  is_splitting_field F L (f * g) :=
-⟨(is_scalar_tower.algebra_map_eq F K L).symm ▸ splits_mul _
-  (splits_comp_of_splits _ _ (splits K f))
-  ((splits_map_iff _ _).1 (splits L $ g.map $ algebra_map F K)),
- by rw [polynomial.map_mul, roots_mul (mul_ne_zero (map_ne_zero hf : f.map (algebra_map F L) ≠ 0)
-        (map_ne_zero hg)), multiset.to_finset_add, finset.coe_union,
-      algebra.adjoin_union_eq_adjoin_adjoin,
-      is_scalar_tower.algebra_map_eq F K L, ← map_map,
-      roots_map (algebra_map K L) ((splits_id_iff_splits $ algebra_map F K).2 $ splits K f),
-      multiset.to_finset_map, finset.coe_image, algebra.adjoin_algebra_map, adjoin_roots,
-      algebra.map_top, is_scalar_tower.adjoin_range_to_alg_hom, ← map_map, adjoin_roots,
-      subalgebra.restrict_scalars_top]⟩
-
-end scalar_tower
-
-/-- Splitting field of `f` embeds into any field that splits `f`. -/
-def lift [algebra K F] (f : K[X]) [is_splitting_field K L f]
-  (hf : polynomial.splits (algebra_map K F) f) : L →ₐ[K] F :=
-if hf0 : f = 0 then (algebra.of_id K F).comp $
-  (algebra.bot_equiv K L : (⊥ : subalgebra K L) →ₐ[K] K).comp $
-  by { rw ← (splits_iff L f).1 (show f.splits (ring_hom.id K), from hf0.symm ▸ splits_zero _),
-  exact algebra.to_top } else
-alg_hom.comp (by { rw ← adjoin_roots L f, exact classical.choice (lift_of_splits _ $ λ y hy,
-    have aeval y f = 0, from (eval₂_eq_eval_map _).trans $
-      (mem_roots $ by exact map_ne_zero hf0).1 (multiset.mem_to_finset.mp hy),
-    ⟨is_algebraic_iff_is_integral.1 ⟨f, hf0, this⟩,
-      splits_of_splits_of_dvd _ hf0 hf $ minpoly.dvd _ _ this⟩) })
-  algebra.to_top
-
-theorem finite_dimensional (f : K[X]) [is_splitting_field K L f] : finite_dimensional K L :=
-⟨@algebra.top_to_submodule K L _ _ _ ▸ adjoin_roots L f ▸
-  fg_adjoin_of_finite (finset.finite_to_set _) (λ y hy,
-  if hf : f = 0
-  then by { rw [hf, polynomial.map_zero, roots_zero] at hy, cases hy }
-  else is_algebraic_iff_is_integral.1 ⟨f, hf, (eval₂_eq_eval_map _).trans $
-    (mem_roots $ by exact map_ne_zero hf).1 (multiset.mem_to_finset.mp hy)⟩)⟩
-
 instance (f : K[X]) : _root_.finite_dimensional K f.splitting_field :=
 finite_dimensional f.splitting_field f
 
@@ -582,39 +507,12 @@ begin
   exact ring_hom.injective (lift L f $ splits (splitting_field f) f : L →+* f.splitting_field)
 end
 
-lemma of_alg_equiv [algebra K F] (p : K[X]) (f : F ≃ₐ[K] L) [is_splitting_field K F p] :
-  is_splitting_field K L p :=
-begin
-  split,
-  { rw ← f.to_alg_hom.comp_algebra_map,
-    exact splits_comp_of_splits _ _ (splits F p) },
-  { rw [←(algebra.range_top_iff_surjective f.to_alg_hom).mpr f.surjective,
-        ←root_set, adjoin_root_set_eq_range (splits F p), root_set, adjoin_roots F p] },
-end
-
 end is_splitting_field
 
-end splitting_field
-
 end polynomial
 
-namespace intermediate_field
+section normal
 
-open polynomial
-
-variables [field K] [field L] [algebra K L] {p : K[X]}
-
-lemma splits_of_splits {F : intermediate_field K L} (h : p.splits (algebra_map K L))
-  (hF : ∀ x ∈ p.root_set L, x ∈ F) : p.splits (algebra_map K F) :=
-begin
-  simp_rw [root_set, finset.mem_coe, multiset.mem_to_finset] at hF,
-  rw splits_iff_exists_multiset,
-  refine ⟨multiset.pmap subtype.mk _ hF, map_injective _ (algebra_map F L).injective _⟩,
-  conv_lhs { rw [polynomial.map_map, ←is_scalar_tower.algebra_map_eq,
-    eq_prod_roots_of_splits h, ←multiset.pmap_eq_map _ _ _ hF] },
-  simp_rw [polynomial.map_mul, polynomial.map_multiset_prod,
-    multiset.map_pmap, polynomial.map_sub, map_C, map_X],
-  refl,
-end
+instance [field F] (p : F[X]) : normal F p.splitting_field := normal.of_is_splitting_field p
 
-end intermediate_field
+end normal

src/field_theory/splitting_field/is_splitting_field.lean

@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+import algebra.char_p.algebra
+import field_theory.intermediate_field
+import ring_theory.adjoin.field
+
+/-!
+# Splitting fields
+
+This file introduces the notion of a splitting field of a polynomial and provides an embedding from
+a splitting field to any field that splits the polynomial. A polynomial `f : K[X]` splits
+over a field extension `L` of `K` if it is zero or all of its irreducible factors over `L` have
+degree `1`. A field extension of `K` of a polynomial `f : K[X]` is called a splitting field
+if it is the smallest field extension of `K` such that `f` splits.
+
+## Main definitions
+
+* `polynomial.is_splitting_field`: A predicate on a field to be a splitting field of a polynomial
+  `f`.
+
+## Main statements
+
+* `polynomial.is_splitting_field.lift`: An embedding of a splitting field of the polynomial `f` into
+  another field such that `f` splits.
+
+-/
+
+noncomputable theory
+open_locale classical big_operators polynomial
+
+universes u v w
+
+variables {F : Type u} (K : Type v) (L : Type w)
+
+namespace polynomial
+
+variables [field K] [field L] [field F] [algebra K L]
+
+/-- Typeclass characterising splitting fields. -/
+class is_splitting_field (f : K[X]) : Prop :=
+(splits [] : splits (algebra_map K L) f)
+(adjoin_roots [] : algebra.adjoin K (↑(f.map (algebra_map K L)).roots.to_finset : set L) = ⊤)
+
+variables {K L F}
+
+namespace is_splitting_field
+
+section scalar_tower
+
+variables [algebra F K] [algebra F L] [is_scalar_tower F K L]
+
+instance map (f : F[X]) [is_splitting_field F L f] :
+  is_splitting_field K L (f.map $ algebra_map F K) :=
+⟨by { rw [splits_map_iff, ← is_scalar_tower.algebra_map_eq], exact splits L f },
+ subalgebra.restrict_scalars_injective F $
+  by { rw [map_map, ← is_scalar_tower.algebra_map_eq, subalgebra.restrict_scalars_top,
+    eq_top_iff, ← adjoin_roots L f, algebra.adjoin_le_iff],
+  exact λ x hx, @algebra.subset_adjoin K _ _ _ _ _ _ hx }⟩
+
+variables (L)
+theorem splits_iff (f : K[X]) [is_splitting_field K L f] :
+  polynomial.splits (ring_hom.id K) f ↔ (⊤ : subalgebra K L) = ⊥ :=
+⟨λ h, eq_bot_iff.2 $ adjoin_roots L f ▸ (roots_map (algebra_map K L) h).symm ▸
+  algebra.adjoin_le_iff.2 (λ y hy,
+    let ⟨x, hxs, hxy⟩ := finset.mem_image.1 (by rwa multiset.to_finset_map at hy) in
+    hxy ▸ set_like.mem_coe.2 $ subalgebra.algebra_map_mem _ _),
+ λ h, @ring_equiv.to_ring_hom_refl K _ ▸
+  ring_equiv.self_trans_symm (ring_equiv.of_bijective _ $ algebra.bijective_algebra_map_iff.2 h) ▸
+  by { rw ring_equiv.to_ring_hom_trans, exact splits_comp_of_splits _ _ (splits L f) }⟩
+
+theorem mul (f g : F[X]) (hf : f ≠ 0) (hg : g ≠ 0) [is_splitting_field F K f]
+  [is_splitting_field K L (g.map $ algebra_map F K)] :
+  is_splitting_field F L (f * g) :=
+⟨(is_scalar_tower.algebra_map_eq F K L).symm ▸ splits_mul _
+  (splits_comp_of_splits _ _ (splits K f))
+  ((splits_map_iff _ _).1 (splits L $ g.map $ algebra_map F K)),
+ by rw [polynomial.map_mul, roots_mul (mul_ne_zero (map_ne_zero hf : f.map (algebra_map F L) ≠ 0)
+        (map_ne_zero hg)), multiset.to_finset_add, finset.coe_union,
+      algebra.adjoin_union_eq_adjoin_adjoin,
+      is_scalar_tower.algebra_map_eq F K L, ← map_map,
+      roots_map (algebra_map K L) ((splits_id_iff_splits $ algebra_map F K).2 $ splits K f),
+      multiset.to_finset_map, finset.coe_image, algebra.adjoin_algebra_map, adjoin_roots,
+      algebra.map_top, is_scalar_tower.adjoin_range_to_alg_hom, ← map_map, adjoin_roots,
+      subalgebra.restrict_scalars_top]⟩
+
+end scalar_tower
+
+variable (L)
+
+/-- Splitting field of `f` embeds into any field that splits `f`. -/
+def lift [algebra K F] (f : K[X]) [is_splitting_field K L f]
+  (hf : polynomial.splits (algebra_map K F) f) : L →ₐ[K] F :=
+if hf0 : f = 0 then (algebra.of_id K F).comp $
+  (algebra.bot_equiv K L : (⊥ : subalgebra K L) →ₐ[K] K).comp $
+  by { rw ← (splits_iff L f).1 (show f.splits (ring_hom.id K), from hf0.symm ▸ splits_zero _),
+  exact algebra.to_top } else
+alg_hom.comp (by { rw ← adjoin_roots L f, exact classical.choice (lift_of_splits _ $ λ y hy,
+    have aeval y f = 0, from (eval₂_eq_eval_map _).trans $
+      (mem_roots $ by exact map_ne_zero hf0).1 (multiset.mem_to_finset.mp hy),
+    ⟨is_algebraic_iff_is_integral.1 ⟨f, hf0, this⟩,
+      splits_of_splits_of_dvd _ hf0 hf $ minpoly.dvd _ _ this⟩) })
+  algebra.to_top
+
+theorem finite_dimensional (f : K[X]) [is_splitting_field K L f] : finite_dimensional K L :=
+⟨@algebra.top_to_submodule K L _ _ _ ▸ adjoin_roots L f ▸
+  fg_adjoin_of_finite (finset.finite_to_set _) (λ y hy,
+  if hf : f = 0
+  then by { rw [hf, polynomial.map_zero, roots_zero] at hy, cases hy }
+  else is_algebraic_iff_is_integral.1 ⟨f, hf, (eval₂_eq_eval_map _).trans $
+    (mem_roots $ by exact map_ne_zero hf).1 (multiset.mem_to_finset.mp hy)⟩)⟩
+
+lemma of_alg_equiv [algebra K F] (p : K[X]) (f : F ≃ₐ[K] L) [is_splitting_field K F p] :
+  is_splitting_field K L p :=
+begin
+  split,
+  { rw ← f.to_alg_hom.comp_algebra_map,
+    exact splits_comp_of_splits _ _ (splits F p) },
+  { rw [←(algebra.range_top_iff_surjective f.to_alg_hom).mpr f.surjective,
+        ←root_set, adjoin_root_set_eq_range (splits F p), root_set, adjoin_roots F p] },
+end
+
+end is_splitting_field
+
+end polynomial
+
+namespace intermediate_field
+
+open polynomial
+
+variables {K L} [field K] [field L] [algebra K L] {p : K[X]}
+
+lemma splits_of_splits {F : intermediate_field K L} (h : p.splits (algebra_map K L))
+  (hF : ∀ x ∈ p.root_set L, x ∈ F) : p.splits (algebra_map K F) :=
+begin
+  simp_rw [root_set, finset.mem_coe, multiset.mem_to_finset] at hF,
+  rw splits_iff_exists_multiset,
+  refine ⟨multiset.pmap subtype.mk _ hF, map_injective _ (algebra_map F L).injective _⟩,
+  conv_lhs { rw [polynomial.map_map, ←is_scalar_tower.algebra_map_eq,
+    eq_prod_roots_of_splits h, ←multiset.pmap_eq_map _ _ _ hF] },
+  simp_rw [polynomial.map_mul, polynomial.map_multiset_prod,
+    multiset.map_pmap, polynomial.map_sub, map_C, map_X],
+  refl,
+end
+
+end intermediate_field

src/ring_theory/polynomial/gauss_lemma.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-import field_theory.splitting_field
+import field_theory.splitting_field.construction
 import ring_theory.int.basic
 import ring_theory.localization.integral
 import ring_theory.integrally_closed