English
If p ∈ ℚ[X] is irreducible of prime degree with certain root-count bounds, then the Galois action is bijective.
Русский
Если p ∈ ℚ[X] ирредуцируемый и имеет простую степень при некоторых ограничениях числа корней, галуа‑действие биективно.
LaTeX
$$$$ \\text{If } p \\text{ irreducible with prime degree and suitable root-count bounds, then } \\mathrm{galActionHom}(p, \\mathbb{C}) \\text{ is bijective.} $$$$
Lean4
/-- An irreducible polynomial of prime degree with 1-3 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_roots1 : Fintype.card (p.rootSet ℝ) + 1 ≤ Fintype.card (p.rootSet ℂ))
(p_roots2 : Fintype.card (p.rootSet ℂ) ≤ Fintype.card (p.rootSet ℝ) + 3) : Function.Bijective (galActionHom p ℂ) :=
by
apply galActionHom_bijective_of_prime_degree p_irr p_deg
let n := (galActionHom p ℂ (restrict p ℂ (Complex.conjAe.restrictScalars ℚ))).support.card
have hn : 2 ∣ n :=
Equiv.Perm.two_dvd_card_support
(by
rw [← MonoidHom.map_pow, ← MonoidHom.map_pow,
show AlgEquiv.restrictScalars ℚ Complex.conjAe ^ 2 = 1 from AlgEquiv.ext Complex.conj_conj, MonoidHom.map_one,
MonoidHom.map_one])
have key := card_complex_roots_eq_card_real_add_card_not_gal_inv p
simp_rw [Set.toFinset_card] at key
omega