English
If p ∈ ℚ[X] is irreducible and has prime degree, then the Galois action on its complex roots is bijective (the full Galois group).
Русский
Если p ∈ ℚ[X] ирредуцируем и имеет простую степень, то Галоа-группа действует на корни полно (биективно).
LaTeX
$$$$ \\text{If } p \\text{ irreducible with } \\mathrm{natDegree}(p) \\text{ prime, then } \\mathrm{galActionHom}(p, \\mathbb{C}) \\text{ is bijective.} $$$$
Lean4
/-- An irreducible polynomial of prime degree with two non-real roots has full Galois group. -/
theorem galActionHom_bijective_of_prime_degree {p : ℚ[X]} (p_irr : Irreducible p) (p_deg : p.natDegree.Prime)
(p_roots : Fintype.card (p.rootSet ℂ) = Fintype.card (p.rootSet ℝ) + 2) : Function.Bijective (galActionHom p ℂ) :=
by
classical
have h1 : Fintype.card (p.rootSet ℂ) = p.natDegree :=
by
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
rw [Multiset.toFinset_card_of_nodup, ← natDegree_eq_card_roots]
· exact IsAlgClosed.splits_codomain p
· exact nodup_roots ((separable_map (algebraMap ℚ ℂ)).mpr p_irr.separable)
let conj' := restrict p ℂ (Complex.conjAe.restrictScalars ℚ)
refine
⟨galActionHom_injective p ℂ, fun x =>
(congr_arg (x ∈ ·) (show (galActionHom p ℂ).range = ⊤ from ?_)).mpr (Subgroup.mem_top x)⟩
apply Equiv.Perm.subgroup_eq_top_of_swap_mem
· rwa [h1]
· rw [h1]
simpa only [Fintype.card_eq_nat_card,
Nat.card_congr (MonoidHom.ofInjective (galActionHom_injective p ℂ)).toEquiv.symm] using
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.toFinset_card (rootSet p ℝ), ← Set.toFinset_card (rootSet p ℂ)]
exact (card_complex_roots_eq_card_real_add_card_not_gal_inv p).symm
