feat(field_theory/polynomial_galois_group): Galois group is S_p (#7352)

Proves that a Galois group is isomorphic to S_p, under certain conditions.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/data/complex/basic.lean

@@ -192,6 +192,10 @@ lemma eq_conj_iff_real {z : ℂ} : conj z = z ↔ ∃ r : ℝ, z = r :=
 lemma eq_conj_iff_re {z : ℂ} : conj z = z ↔ (z.re : ℂ) = z :=
 eq_conj_iff_real.trans ⟨by rintro ⟨r, rfl⟩; simp, λ h, ⟨_, h.symm⟩⟩
 
+lemma eq_conj_iff_im {z : ℂ} : conj z = z ↔ z.im = 0 :=
+⟨λ h, add_self_eq_zero.mp (neg_eq_iff_add_eq_zero.mp (congr_arg im h)),
+  λ h, ext rfl (neg_eq_iff_add_eq_zero.mpr (add_self_eq_zero.mpr h))⟩
+
 instance : star_ring ℂ :=
 { star := λ z, conj z,
   star_involutive := λ z, by simp,

src/data/complex/module.lean

@@ -79,6 +79,14 @@ instance [comm_semiring R] [algebra R ℝ] : algebra R ℂ :=
   commutes' := λ r ⟨xr, xi⟩, by ext; simp [smul_re, smul_im, algebra.commutes],
   ..complex.of_real.comp (algebra_map R ℝ) }
 
+/-- Complex conjugation as an `ℝ`-algebra isomorphism  -/
+def conj_alg_equiv : ℂ ≃ₐ[ℝ] ℂ :=
+{ inv_fun := complex.conj,
+  left_inv := complex.conj_conj,
+  right_inv := complex.conj_conj,
+  commutes' := complex.conj_of_real,
+  .. complex.conj }
+
 section
 open_locale complex_order
 

src/data/fintype/basic.lean

@@ -1035,14 +1035,16 @@ by simp [fintype.subtype_card, finset.card_univ]
   (set.univ : set α).to_finset = finset.univ :=
 by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }
 
-@[simp] lemma set.to_finset_empty [fintype α] :
-  (∅ : set α).to_finset = ∅ :=
-by { ext, simp only [set.mem_empty_eq, set.mem_to_finset, not_mem_empty] }
-
 @[simp] lemma set.to_finset_eq_empty_iff {s : set α} [fintype s] :
   s.to_finset = ∅ ↔ s = ∅ :=
 by simp [ext_iff, set.ext_iff]
 
