Irreducible

Stream: mathlib4

[BANGJI HU]

How do I use Eisenstein in mathlib to prove irreducibility

import Mathlib.Analysis.Complex.Polynomial.UnitTrinomial
import Mathlib.RingTheory.Polynomial.GaussLemma
import Mathlib.Tactic.LinearCombination

open Polynomial

theorem X_pow_sub_X_sub_one_irreducible_rat : Irreducible (X ^ 3 - X^2 - 8 : ℚ[X]) := by
sorry

[Kevin Buzzard]

What's the maths proof? Eisenstein does not apply to that polynomial

[Edison Xie]

Kevin Buzzard said:

What's the maths proof? Eisenstein does not apply to that polynomial

math proof is probly prime test at 3 since it has no root in $\mathbb{F}_{3}$?

[Jeremy Tan]

Or RRT

[Ilmārs Cīrulis]

I tried and tinkered, but got stuck.
The first sorry, maybe, is solved by showing that no integer divisors of -8 are roots of polynomial.
The second sorry seems like it should be easy, but it isn't for me, probably because I don't know something.

:dissolve:

import Mathlib
open Polynomial

theorem X_pow_sub_X_sub_one_irreducible_rat : Irreducible (X ^ 3 - X^2 - 8 : ℚ[X]) := by
  have H: (X ^ 3 - X ^ 2 - 8: ℚ[X]) = map (Int.castRingHom ℚ) (X ^ 3 - X ^ 2 - 8: ℤ[X]) := by simp
  rw [H, <- Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast] <;> clear H
  . sorry
  . intro r Hr
    rw [<- Polynomial.dvd_content_iff_C_dvd] at Hr
    have H: (X ^ 3 - X ^ 2 - 8: ℤ[X]).content = 1 := by
      sorry
    rw [H] at Hr
    exact isUnit_of_dvd_one Hr

[Yury G. Kudryashov]

I suggest that we wait for (1) a math proof; (2) the source of the problem from @hand bob before trying to answer the question.

[BANGJI HU]

The Rational Root Theorem states that any rational root $pq$ of $f(x)$ must satisfy:

• $p$ divides the constant term ($−8$),

• $q$ divides the leading coefficient ($1$).

Thus, the possible rational roots are $±1,±2,±4,±8$.

[Yury G. Kudryashov]

This answers (1) but not (2).

[Yury G. Kudryashov]

Anyway,

• The Rational Root Theorem is not in Mathlib yet. You're welcome to formalize & PR it.
• You'll also need a theorem saying that a reducible polynomial of degree \le 3 has a root.

[BANGJI HU]

The Rational Root Theorem states that if a polynomial with integer coefficients
f(x) = a_n x^n + a_{n-1} x^{n-1} + ... + a_0
has a rational root p/q (where p and q are coprime integers), then p must be a divisor of the constant term a_0, and q must be a divisor of the leading coefficient a_n.

For the polynomial
f(x) = x^3 + 3x^2 - 8,
the leading coefficient a_n = 1, and the constant term a_0 = -8. Therefore, the possible rational roots are:
p/q = ±1, ±2, ±4, ±8.

We verify each of these possible rational roots:

import Mathlib



open Polynomial
open IsFractionRing

--Given the polynomial : $f(x) = x^3 + x + 7$
noncomputable def P : Polynomial ℤ := C 1 * X ^ 3 + C 3 * X^2 - C 8
--All this lemmas are some trivial things in mathmetics, but not easy in lean

lemma coeffs : (∀ n > 3, P.coeff n = 0) ∧ P.coeff 3 = 1 ∧
    P.coeff 2 = 3 ∧ P.coeff 1 = 0 ∧ P.coeff 0 = -8 := by
  simp only [P, coeff_add, coeff_C, coeff_C_mul_X, coeff_C_mul_X_pow]
  norm_num
  intro n hn
  repeat' rw [if_neg]
  any_goals linarith only [hn]
  simp only [add_zero, zero_sub, neg_eq_zero]
  compute_degree
  omega
--1.$\operatorname{deg}P = 3$
lemma P_natDeg : P.natDegree = 3 :=
  have : P.degree = 3 := by
    unfold P; compute_degree
    simp only [ne_eq, one_ne_zero, not_false_eq_true]
    repeat exact Nat.le_of_ble_eq_true rfl
  natDegree_eq_of_degree_eq_some this

lemma P_inQ_natDeg : (Polynomial.map (algebraMap ℤ ℚ) P).natDegree = 3 := by
  have : (Polynomial.map (algebraMap ℤ ℚ) P).coeff 3 = (algebraMap ℤ ℚ) (P.coeff 3) :=
    coeff_map (algebraMap ℤ ℚ) 3
  simp only [coeffs.2.1, algebraMap_int_eq, eq_intCast, Int.cast_one] at this
  have : (Polynomial.map (algebraMap ℤ ℚ) P).natDegree ≥ 3 :=
    le_natDegree_of_ne_zero <| ne_zero_of_eq_one this
  linarith[natDegree_map_le (algebraMap ℤ ℚ) P, P_natDeg]

