galActionHom_bijective_of_prime_degree'

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

Похожие утверждения