+instance : fintype (∅ : set α) := ⟨∅, subtype.property⟩
+
+@[simp] lemma set.to_finset_empty :
+  (∅ : set α).to_finset = ∅ :=
+set.to_finset_eq_empty_iff.mpr rfl
+
 theorem fintype.card_subtype_le [fintype α] (p : α → Prop) [decidable_pred p] :
   fintype.card {x // p x} ≤ fintype.card α :=
 fintype.card_le_of_embedding (function.embedding.subtype _)

src/data/polynomial/ring_division.lean

@@ -534,6 +534,14 @@ rfl
   (0 : polynomial R).root_set S = ∅ :=
 by rw [root_set_def, polynomial.map_zero, roots_zero, to_finset_zero, finset.coe_empty]
 
+instance root_set_fintype {R : Type*} [integral_domain R] (p : polynomial R) (S : Type*)
+  [integral_domain S] [algebra R S] : fintype (p.root_set S) :=
+finset_coe.fintype _
+
+lemma root_set_finite {R : Type*} [integral_domain R] (p : polynomial R) (S : Type*)
+  [integral_domain S] [algebra R S] : (p.root_set S).finite :=
+⟨polynomial.root_set_fintype p S⟩
+
 end roots
 
 theorem is_unit_iff {f : polynomial R} : is_unit f ↔ ∃ r : R, is_unit r ∧ C r = f :=

src/field_theory/polynomial_galois_group.lean

@@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Patrick Lutz
 -/
 
+import analysis.complex.polynomial
 import field_theory.galois
+import group_theory.perm.cycle_type
+import ring_theory.eisenstein_criterion
 
 /-!
 # Galois Groups of Polynomials
@@ -23,6 +26,8 @@ the automorphism group of the splitting field.
 - `restrict_smul`: `restrict p E` is compatible with `gal_action p E`.
 - `gal_action_hom_injective`: the action of `gal p` on the roots of `p` in `E` is faithful.
 - `restrict_prod_inj`: `gal (p * q)` embeds as a subgroup of `gal p × gal q`.
+- `gal_action_hom_bijective_of_prime_degree`: An irreducible polynomial of prime degree
+  with two non-real roots has full Galois group
 -/
 
 noncomputable theory
@@ -165,6 +170,10 @@ def gal_action_hom [fact (p.splits (algebra_map F E))] : p.gal →* equiv.perm (
   map_one' := by { ext1 x, exact mul_action.one_smul x },
   map_mul' := λ x y, by { ext1 z, exact mul_action.mul_smul x y z } }
 
+lemma gal_action_hom_restrict [fact (p.splits (algebra_map F E))]
+  (ϕ : E ≃ₐ[F] E) (x : root_set p E) : ↑(gal_action_hom p E (restrict p E ϕ) x) = ϕ x :=
+restrict_smul ϕ x
+
 lemma gal_action_hom_injective [fact (p.splits (algebra_map F E))] :
   function.injective (gal_action_hom p E) :=
 begin
@@ -324,6 +333,91 @@ begin
   rw [aeval_def, map_root_of_splits _ (splitting_field.splits p) hp],
 end
 
+lemma splits_ℚ_ℂ {p : polynomial ℚ} : fact (p.splits (algebra_map ℚ ℂ)) :=
+⟨is_alg_closed.splits_codomain p⟩
+
+local attribute [instance] splits_ℚ_ℂ
+
+/-- The number of complex roots equals the number of real roots plus
+  the number of roots not fixed by complex conjugation -/
+lemma gal_action_hom_bijective_of_prime_degree_aux {p : polynomial ℚ} :
+  (p.root_set ℂ).to_finset.card = (p.root_set ℝ).to_finset.card +
+  (gal_action_hom p ℂ (restrict p ℂ (complex.conj_alg_equiv.restrict_scalars ℚ))).support.card :=
+begin
+  by_cases hp : p = 0,
+  { simp_rw [hp, root_set_zero, set.to_finset_eq_empty_iff.mpr rfl, finset.card_empty, zero_add],
+    refine eq.symm (nat.le_zero_iff.mp ((finset.card_le_univ _).trans (le_of_eq _))),
+    simp_rw [hp, root_set_zero, fintype.card_eq_zero_iff],
+    exact λ h, (set.mem_empty_eq h.val).mp h.mem },
+  have inj : function.injective (is_scalar_tower.to_alg_hom ℚ ℝ ℂ) := (algebra_map ℝ ℂ).injective,
+  rw [←finset.card_image_of_injective _ subtype.coe_injective,
+      ←finset.card_image_of_injective _ inj],
+  let a : finset ℂ := _,
+  let b : finset ℂ := _,
+  let c : finset ℂ := _,
+  change a.card = b.card + c.card,
+  have ha : ∀ z : ℂ, z ∈ a ↔ aeval z p = 0 :=
+  λ z, by rw [set.mem_to_finset, mem_root_set hp],
+  have hb : ∀ z : ℂ, z ∈ b ↔ aeval z p = 0 ∧ z.im = 0,
+  { intro z,
+    simp_rw [finset.mem_image, exists_prop, set.mem_to_finset, mem_root_set hp],
+    split,
+    { rintros ⟨w, hw, rfl⟩,
+      exact ⟨by rw [aeval_alg_hom_apply, hw, alg_hom.map_zero], rfl⟩ },
+    { rintros ⟨hz1, hz2⟩,
+      have key : is_scalar_tower.to_alg_hom ℚ ℝ ℂ z.re = z := by { ext, refl, rw hz2, refl },
+      exact ⟨z.re, inj (by rwa [←aeval_alg_hom_apply, key, alg_hom.map_zero]), key⟩ } },
+  have hc0 : ∀ w : p.root_set ℂ, gal_action_hom p ℂ
+    (restrict p ℂ (complex.conj_alg_equiv.restrict_scalars ℚ)) w = w ↔ w.val.im = 0,
+  { intro w,
+    rw [subtype.ext_iff, gal_action_hom_restrict],
+    exact complex.eq_conj_iff_im },
+  have hc : ∀ z : ℂ, z ∈ c ↔ aeval z p = 0 ∧ z.im ≠ 0,
+  { intro z,
+    simp_rw [finset.mem_image, exists_prop],
+    split,
+    { rintros ⟨w, hw, rfl⟩,
+      exact ⟨(mem_root_set hp).mp w.2, mt (hc0 w).mpr (equiv.perm.mem_support.mp hw)⟩ },
+    { rintros ⟨hz1, hz2⟩,
+      exact ⟨⟨z, (mem_root_set hp).mpr hz1⟩,
+        equiv.perm.mem_support.mpr (mt (hc0 _).mp hz2), rfl⟩ } },
+  rw ← finset.card_disjoint_union,
+  { apply congr_arg finset.card,
+    simp_rw [finset.ext_iff, finset.mem_union, ha, hb, hc],
+    tauto },
+  { intro z,
+    rw [finset.inf_eq_inter, finset.mem_inter, hb, hc],
+    tauto },
+  { apply_instance },
+end
+
+/-- An irreducible polynomial of prime degree with two non-real roots has full Galois group -/
+lemma gal_action_hom_bijective_of_prime_degree
+  {p : polynomial ℚ} (p_irr : irreducible p) (p_deg : p.nat_degree.prime)
+  (p_roots : fintype.card (p.root_set ℂ) = fintype.card (p.root_set ℝ) + 2) :
+  function.bijective (gal_action_hom p ℂ) :=
+begin
+  have h1 : fintype.card (p.root_set ℂ) = p.nat_degree,
+  { simp_rw [root_set_def, fintype.card_coe],
+    rw [multiset.to_finset_card_of_nodup, ←nat_degree_eq_card_roots],
+    { exact is_alg_closed.splits_codomain p },
+    { exact nodup_roots ((separable_map (algebra_map ℚ ℂ)).mpr p_irr.separable) } },
+  have h2 : fintype.card p.gal = fintype.card (gal_action_hom p ℂ).range :=
+  fintype.card_congr (monoid_hom.of_injective (gal_action_hom_injective p ℂ)).to_equiv,
+  let conj := restrict p ℂ (complex.conj_alg_equiv.restrict_scalars ℚ),
+  refine ⟨gal_action_hom_injective p ℂ, λ x, (congr_arg (has_mem.mem x)
+    (show (gal_action_hom p ℂ).range = ⊤, from _)).mpr (subgroup.mem_top x)⟩,
+  apply equiv.perm.subgroup_eq_top_of_swap_mem,
+  { rwa h1 },
+  { rw [h1, ←h2],
+    exact prime_degree_dvd_card p_irr p_deg },
+  { exact ⟨conj, rfl⟩ },
+  { rw ← equiv.perm.card_support_eq_two,
+    apply nat.add_left_cancel,
+    rw [←p_roots, ←set.to_finset_card (root_set p ℝ), ←set.to_finset_card (root_set p ℂ)],
+    exact gal_action_hom_bijective_of_prime_degree_aux.symm },
+end
+
 end gal
 
 end polynomial

src/group_theory/subgroup.lean

@@ -1219,6 +1219,33 @@ def cod_restrict (f : G →* N) (S : subgroup N) (h : ∀ x, f x ∈ S) : G →*
   map_one' := subtype.eq f.map_one,
   map_mul' := λ x y, subtype.eq (f.map_mul x y) }
 
+/-- Computable alternative to `monoid_hom.of_injective`. -/
+def of_left_inverse {f : G →* N} {g : N →* G} (h : function.left_inverse g f) : G ≃* f.range :=
+{ to_fun := f.range_restrict,
+  inv_fun := g ∘ f.range.subtype,
+  left_inv := h,
+  right_inv := by
+  { rintros ⟨x, y, rfl⟩,
+    apply subtype.ext,
+    rw [coe_range_restrict, function.comp_apply, subgroup.coe_subtype, subtype.coe_mk, h] },
+  .. f.range_restrict }
+
+@[simp] lemma of_left_inverse_apply {f : G →* N} {g : N →* G}
+  (h : function.left_inverse g f) (x : G) :
+  ↑(of_left_inverse h x) = f x := rfl
+
+@[simp] lemma of_left_inverse_symm_apply {f : G →* N} {g : N →* G}
+  (h : function.left_inverse g f) (x : f.range) :
+  (of_left_inverse h).symm x = g x := rfl
+
+/-- The range of an injective group homomorphism is isomorphic to its domain. -/
+noncomputable def of_injective {f : G →* N} (hf : function.injective f) : G ≃* f.range :=
+(mul_equiv.of_bijective (f.cod_restrict f.range (λ x, ⟨x, rfl⟩))
+  ⟨λ x y h, hf (subtype.ext_iff.mp h), by { rintros ⟨x, y, rfl⟩, exact ⟨y, rfl⟩ }⟩)
+
+lemma of_injective_apply {f : G →* N} (hf : function.injective f) {x : G} :
+  ↑(of_injective hf x) = f x := rfl
+
 /-- The multiplicative kernel of a monoid homomorphism is the subgroup of elements `x : G` such that
 `f x = 1` -/
 @[to_additive "The additive kernel of an `add_monoid` homomorphism is the `add_subgroup` of elements