From a0ae2165d015aef83609c5d48f1e58320697df82 Mon Sep 17 00:00:00 2001 From: negiizhao Date: Thu, 15 Sep 2022 06:43:26 +0000 Subject: [PATCH] feat(field_theory/splitting_field): generalize `splits` for `comm_ring K` (#16405) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 2 +- src/field_theory/normal.lean | 4 +- src/field_theory/splitting_field.lean | 219 ++++++++++++++++---------- 3 files changed, 137 insertions(+), 88 deletions(-) diff --git a/src/field_theory/abel_ruffini.lean b/src/field_theory/abel_ruffini.lean index aa9ee0ae382e9..2ecab32a062ae 100644 --- a/src/field_theory/abel_ruffini.lean +++ b/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, diff --git a/src/field_theory/normal.lean b/src/field_theory/normal.lean index 5e104283fa2ec..db49716d7fbc2 100644 --- a/src/field_theory/normal.lean +++ b/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, diff --git a/src/field_theory/splitting_field.lean b/src/field_theory/splitting_field.lean index b9c950db65b53..f4522aa6a7dcc 100644 --- a/src/field_theory/splitting_field.lean +++ b/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,29 +45,32 @@ 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, @@ -74,18 +78,16 @@ or.inr $ λ g hg ⟨p, hp⟩, 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) @@ -93,31 +95,19 @@ lemma splits_of_nat_degree_eq_one {f : K[X]} (hf : nat_degree f = 1) : splits i 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] @@ -125,22 +115,14 @@ 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))