docs(field_theory/polynomial_galois_group): improve existing docs (#7586

)




Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>

src/field_theory/polynomial_galois_group.lean

@@ -12,22 +12,32 @@ import ring_theory.eisenstein_criterion
 /-!
 # Galois Groups of Polynomials
 
-In this file we introduce the Galois group of a polynomial, defined as
-the automorphism group of the splitting field.
+In this file, we introduce the Galois group of a polynomial `p` over a field `F`,
+defined as the automorphism group of its splitting field. We also provide
+some results about some extension `E` above `p.splitting_field`, and some specific
+results about the Galois groups of ℚ-polynomials with specific numbers of non-real roots.
 
 ## Main definitions
 
-- `gal p`: the Galois group of a polynomial p.
-- `restrict p E`: the restriction homomorphism `(E ≃ₐ[F] E) → gal p`.
-- `gal_action p E`: the action of `gal p` on the roots of `p` in `E`.
+- `polynomial.gal p`: the Galois group of a polynomial p.
+- `polynomial.gal.restrict p E`: the restriction homomorphism `(E ≃ₐ[F] E) → gal p`.
+- `polynomial.gal.gal_action p E`: the action of `gal p` on the roots of `p` in `E`.
 
 ## Main results
 
-- `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
+- `polynomial.gal.restrict_smul`: `restrict p E` is compatible with `gal_action p E`.
+- `polynomial.gal.gal_action_hom_injective`: `gal p` acting on the roots of `p` in `E` is faithful.
+- `polynomial.gal.restrict_prod_injective`: `gal (p * q)` embeds as a subgroup of `gal p × gal q`.
+- `polynomial.gal.card_of_separable`: For a separable polynomial, its Galois group has cardinality
+equal to the dimension of its splitting field over `F`.
+- `polynomial.gal.gal_action_hom_bijective_of_prime_degree`:
+An irreducible polynomial of prime degree with two non-real roots has full Galois group.
+
+## Other results
+- `polynomial.gal.card_complex_roots_eq_card_real_add_card_not_gal_inv`: The number of complex roots
+equals the number of real roots plus the number of roots not fixed by complex conjugation
+(i.e. with some imaginary component).
+
 -/
 
 noncomputable theory
@@ -39,7 +49,7 @@ namespace polynomial
 
 variables {F : Type*} [field F] (p q : polynomial F) (E : Type*) [field E] [algebra F E]
 
-/-- The Galois group of a polynomial -/
+/-- The Galois group of a polynomial. -/
 @[derive [has_coe_to_fun, group, fintype]]
 def gal := p.splitting_field ≃ₐ[F] p.splitting_field
 
@@ -52,19 +62,16 @@ begin
   rwa [eq_top_iff, ←splitting_field.adjoin_roots, algebra.adjoin_le_iff],
 end
 
-instance [h : fact (p.splits (ring_hom.id F))] : unique p.gal :=
-{ default := 1,
-  uniq := λ f, alg_equiv.ext (λ x, by { obtain ⟨y, rfl⟩ := algebra.mem_bot.mp
-    ((set_like.ext_iff.mp ((is_splitting_field.splits_iff _ p).mp h.1) x).mp algebra.mem_top),
-    rw [alg_equiv.commutes, alg_equiv.commutes] }) }
-
 /-- If `p` splits in `F` then the `p.gal` is trivial. -/
 def unique_gal_of_splits (h : p.splits (ring_hom.id F)) : unique p.gal :=
 { default := 1,
   uniq := λ f, alg_equiv.ext (λ x, by { obtain ⟨y, rfl⟩ := algebra.mem_bot.mp
     ((set_like.ext_iff.mp ((is_splitting_field.splits_iff _ p).mp h) x).mp algebra.mem_top),
     rw [alg_equiv.commutes, alg_equiv.commutes] }) }
 
+instance [h : fact (p.splits (ring_hom.id F))] : unique p.gal :=
+unique_gal_of_splits _ (h.1)
+
 instance unique_gal_zero : unique (0 : polynomial F).gal :=
 unique_gal_of_splits _ (splits_zero _)
 
@@ -90,7 +97,7 @@ instance [h : fact (p.splits (algebra_map F E))] : is_scalar_tower F p.splitting
 is_scalar_tower.of_algebra_map_eq
   (λ x, ((is_splitting_field.lift p.splitting_field p h.1).commutes x).symm)
 
-/-- The restriction homomorphism -/
+/-- Restrict from a superfield automorphism into a member of `gal p`. -/
 def restrict [fact (p.splits (algebra_map F E))] : (E ≃ₐ[F] E) →* p.gal :=
 alg_equiv.restrict_normal_hom p.splitting_field
 
@@ -100,7 +107,8 @@ alg_equiv.restrict_normal_hom_surjective E
 
 section roots_action
 
-/-- The function from `roots p p.splitting_field` to `roots p E` -/
+/-- The function taking `roots p p.splitting_field` to `roots p E`. This is actually a bijection,
+see `polynomial.gal.map_roots_bijective`. -/
 def map_roots [fact (p.splits (algebra_map F E))] :
   root_set p p.splitting_field → root_set p E :=
 λ x, ⟨is_scalar_tower.to_alg_hom F p.splitting_field E x, begin
@@ -116,6 +124,7 @@ begin
   split,
   { exact λ _ _ h, subtype.ext (ring_hom.injective _ (subtype.ext_iff.mp h)) },
   { intro y,
+    -- this is just an equality of two different ways to write the roots of `p` as an `E`-polynomial
     have key := roots_map
       (is_scalar_tower.to_alg_hom F p.splitting_field E : p.splitting_field →+* E)
       ((splits_id_iff_splits _).mpr (is_splitting_field.splits p.splitting_field p)),
@@ -126,7 +135,7 @@ begin
     exact ⟨⟨x, multiset.mem_to_finset.mpr hx1⟩, subtype.ext hx2⟩ }
 end
 
-/-- The bijection between `root_set p p.splitting_field` and `root_set p E` -/
+/-- The bijection between `root_set p p.splitting_field` and `root_set p E`. -/
 def roots_equiv_roots [fact (p.splits (algebra_map F E))] :
   (root_set p p.splitting_field) ≃ (root_set p E) :=
 equiv.of_bijective (map_roots p E) (map_roots_bijective p E)
@@ -144,13 +153,15 @@ instance gal_action_aux : mul_action p.gal (root_set p p.splitting_field) :=
   one_smul := λ _, by { ext, refl },
   mul_smul := λ _ _ _, by { ext, refl } }
 
+/-- The action of `gal p` on the roots of `p` in `E`. -/
 instance gal_action [fact (p.splits (algebra_map F E))] : mul_action p.gal (root_set p E) :=
 { smul := λ ϕ x, roots_equiv_roots p E (ϕ • ((roots_equiv_roots p E).symm x)),
   one_smul := λ _, by simp only [equiv.apply_symm_apply, one_smul],
   mul_smul := λ _ _ _, by simp only [equiv.apply_symm_apply, equiv.symm_apply_apply, mul_smul] }
 
 variables {p E}
 
+/-- `polynomial.gal.restrict p E` is compatible with `polynomial.gal.gal_action p E`. -/
 @[simp] lemma restrict_smul [fact (p.splits (algebra_map F E))]
   (ϕ : E ≃ₐ[F] E) (x : root_set p E) : ↑((restrict p E ϕ) • x) = ϕ x :=
 begin
@@ -163,7 +174,7 @@ end
 
 variables (p E)
 
-/-- `gal_action` as a permutation representation -/
+/-- `polynomial.gal.gal_action` as a permutation representation -/
 def gal_action_hom [fact (p.splits (algebra_map F E))] : p.gal →* equiv.perm (root_set p E) :=
 { to_fun := λ ϕ, equiv.mk (λ x, ϕ • x) (λ x, ϕ⁻¹ • x)
   (λ x, inv_smul_smul ϕ x) (λ x, smul_inv_smul ϕ x),
@@ -174,16 +185,13 @@ 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
 
+/-- `gal p` embeds as a subgroup of permutations of the roots of `p` in `E`. -/
 lemma gal_action_hom_injective [fact (p.splits (algebra_map F E))] :
   function.injective (gal_action_hom p E) :=
 begin
   rw monoid_hom.injective_iff,
   intros ϕ hϕ,
-  let equalizer := alg_hom.equalizer ϕ.to_alg_hom (alg_hom.id F p.splitting_field),
-  suffices : equalizer = ⊤,
-  { exact alg_equiv.ext (λ x, (set_like.ext_iff.mp this x).mpr algebra.mem_top) },
-  rw [eq_top_iff, ←splitting_field.adjoin_roots, algebra.adjoin_le_iff],
-  intros x hx,
+  ext x hx,
   have key := equiv.perm.ext_iff.mp hϕ (roots_equiv_roots p E ⟨x, hx⟩),
   change roots_equiv_roots p E (ϕ • (roots_equiv_roots p E).symm
     (roots_equiv_roots p E ⟨x, hx⟩)) = roots_equiv_roots p E ⟨x, hx⟩ at key,
@@ -195,7 +203,7 @@ end roots_action
 
 variables {p q}
 
-/-- The restriction homomorphism between Galois groups -/
+/-- `polynomial.gal.restrict`, when both fields are splitting fields of polynomials. -/
 def restrict_dvd (hpq : p ∣ q) : q.gal →* p.gal :=
 if hq : q = 0 then 1 else @restrict F _ p _ _ _
   ⟨splits_of_splits_of_dvd (algebra_map F q.splitting_field) hq (splitting_field.splits q) hpq⟩
@@ -206,10 +214,11 @@ by simp only [restrict_dvd, dif_neg hq, restrict_surjective]
 
 variables (p q)
 
-/-- The Galois group of a product embeds into the product of the Galois groups  -/
+/-- The Galois group of a product maps into the product of the Galois groups.  -/
 def restrict_prod : (p * q).gal →* p.gal × q.gal :=
 monoid_hom.prod (restrict_dvd (dvd_mul_right p q)) (restrict_dvd (dvd_mul_left q p))
 
+/-- `polynomial.gal.restrict_prod` is actually a subgroup embedding. -/
 lemma restrict_prod_injective : function.injective (restrict_prod p q) :=
 begin
   by_cases hpq : (p * q) = 0,
@@ -218,22 +227,17 @@ begin
   intros f g hfg,
   dsimp only [restrict_prod, restrict_dvd] at hfg,
   simp only [dif_neg hpq, monoid_hom.prod_apply, prod.mk.inj_iff] at hfg,
-  suffices : alg_hom.equalizer f.to_alg_hom g.to_alg_hom = ⊤,
-  { exact alg_equiv.ext (λ x, (set_like.ext_iff.mp this x).mpr algebra.mem_top) },
-  rw [eq_top_iff, ←splitting_field.adjoin_roots, algebra.adjoin_le_iff],
-  intros x hx,
-  rw [map_mul, polynomial.roots_mul] at hx,
+  ext x hx,
+  rw [root_set, map_mul, polynomial.roots_mul] at hx,
   cases multiset.mem_add.mp (multiset.mem_to_finset.mp hx) with h h,
-  { change f x = g x,
-    haveI : fact (p.splits (algebra_map F (p * q).splitting_field)) :=
+  { 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⟩) :=
       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 _) },
-  { change f x = g x,
-    haveI : fact (q.splits (algebra_map F (p * q).splitting_field)) :=
+  { 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⟩) :=
@@ -257,6 +261,7 @@ begin
     exact splits_comp_of_splits _ _ h₂, },
 end
 
+/-- `p` splits in the splitting field of `p ∘ q`, for `q` non-constant. -/
 lemma splits_in_splitting_field_of_comp (hq : q.nat_degree ≠ 0) :
   p.splits (algebra_map F (p.comp q).splitting_field) :=
 begin
@@ -293,7 +298,7 @@ begin
     (λ _, splits_of_is_unit _) (λ _ _ _ h, key2 (key1 h)),
 end
 
-/-- The restriction homomorphism from the Galois group of a homomorphism -/
+/-- `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⟩
 