example : Irreducible (Polynomial.map (algebraMap ℤ ℚ) P) := by
  --2. $P \neq 0$
  have P_inQ_notzero : Polynomial.map (algebraMap ℤ ℚ) P ≠ 0 :=
    zero_le_degree_iff.mp <| le_of_lt <| natDegree_pos_iff_degree_pos.mp
    <| by rw [P_inQ_natDeg]; norm_num
  --3.$P$ is not unit
  have P_inQ_notUnit : ¬IsUnit (Polynomial.map (algebraMap ℤ ℚ) P) := by
    apply not_isUnit_of_natDegree_pos
    rw[P_inQ_natDeg]; norm_num

  /-The Rational Root Theorem states that if a polynomial with integer coefficients has a rational root
    $ \frac{p}{q} $ (in lowest terms), then $ p $ divides the constant term and $q$ divides
    the leading coefficient. -/
  apply (irreducible_iff_degree_lt (Polynomial.map (algebraMap ℤ ℚ) P) P_inQ_notzero
    P_inQ_notUnit).mpr

  intro q qdeg dvd
  simp only [P_inQ_natDeg, Nat.reduceDiv, Nat.cast_one] at qdeg

  have qneq0: q ≠ 0 := fun nq ↦ (by simp only [nq, zero_dvd_iff] at dvd; contradiction)

  by_cases choice : q.natDegree = 1
  · have choice : q.degree = 1 := by rw[degree_eq_natDegree qneq0, choice, Nat.cast_one]

    obtain ⟨x, hx⟩ : ∃ x, q.IsRoot x := exists_root_of_degree_eq_one choice

    have x_P_root : (aeval x) P = 0 := by
      rw[← (aeval_map_algebraMap ℚ x P)]
      exact aeval_eq_zero_of_dvd_aeval_eq_zero dvd hx
    have den_dvd : (den ℤ x : ℤ) ∣ P.leadingCoeff := den_dvd_of_is_root x_P_root
    rw[← coeff_natDegree, P_natDeg, coeffs.2.1] at den_dvd

    have den_dvd : (den ℤ x : ℤ) = 1 ∨ (den ℤ x : ℤ) = -1 :=
      Int.natAbs_eq_natAbs_iff.mp <| Nat.eq_one_of_dvd_one <| Int.ofNat_dvd_right.mp den_dvd

    have dvd : IsLocalization.mk' ℚ (num ℤ x) (den ℤ x) = x := mk'_num_den ℤ x
    simp only [mk'_eq_div, algebraMap_int_eq, eq_intCast] at dvd

    obtain ⟨x₀, hx⟩ : ∃ x₀ : ℤ , (x₀ : ℚ) = x := by
      rcases den_dvd with h | h
      · simp only [h, Int.cast_one, div_one] at dvd
        use (num ℤ x : ℤ)
      · simp only [h, Int.reduceNeg, Int.cast_neg, Int.cast_one] at dvd
        use (-num ℤ x : ℤ)
        nth_rw 2[← dvd]
        rw[div_neg (num ℤ x : ℚ), div_one (num ℤ x : ℚ), Int.cast_neg]

    simp only [P] at x_P_root
    rw [map_add, map_add, aeval_C] at x_P_root
    simp only [eq_intCast, Int.cast_one, one_mul, map_pow, aeval_X, algebraMap_int_eq,
      Int.cast_ofNat] at x_P_root
    have t1 : x < 0 := by by_contra nh; push_neg at nh; linarith[pow_nonneg nh 3]

    have t2 : -2 < x := by
      by_contra nh; push_neg at nh
      have : x ^ 3 ≤ (-2) ^ 3 := by
        have : 2 ^ 3 ≤ (-x) ^ 3 := by
          apply pow_le_pow_left
          repeat linarith
        have : - (-x) ^ 3 ≤ - 2 ^ 3 := by linarith
        rw [Odd.neg_pow (Nat.odd_iff.mpr rfl)] at this
        linarith
      linarith

    rw[← hx] at t1 t2 x_P_root
    simp only [Int.cast_lt_zero] at t1
    have : -1 ≤ x₀ := Int.cast_lt.mp t2

    have : x₀ = -1 := by linarith [Int.le_sub_one_of_lt t1]
    simp only [this, Int.reduceNeg, Int.cast_neg, Int.cast_one] at x_P_root
    norm_num at x_P_root

  ·
    have qdeg : q.natDegree < 1 := Nat.lt_of_le_of_ne (natDegree_le_iff_degree_le.mpr qdeg) choice
    have := degree_eq_natDegree qneq0
    rw [Nat.lt_one_iff.mp qdeg, CharP.cast_eq_zero] at this
    exact isUnit_iff_degree_eq_zero.mpr this

[BANGJI HU]

@Ilmārs Cīrulis

[Aaron Hill]

Yury G. Kudryashov said:

Anyway,

• The Rational Root Theorem is not in Mathlib yet. You're welcome to formalize & PR it.
• You'll also need a theorem saying that a reducible polynomial of degree \le 3 has a root.

Slightly off-topic - I think the rational root theorem is already in mathlib:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Polynomial/RationalRoot.html#isInteger_of_is_root_of_monic

[Yury G. Kudryashov]

Thanks! We should specialize it to integer & rational numbers though.