feat(field_theory/splitting_field): generalize splits for `comm_rin…

…g K` (#16405)

The definition of `splits` has been slightly changed for this change. Hence 2 lemmas `splits_iff` and `splits.def` are added for the `field K` case.

I guess it may be helpful if we are able to talk about something like `splits i (p : ℤ[X])`?

src/field_theory/abel_ruffini.lean

@@ -133,7 +133,7 @@ begin
   have hn''' : (X ^ n - 1 : F[X]) ≠ 0 :=
     λ h, one_ne_zero ((leading_coeff_X_pow_sub_one hn').symm.trans (congr_arg leading_coeff h)),
   have mem_range : ∀ {c}, c ^ n = 1 → ∃ d, algebra_map F (X ^ n - C a).splitting_field d = c :=
-    λ c hc, ring_hom.mem_range.mp (minpoly.mem_range_of_degree_eq_one F c (or.resolve_left h hn'''
+    λ c hc, ring_hom.mem_range.mp (minpoly.mem_range_of_degree_eq_one F c (h.def.resolve_left hn'''
       (minpoly.irreducible ((splitting_field.normal (X ^ n - C a)).is_integral c)) (minpoly.dvd F c
       (by rwa [map_id, alg_hom.map_sub, sub_eq_zero, aeval_X_pow, aeval_one])))),
   apply is_solvable_of_comm,

src/field_theory/normal.lean

@@ -96,7 +96,7 @@ lemma alg_hom.normal_bijective [h : normal F E] (ϕ : E →ₐ[F] K) : function.
 ⟨ϕ.to_ring_hom.injective, λ x, by
 { letI : algebra E K := ϕ.to_ring_hom.to_algebra,
   obtain ⟨h1, h2⟩ := h.out (algebra_map K E x),
-  cases minpoly.mem_range_of_degree_eq_one E x (or.resolve_left h2 (minpoly.ne_zero h1)
+  cases minpoly.mem_range_of_degree_eq_one E x (h2.def.resolve_left (minpoly.ne_zero h1)
     (minpoly.irreducible (is_integral_of_is_scalar_tower x
       ((is_integral_algebra_map_iff (algebra_map K E).injective).mp h1)))
     (minpoly.dvd E x ((algebra_map K E).injective (by
@@ -246,7 +246,7 @@ def alg_hom.restrict_normal_aux [h : normal F E] :
     rintros x ⟨y, ⟨z, hy⟩, hx⟩,
     rw [←hx, ←hy],
     apply minpoly.mem_range_of_degree_eq_one E,
-    exact or.resolve_left (h.splits z) (minpoly.ne_zero (h.is_integral z))
+    exact or.resolve_left (h.splits z).def (minpoly.ne_zero (h.is_integral z))
       (minpoly.irreducible $ is_integral_of_is_scalar_tower _ $
         is_integral_alg_hom ϕ $ is_integral_alg_hom _ $ h.is_integral z)
       (minpoly.dvd E _ $ by rw [aeval_map, aeval_alg_hom, aeval_alg_hom, alg_hom.comp_apply,

src/field_theory/splitting_field.lean

@@ -17,8 +17,9 @@ if it is the smallest field extension of `K` such that `f` splits.
 
 ## Main definitions
 
-* `polynomial.splits i f`: A predicate on a field homomorphism `i : K → L` and a polynomial `f`
-  saying that `f` is zero or all of its irreducible factors over `L` have degree `1`.
+* `polynomial.splits i f`: A predicate on a homomorphism `i : K →+* L` from a commutative ring to a
+  field and a polynomial `f` saying that `f.map i` is zero or all of its irreducible factors over
+  `L` have degree `1`.
 * `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`.
@@ -44,103 +45,84 @@ variables {F : Type u} {K : Type v} {L : Type w}
 
 namespace polynomial
 
-variables [field K] [field L] [field F]
 open polynomial
 
 section splits
 
+section comm_ring
+variables [comm_ring K] [field L] [field F]
 variables (i : K →+* L)
 
 /-- A polynomial `splits` iff it is zero or all of its irreducible factors have `degree` 1. -/
 def splits (f : K[X]) : Prop :=
-f = 0 ∨ ∀ {g : L[X]}, irreducible g → g ∣ f.map i → degree g = 1
+f.map i = 0 ∨ ∀ {g : L[X]}, irreducible g → g ∣ f.map i → degree g = 1
 
-@[simp] lemma splits_zero : splits i (0 : K[X]) := or.inl rfl
+@[simp] lemma splits_zero : splits i (0 : K[X]) := or.inl (polynomial.map_zero i)
 
-@[simp] lemma splits_C (a : K) : splits i (C a) :=
-if ha : a = 0 then ha.symm ▸ (@C_0 K _).symm ▸ splits_zero i
-else
-have hia : i a ≠ 0, from mt ((injective_iff_map_eq_zero i).1 i.injective _) ha,
-or.inr $ λ g hg ⟨p, hp⟩, absurd hg.1 (not_not.2 (is_unit_iff_degree_eq_zero.2 $
-  by have := congr_arg degree hp;
-    simp [degree_C hia, @eq_comm (with_bot ℕ) 0,
-      nat.with_bot.add_eq_zero_iff] at this; clear _fun_match; tauto))
+lemma splits_of_map_eq_C {f : K[X]} {a : L} (h : f.map i = C a) : splits i f :=
+if ha : a = 0 then or.inl (h.trans (ha.symm ▸ C_0))
+else or.inr $ λ g hg ⟨p, hp⟩, absurd hg.1 $ not_not.2 $ is_unit_iff_degree_eq_zero.2 $
+begin
+  have := congr_arg degree hp,
+  rw [h, degree_C ha, degree_mul, @eq_comm (with_bot ℕ) 0, nat.with_bot.add_eq_zero_iff] at this,
+  exact this.1,
+end
 
-lemma splits_of_degree_eq_one {f : K[X]} (hf : degree f = 1) : splits i f :=
+@[simp] lemma splits_C (a : K) : splits i (C a) := splits_of_map_eq_C i (map_C i)
+
+lemma splits_of_map_degree_eq_one {f : K[X]} (hf : degree (f.map i) = 1) : splits i f :=
 or.inr $ λ g hg ⟨p, hp⟩,
   by have := congr_arg degree hp;
   simp [nat.with_bot.add_eq_one_iff, hf, @eq_comm (with_bot ℕ) 1,
     mt is_unit_iff_degree_eq_zero.2 hg.1] at this;
   clear _fun_match; tauto
 
 lemma splits_of_degree_le_one {f : K[X]} (hf : degree f ≤ 1) : splits i f :=
-begin
-  cases h : degree f with n,
-  { rw [degree_eq_bot.1 h]; exact splits_zero i },
-  { cases n with n,
-    { rw [eq_C_of_degree_le_zero (trans_rel_right (≤) h le_rfl)];
-      exact splits_C _ _ },
-    { have hn : n = 0,
-      { rw h at hf,
-        cases n, { refl }, { exact absurd hf dec_trivial } },
-      exact splits_of_degree_eq_one _ (by rw [h, hn]; refl) } }
+if hif : degree (f.map i) ≤ 0 then splits_of_map_eq_C i (degree_le_zero_iff.mp hif)
+else begin
+  push_neg at hif,
+  rw [← order.succ_le_iff, ← with_bot.coe_zero, with_bot.succ_coe, nat.succ_eq_succ] at hif,
+  exact splits_of_map_degree_eq_one i (le_antisymm ((degree_map_le i _).trans hf) hif),
 end
 
+lemma splits_of_degree_eq_one {f : K[X]} (hf : degree f = 1) : splits i f :=
+splits_of_degree_le_one i hf.le
+
 lemma splits_of_nat_degree_le_one {f : K[X]} (hf : nat_degree f ≤ 1) : splits i f :=
 splits_of_degree_le_one i (degree_le_of_nat_degree_le hf)
 
 lemma splits_of_nat_degree_eq_one {f : K[X]} (hf : nat_degree f = 1) : splits i f :=
 splits_of_nat_degree_le_one i (le_of_eq hf)
 
 lemma splits_mul {f g : K[X]} (hf : splits i f) (hg : splits i g) : splits i (f * g) :=
-if h : f * g = 0 then by simp [h]
+if h : (f * g).map i = 0 then or.inl h
 else or.inr $ λ p hp hpf, ((principal_ideal_ring.irreducible_iff_prime.1 hp).2.2 _ _
     (show p ∣ map i f * map i g, by convert hpf; rw polynomial.map_mul)).elim
   (hf.resolve_left (λ hf, by simpa [hf] using h) hp)
   (hg.resolve_left (λ hg, by simpa [hg] using h) hp)
 
-lemma splits_of_splits_mul {f g : K[X]} (hfg : f * g ≠ 0) (h : splits i (f * g)) :
+lemma splits_of_splits_mul' {f g : K[X]} (hfg : (f * g).map i ≠ 0) (h : splits i (f * g)) :
   splits i f ∧ splits i g :=
 ⟨or.inr $ λ g hgi hg, or.resolve_left h hfg hgi
    (by rw polynomial.map_mul; exact hg.trans (dvd_mul_right _ _)),
  or.inr $ λ g hgi hg, or.resolve_left h hfg hgi
    (by rw polynomial.map_mul; exact hg.trans (dvd_mul_left _ _))⟩
 
-lemma splits_of_splits_of_dvd {f g : K[X]} (hf0 : f ≠ 0) (hf : splits i f) (hgf : g ∣ f) :
-  splits i g :=
-by { obtain ⟨f, rfl⟩ := hgf, exact (splits_of_splits_mul i hf0 hf).1 }
-
-lemma splits_of_splits_gcd_left {f g : K[X]} (hf0 : f ≠ 0) (hf : splits i f) :
-  splits i (euclidean_domain.gcd f g) :=
-polynomial.splits_of_splits_of_dvd i hf0 hf (euclidean_domain.gcd_dvd_left f g)
-
-lemma splits_of_splits_gcd_right {f g : K[X]} (hg0 : g ≠ 0) (hg : splits i g) :
-  splits i (euclidean_domain.gcd f g) :=
-polynomial.splits_of_splits_of_dvd i hg0 hg (euclidean_domain.gcd_dvd_right f g)
-
 lemma splits_map_iff (j : L →+* F) {f : K[X]} :
   splits j (f.map i) ↔ splits (j.comp i) f :=
 by simp [splits, polynomial.map_map]
 
 theorem splits_one : splits i 1 :=
 splits_C i 1
 
-theorem splits_of_is_unit {u : K[X]} (hu : is_unit u) : u.splits i :=
-splits_of_splits_of_dvd i one_ne_zero (splits_one _) $ is_unit_iff_dvd_one.1 hu
+theorem splits_of_is_unit [is_domain K] {u : K[X]} (hu : is_unit u) : u.splits i :=
+(is_unit_iff.mp hu).some_spec.2 ▸ splits_C _ _
 
 theorem splits_X_sub_C {x : K} : (X - C x).splits i :=
-splits_of_degree_eq_one _ $ degree_X_sub_C x
+splits_of_degree_le_one _ $ degree_X_sub_C_le _
 
 theorem splits_X : X.splits i :=
-splits_of_degree_eq_one _ $ degree_X
-
-theorem splits_id_iff_splits {f : K[X]} :
-  (f.map i).splits (ring_hom.id L) ↔ f.splits i :=
-by rw [splits_map_iff, ring_hom.id_comp]
-
-theorem splits_mul_iff {f g : K[X]} (hf : f ≠ 0) (hg : g ≠ 0) :
-  (f * g).splits i ↔ f.splits i ∧ g.splits i :=
-⟨splits_of_splits_mul i (mul_ne_zero hf hg), λ ⟨hfs, hgs⟩, splits_mul i hfs hgs⟩
+splits_of_degree_le_one _ degree_X_le
 
 theorem splits_prod {ι : Type u} {s : ι → K[X]} {t : finset ι} :
   (∀ j ∈ t, (s j).splits i) → (∏ x in t, s x).splits i :=
@@ -158,6 +140,91 @@ end
 
 lemma splits_X_pow (n : ℕ) : (X ^ n).splits i := splits_pow i (splits_X i) n
 
+theorem splits_id_iff_splits {f : K[X]} :
+  (f.map i).splits (ring_hom.id L) ↔ f.splits i :=
+by rw [splits_map_iff, ring_hom.id_comp]
+
+lemma exists_root_of_splits' {f : K[X]} (hs : splits i f) (hf0 : degree (f.map i) ≠ 0) :
+  ∃ x, eval₂ i x f = 0 :=
+if hf0' : f.map i = 0 then by simp [eval₂_eq_eval_map, hf0']
+else
+  let ⟨g, hg⟩ := wf_dvd_monoid.exists_irreducible_factor
+    (show ¬ is_unit (f.map i), from mt is_unit_iff_degree_eq_zero.1 hf0) hf0' in
+  let ⟨x, hx⟩ := exists_root_of_degree_eq_one (hs.resolve_left hf0' hg.1 hg.2) in
+  let ⟨i, hi⟩ := hg.2 in
+  ⟨x, by rw [← eval_map, hi, eval_mul, show _ = _, from hx, zero_mul]⟩
+
+lemma roots_ne_zero_of_splits' {f : K[X]} (hs : splits i f) (hf0 : nat_degree (f.map i) ≠ 0) :
+  (f.map i).roots ≠ 0 :=
+let ⟨x, hx⟩ := exists_root_of_splits' i hs (λ h, hf0 $ nat_degree_eq_of_degree_eq_some h) in
+λ h, by { rw ← eval_map at hx,
+  cases h.subst ((mem_roots _).2 hx), exact ne_zero_of_nat_degree_gt (nat.pos_of_ne_zero hf0) }
+
+/-- Pick a root of a polynomial that splits. See `root_of_splits` for polynomials over a field
+which has simpler assumptions. -/
+def root_of_splits' {f : K[X]} (hf : f.splits i) (hfd : (f.map i).degree ≠ 0) : L :=
+classical.some $ exists_root_of_splits' i hf hfd
+
+theorem map_root_of_splits' {f : K[X]} (hf : f.splits i) (hfd) :
+  f.eval₂ i (root_of_splits' i hf hfd) = 0 :=
+classical.some_spec $ exists_root_of_splits' i hf hfd
+
+lemma nat_degree_eq_card_roots' {p : K[X]} {i : K →+* L}
+  (hsplit : splits i p) : (p.map i).nat_degree = (p.map i).roots.card :=
+begin
+  by_cases hp : p.map i = 0,
+  { rw [hp, nat_degree_zero, roots_zero, multiset.card_zero] },
+  obtain ⟨q, he, hd, hr⟩ := exists_prod_multiset_X_sub_C_mul (p.map i),
+  rw [← splits_id_iff_splits, ← he] at hsplit,
+  rw ← he at hp,
+  have hq : q ≠ 0 := λ h, hp (by rw [h, mul_zero]),
+  rw [← hd, add_right_eq_self],
+  by_contra,
+  have h' : (map (ring_hom.id L) q).nat_degree ≠ 0, { simp [h], },
+  have := roots_ne_zero_of_splits' (ring_hom.id L) (splits_of_splits_mul' _ _ hsplit).2 h',
+  { rw map_id at this, exact this hr },
+  { rw [map_id], exact mul_ne_zero monic_prod_multiset_X_sub_C.ne_zero hq },
+end
+
+lemma degree_eq_card_roots' {p : K[X]} {i : K →+* L} (p_ne_zero : p.map i ≠ 0)
+  (hsplit : splits i p) : (p.map i).degree = (p.map i).roots.card :=
+by rw [degree_eq_nat_degree p_ne_zero, nat_degree_eq_card_roots' hsplit]
+
+end comm_ring
+
+variables [field K] [field L] [field F]
+variables (i : K →+* L)
+
+/-- This lemma is for polynomials over a field. -/
+lemma splits_iff (f : K[X]) :
+  splits i f ↔ f = 0 ∨ ∀ {g : L[X]}, irreducible g → g ∣ f.map i → degree g = 1 :=
+by rw [splits, map_eq_zero]
+
+/-- This lemma is for polynomials over a field. -/
+lemma splits.def {i : K →+* L} {f : K[X]} (h : splits i f) :
+  f = 0 ∨ ∀ {g : L[X]}, irreducible g → g ∣ f.map i → degree g = 1 :=
+(splits_iff i f).mp h
+
+lemma splits_of_splits_mul {f g : K[X]} (hfg : f * g ≠ 0) (h : splits i (f * g)) :
+  splits i f ∧ splits i g :=
+splits_of_splits_mul' i (map_ne_zero hfg) h
+
+lemma splits_of_splits_of_dvd {f g : K[X]} (hf0 : f ≠ 0) (hf : splits i f) (hgf : g ∣ f) :
+  splits i g :=
+by { obtain ⟨f, rfl⟩ := hgf, exact (splits_of_splits_mul i hf0 hf).1 }
+
+lemma splits_of_splits_gcd_left {f g : K[X]} (hf0 : f ≠ 0) (hf : splits i f) :
+  splits i (euclidean_domain.gcd f g) :=
+polynomial.splits_of_splits_of_dvd i hf0 hf (euclidean_domain.gcd_dvd_left f g)
+
+lemma splits_of_splits_gcd_right {f g : K[X]} (hg0 : g ≠ 0) (hg : splits i g) :
+  splits i (euclidean_domain.gcd f g) :=
+polynomial.splits_of_splits_of_dvd i hg0 hg (euclidean_domain.gcd_dvd_right f g)
+
+theorem splits_mul_iff {f g : K[X]} (hf : f ≠ 0) (hg : g ≠ 0) :
+  (f * g).splits i ↔ f.splits i ∧ g.splits i :=
+⟨splits_of_splits_mul i (mul_ne_zero hf hg), λ ⟨hfs, hgs⟩, splits_mul i hfs hgs⟩
+
 theorem splits_prod_iff {ι : Type u} {s : ι → K[X]} {t : finset ι} :
   (∀ j ∈ t, s j ≠ 0) → ((∏ x in t, s x).splits i ↔ ∀ j ∈ t, (s j).splits i) :=
 begin
@@ -166,57 +233,39 @@ begin
   rw [finset.prod_insert hat, splits_mul_iff i ht.1 (finset.prod_ne_zero_iff.2 ht.2), ih ht.2]
 end
 
-lemma degree_eq_one_of_irreducible_of_splits {p : L[X]}
-  (hp : irreducible p) (hp_splits : splits (ring_hom.id L) p) :
+lemma degree_eq_one_of_irreducible_of_splits {p : K[X]}
+  (hp : irreducible p) (hp_splits : splits (ring_hom.id K) p) :
   p.degree = 1 :=
 begin
-  by_cases h_nz : p = 0,
-  { exfalso, simp * at *, },
   rcases hp_splits,
-  { contradiction },
+  { exfalso, simp * at *, },
   { apply hp_splits hp, simp }
 end
 
 lemma exists_root_of_splits {f : K[X]} (hs : splits i f) (hf0 : degree f ≠ 0) :
   ∃ x, eval₂ i x f = 0 :=
-if hf0 : f = 0 then by simp [hf0]
-else
-  let ⟨g, hg⟩ := wf_dvd_monoid.exists_irreducible_factor
-    (show ¬ is_unit (f.map i), from mt is_unit_iff_degree_eq_zero.1 (by rwa degree_map))
-    (map_ne_zero hf0) in
-  let ⟨x, hx⟩ := exists_root_of_degree_eq_one (hs.resolve_left hf0 hg.1 hg.2) in
-  let ⟨i, hi⟩ := hg.2 in
-  ⟨x, by rw [← eval_map, hi, eval_mul, show _ = _, from hx, zero_mul]⟩
+exists_root_of_splits' i hs ((f.degree_map i).symm ▸ hf0)
 
 lemma roots_ne_zero_of_splits {f : K[X]} (hs : splits i f) (hf0 : nat_degree f ≠ 0) :
   (f.map i).roots ≠ 0 :=
-let ⟨x, hx⟩ := exists_root_of_splits i hs (λ h, hf0 $ nat_degree_eq_of_degree_eq_some h) in
-λ h, by { rw ← eval_map at hx,
-  cases h.subst ((mem_roots _).2 hx), exact map_ne_zero (λ h, (h.subst hf0) rfl) }
+roots_ne_zero_of_splits' i hs (ne_of_eq_of_ne (nat_degree_map i) hf0)
 
-/-- Pick a root of a polynomial that splits. -/
+/-- Pick a root of a polynomial that splits. This version is for polynomials over a field and has
+simpler assumptions. -/
 def root_of_splits {f : K[X]} (hf : f.splits i) (hfd : f.degree ≠ 0) : L :=
-classical.some $ exists_root_of_splits i hf hfd
+root_of_splits' i hf ((f.degree_map i).symm ▸ hfd)
+
+/-- `root_of_splits'` is definitionally equal to `root_of_splits`. -/
+lemma root_of_splits'_eq_root_of_splits {f : K[X]} (hf : f.splits i) (hfd) :
+  root_of_splits' i hf hfd = root_of_splits i hf (f.degree_map i ▸ hfd) := rfl
 
 theorem map_root_of_splits {f : K[X]} (hf : f.splits i) (hfd) :
   f.eval₂ i (root_of_splits i hf hfd) = 0 :=
-classical.some_spec $ exists_root_of_splits i hf hfd
+map_root_of_splits' i hf (ne_of_eq_of_ne (degree_map f i) hfd)
 
 lemma nat_degree_eq_card_roots {p : K[X]} {i : K →+* L}
   (hsplit : splits i p) : p.nat_degree = (p.map i).roots.card :=
-begin
-  by_cases hp : p = 0,
-  { rw [hp, nat_degree_zero, polynomial.map_zero, roots_zero, multiset.card_zero] },
-  obtain ⟨q, he, hd, hr⟩ := exists_prod_multiset_X_sub_C_mul (p.map i),
-  rw [← splits_id_iff_splits, ← he] at hsplit,
-  have hpm : p.map i ≠ 0 := map_ne_zero hp, rw ← he at hpm,
-  have hq : q ≠ 0 := λ h, hpm (by rw [h, mul_zero]),
-  rw [← nat_degree_map i, ← hd, add_right_eq_self],
-  by_contra,
-  have := roots_ne_zero_of_splits (ring_hom.id L) (splits_of_splits_mul _ _ hsplit).2 h,
-  { rw map_id at this, exact this hr },
-  { exact mul_ne_zero monic_prod_multiset_X_sub_C.ne_zero hq },
-end
+(nat_degree_map i).symm.trans $ nat_degree_eq_card_roots' hsplit
 
 lemma degree_eq_card_roots {p : K[X]} {i : K →+* L} (p_ne_zero : p ≠ 0)
   (hsplit : splits i p) : p.degree = (p.map i).roots.card :=
@@ -282,7 +331,7 @@ open unique_factorization_monoid associates
 lemma splits_of_exists_multiset {f : K[X]} {s : multiset L}
   (hs : f.map i = C (i f.leading_coeff) * (s.map (λ a : L, X - C a)).prod) :
   splits i f :=
-if hf0 : f = 0 then or.inl hf0
+if hf0 : f = 0 then hf0.symm ▸ splits_zero i
 else or.inr $ λ p hp hdp, begin
   rw irreducible_iff_prime at hp,
   rw [hs, ← multiset.prod_to_list] at hdp,
@@ -295,13 +344,13 @@ else or.inr $ λ p hp hdp, begin
     exact degree_X_sub_C a },
 end
 
-lemma splits_of_splits_id {f : K[X]} : splits (ring_hom.id _) f → splits i f :=
+lemma splits_of_splits_id {f : K[X]} : splits (ring_hom.id K) f → splits i f :=
 unique_factorization_monoid.induction_on_prime f (λ _, splits_zero _)
   (λ _ hu _, splits_of_degree_le_one _
     ((is_unit_iff_degree_eq_zero.1 hu).symm ▸ dec_trivial))
   (λ a p ha0 hp ih hfi, splits_mul _
     (splits_of_degree_eq_one _
-      ((splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).1.resolve_left
+      ((splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).1.def.resolve_left
         hp.1 hp.irreducible (by rw map_id)))
     (ih (splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).2))