@@ -303,6 +308,8 @@ by simp only [restrict_comp, restrict_surjective]
 
 variables {p q}
 
+/-- For a separable polynomial, its Galois group has cardinality
+equal to the dimension of its splitting field over `F`. -/
 lemma card_of_separable (hp : p.separable) :
   fintype.card p.gal = finrank F p.splitting_field :=
 begin
@@ -333,14 +340,16 @@ begin
   rw [aeval_def, map_root_of_splits _ (splitting_field.splits p) hp],
 end
 
+section rationals
+
 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 ℚ) :
+    the number of roots not fixed by complex conjugation (i.e. with some imaginary component). -/
+lemma card_complex_roots_eq_card_real_add_card_not_gal_inv (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
@@ -391,7 +400,7 @@ begin
   { apply_instance },
 end
 
-/-- An irreducible polynomial of prime degree with two non-real roots has full Galois group -/
+/-- 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) :
@@ -415,10 +424,10 @@ begin
   { 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 p).symm },
+    exact (card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm },
 end
 
-/-- An irreducible polynomial of prime degree with 1-3 non-real roots has full Galois group -/
+/-- An irreducible polynomial of prime degree with 1-3 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_roots1 : fintype.card (p.root_set ℝ) + 1 ≤ fintype.card (p.root_set ℂ))
@@ -432,7 +441,7 @@ begin
   equiv.perm.two_dvd_card_support (by rw [←monoid_hom.map_pow, ←monoid_hom.map_pow,
     show alg_equiv.restrict_scalars ℚ complex.conj_alg_equiv ^ 2 = 1,
     from alg_equiv.ext complex.conj_conj, monoid_hom.map_one, monoid_hom.map_one]),
-  have key := gal_action_hom_bijective_of_prime_degree_aux p,
+  have key := card_complex_roots_eq_card_real_add_card_not_gal_inv p,
   simp_rw [set.to_finset_card] at key,
   rw [key, add_le_add_iff_left] at p_roots1 p_roots2,
   rw [key, add_right_inj],
@@ -444,6 +453,8 @@ begin
     (show 2 * 0 + 1 ≠ 2 * k, from nat.two_mul_ne_two_mul_add_one.symm))),
 end
 
+end rationals
+
 end gal
 
 end polynomial