generalizedEisenstein — Mathlib

English

Under suitable hypotheses, including a prime irreducible factor q in a larger field K, a primitive f with image a power of q is irreducible.

Русский

При подходящих предположениях, включая простейший ирреализуемый фактор q в большем поле K, полином f с образом, являющимся степенью q, ирредуцируем.

LaTeX

$$$\\text{generalizedEisenstein}: Irreducible (map_{R\\to K} f) \\text{ given } q.Monic, f.IsPrimitive, 0 < deg f, nonzero leadingCoeff, f.map = C * q^p, f.modByMonic q \\neq 0$$$

Lean4

/-- A generalized Eisenstein criterion

Let `R` be an integral domain and `K` an `R`-algebra which is a domain.
Let `q : R[X]` be a monic polynomial which is prime in `K[X]`.
Let `f : R[X]` be a primitive polynomial of strictly positive degree
whose leading coefficient is not zero in `K`
and such that the image `f` in `K[X]` is a power of `q`.
Assume moreover that `f.modByMonic q` is not zero in `(R ⧸ (P ^ 2))[X]`,
where `P` is the kernel of `algebraMap R K`.
Then `f` is irreducible. -/
theorem generalizedEisenstein {q f : R[X]} {p : ℕ} (hq_irr : Irreducible (q.map (algebraMap R K))) (hq_monic : q.Monic)
    (hf_prim : f.IsPrimitive) (hfd0 : 0 < natDegree f) (hfP : algebraMap R K f.leadingCoeff ≠ 0)
    (hfmodP : f.map (algebraMap R K) = C (algebraMap R K f.leadingCoeff) * q.map (algebraMap R K) ^ p)
    (hfmodP2 : (f.modByMonic q).map (mk ((ker (algebraMap R K)) ^ 2)) ≠ 0) : Irreducible f
    where
  not_isUnit := mt degree_eq_zero_of_isUnit fun h => by simp_all [natDegree_pos_iff_degree_pos]
  isUnit_or_isUnit g h
    h_eq := by
    -- We have to show that factorizations `f = g * h` are trivial

    set P : Ideal R := ker (algebraMap R K)
    obtain ⟨m, r, hg, hr, hm0⟩ :=
      generalizedEisenstein_aux hq_irr hq_monic hfP hf_prim hfmodP (h_eq ▸ dvd_mul_right g h)
    obtain ⟨n, s, hh, hs, hn0⟩ := generalizedEisenstein_aux hq_irr hq_monic hfP hf_prim hfmodP (h_eq ▸ dvd_mul_left h g)
    by_cases hm :
      m =
        0
          -- If `m = 0`, `generalizedEisenstein_aux` shows that `g` is a unit.

    · left; exact hm0 hm
    by_cases hn :
      n =
        0
          -- If `n = 0`, `generalizedEisenstein_aux` shows that `h` is a unit.

    · right; exact hn0 hn
    exfalso
    apply hfmodP2
    suffices f %ₘ q = (r * s) %ₘ q by
      -- Since the coefficients of `r` and `s` are in `P`, those of `r * s` are in `P ^ 2`

      suffices h : map (Ideal.Quotient.mk (P ^ 2)) (r * s) = 0 by simp [this, h, map_modByMonic, hq_monic]
      ext n
      have h (x : ℕ × ℕ) : (Ideal.Quotient.mk (P ^ 2)) (r.coeff x.1 * s.coeff x.2) = 0 :=
        by
        rw [eq_zero_iff_mem, pow_two]
        apply mul_mem_mul
        · rw [mem_ker, ← coeff_map, hr, coeff_zero]
        · rw [mem_ker, ← coeff_map, hs, coeff_zero]
      simp [-Polynomial.map_mul, coeff_mul, h]
        -- It remains to prove the equality `f %ₘ q = (r * s) %ₘ q`, which is straightforward

    rw [h_eq, hg, hh]
    simp only [add_mul, mul_add, map_add, ← modByMonicHom_apply]
    simp only [← add_assoc, modByMonicHom_apply]
    iterate 3 rw [(modByMonic_eq_zero_iff_dvd hq_monic).mpr]
    · simp
    · exact ((dvd_pow_self q hm).mul_left _).mul_right _
    · simp only [← mul_assoc]
      exact (dvd_pow_self q hn).mul_left _
    · exact ((dvd_pow_self q hn).mul_left _).mul_left _

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