Proving that ((X^2 - X + 5) : ℤ[X]) is prime

Stream: new members

[Isak Colboubrani]

What is the simplest way to prove that the polynomial ((X^2 - X + 5) : ℤ[X]) is prime using Mathlib?

import Mathlib
open Polynomial
example : Prime ((X^2 - X + 5) : ℤ[X]) := by sorry

[Ruben Van de Velde]

Searching https://loogle.lean-lang.org for Prime, Polynomial, it doesn't seem like we have much for polynomials of degree > 1

[Kevin Buzzard]

What's the simplest way to prove it's prime mathematically? Z[X] is a polynomial ring over a UFD so it's a UFD, so prime iff irreducible,.and now Gauss' lemma says irreducible iff irreducible in Q[X] because the degree is positive (even this positivity claim needs a proof and a little thought is required here!), and now a result in mathlib says a polynomial of degree <= 3 over a field is irreducible iff it has no roots, and another theorem says that if a monic polynomial with integer coefficients has a rational root then that rational root is integral and divides the constant term, and now you just have four numbers to check.

[Scott Carnahan]

Once you get to the irreducible condition, you can try factoring X^2 - X + 5 into a product of two non-units in Z[X], and bash out some cases.

[Daniel Weber]

You can substitute x = t + 2 to get t² + 3t + 7 and apply Cohn's irreducibility criterion

[Daniel Weber]

Or substitute x = t + 10 to get t² + 19t + 95 and apply Eisenstein's criterion

[Damiano Testa]

If we're still giving ways of proving it, to show irreducibility you can also reduce modulo two and try all possibilities.

[Johan Commelin]

There was a project to define computable polynomials. One motivating application was a tactic for such irreducibility proofs.

[Johan Commelin]

@Alain Chavarri Villarello do you know the status of the project, by chance?

[Johan Commelin]

@Kevin Buzzard I can't find the "degree <= 3" result. It was discussed recently, but I'm not sure it is actually in mathlib.

[Riccardo Brasca]

docs#Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three

[Johan Commelin]

I've started on the suggested approaches. This is what I have so far

import Mathlib
open Polynomial

theorem monic_helper : Monic ((X^2 - X + 5) : ℤ[X]) := by
  unfold Polynomial.Monic Polynomial.leadingCoeff
  have : (X^2 - X + 5 : ℤ[X]).natDegree = 2 := by
    compute_degree
    norm_num
  rw [this]
  simp
  apply coeff_X_of_ne_one
  norm_num

@[simps]
noncomputable
def Polynomial.linearSubst {R : Type*} [CommRing R] (r : R) : R[X] ≃+* R[X] where
  __ := (Polynomial.aeval (R := R) (X + C r)).toRingHom
  invFun := (Polynomial.aeval (R := R) (X - C r)).toRingHom
  left_inv := by
    intro f
    dsimp
    rw [← AlgHom.comp_apply]
    conv_rhs => rw [← AlgHom.id_apply (R := R) f]
    congr 1
    ext
    simp
  right_inv := by
    intro f
    dsimp
    rw [← AlgHom.comp_apply]
    conv_rhs => rw [← AlgHom.id_apply (R := R) f]
    congr 1
    ext
    simp

theorem RingEquiv.irreducible_apply {R S : Type*} [CommRing R] [CommRing S] (e : R ≃+* S) (r : R) :
    Irreducible (e r) ↔ Irreducible r := by
  constructor
  · intro h
    constructor
    · intro oops
      apply h.not_unit
      exact e.isUnit_iff.mpr oops
    · intro a b hab
      apply (h.isUnit_or_isUnit (by simpa using congr(e $hab))).imp
        e.isUnit_iff.mp e.isUnit_iff.mp
  · intro h
    constructor
    · intro oops
      apply h.not_unit
      exact (RingEquiv.isUnit_iff e).mp oops
    · intro a b hab
      apply (h.isUnit_or_isUnit (by simpa using congr(e.symm $hab))).imp
        e.symm.isUnit_iff.mp e.symm.isUnit_iff.mp

-- Kevin
example : Prime ((X^2 - X + 5) : ℤ[X]) := by
  rw [← irreducible_iff_prime]
  rw [Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map (K := ℚ) (h := ?monic)]
  case monic => exact monic_helper
  suffices Irreducible (X^2 - X + 5 : ℚ[X]) by simpa
  sorry

-- Daniel (Eisenstein edition)
example : Prime ((X^2 - X + 5) : ℤ[X]) := by
  rw [← irreducible_iff_prime]
  let f : ℤ[X] ≃+* ℤ[X] := Polynomial.linearSubst 10
  rw [← RingEquiv.irreducible_apply f]
  have aux : f (X^2 - X + 5) = X^2 + 19 * X + 95 := by
    simp [f, map_ofNat]
    ring
  rw [aux]
  have hndeg : natDegree (X^2 + 19 * X + 95 : ℤ[X]) = 2 := by
    compute_degree <;> norm_num
  have hdeg : degree (X^2 + 19 * X + 95 : ℤ[X]) = 2 := by
    rw [degree_eq_natDegree, hndeg]
    · simp
    · intro a; simp_all only [natDegree_zero, OfNat.zero_ne_ofNat] -- aesop
  let I := Ideal.span (α := ℤ) {19}
  have hI : I.IsPrime := by
    sorry
  apply Polynomial.irreducible_of_eisenstein_criterion hI
  · rw [leadingCoeff, hndeg]
    simpa [coeff_X_of_ne_one, ← Ideal.eq_top_iff_one] using hI.ne_top
  · sorry
  · rw [hdeg]; norm_num
  · dsimp only [I]
    rw [pow_two, Ideal.span_singleton_mul_span_singleton]
    rw [Ideal.mem_span_singleton]
    simp
    norm_num
  · sorry

-- Damiano
example : Prime ((X^2 - X + 5) : ℤ[X]) := by
  rw [← irreducible_iff_prime]
  let f : ℤ →+* ZMod 2 := Int.castRingHom (ZMod 2)
  apply Polynomial.Monic.irreducible_of_irreducible_map f
  · exact monic_helper
  suffices Irreducible (X^2 - X + 5 : (ZMod 2)[X]) by simpa [f]
  suffices Irreducible (X^2 + X + 1 : (ZMod 2)[X]) by
    convert this using 1
    rw [← sub_eq_zero]
    ring_nf -- we really need `ring` mod characteristic p, PR exists!
    have h20 : (2 : ZMod 2) = 0 := rfl
    have h40 : (4 : ZMod 2) = 0 := rfl
    rw [← Polynomial.C_inj, map_ofNat, map_zero] at h20 h40
    simp [h20, h40]
  -- decide -- haha! only serious
  -- norm_num -- haha! still serious
  sorry

[Johan Commelin]

Clearly we need a lot more tactic support here.

[Damiano Testa]

Can't the monic goal be solved by monicity!?

[Damiano Testa]

Also, compute_degree! discharges with norm_num (or it should!).

[Riccardo Brasca]

The linear substitution and the fact that irreducibility is persevered by equiv should be in mathlib

[Riccardo Brasca]

I mean, we want those

[Damiano Testa]

I think that irreducibility of image implies irreducible is there.

[Damiano Testa]

docs#of_irreducible_map maybe?

[Riccardo Brasca]

That one is for local hom. In general it is false because one factor can be sent to a unit

[Damiano Testa]

Right, but I think that the definition of local Hom is general enough that it applies to an iso.

[Riccardo Brasca]

Ah yes, you're right

[Johan Commelin]

That's a good point

[Damiano Testa]

Btw, somewhere in the docs for local hom it should say that it is more general...

[Johan Commelin]

I finished the Eisenstein approach suggested by Daniel Weber

-- Daniel (Eisenstein edition)
example : Prime ((X^2 - X + 5) : ℤ[X]) := by
  rw [← irreducible_iff_prime]
  let f : ℤ[X] ≃+* ℤ[X] := Polynomial.linearSubst 10
  rw [← RingEquiv.irreducible_apply f]
  have aux : f (X^2 - X + 5) = X^2 + 19 * X + 95 := by
    simp [f, map_ofNat]
    ring
  rw [aux]
  have hndeg : natDegree (X^2 + 19 * X + 95 : ℤ[X]) = 2 := by compute_degree!
  have hdeg : degree (X^2 + 19 * X + 95 : ℤ[X]) = 2 := by compute_degree!
  let I := Ideal.span (α := ℤ) {19}
  have hI : I.IsPrime := by
    rw [Ideal.span_singleton_prime, Int.prime_iff_natAbs_prime] <;> norm_num
  apply Polynomial.irreducible_of_eisenstein_criterion hI
  · rw [leadingCoeff, hndeg]
    simpa [coeff_X_of_ne_one, ← Ideal.eq_top_iff_one] using hI.ne_top
  · simp only [coe_lt_degree, hndeg, coeff_add, coeff_X_pow, coeff_ofNat_mul]
    intro n hn
    interval_cases n <;> simp
    · rw [Ideal.mem_span_singleton]
      norm_num
    · exact Ideal.mem_span_singleton_self 19
  · rw [hdeg]; norm_num
  · dsimp only [I]
    rw [pow_two, Ideal.span_singleton_mul_span_singleton]
    rw [Ideal.mem_span_singleton]
    simp
    norm_num
  · rw [isPrimitive_iff_content_eq_one, content_eq_gcd_range_succ, hndeg]
    simp [Finset.range_succ, coeff_X_of_ne_one]

[Johan Commelin]

And Kevin's approach:

-- Kevin
example : Prime ((X^2 - X + 5) : ℤ[X]) := by
  rw [← irreducible_iff_prime]
  have hmon : Monic (X^2 - X + 5 : ℤ[X]) := by monicity!
  rw [Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map (K := ℚ) hmon]
  suffices Irreducible (X^2 - X + 5 : ℚ[X]) by simpa
  rw [Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three]
  swap; apply le_of_eq; symm; compute_degree!
  swap; compute_degree!
  rw [Multiset.eq_zero_iff_forall_not_mem]
  intro x hx
  rw [mem_roots_iff_aeval_eq_zero (ne_zero_of_mem_roots hx)] at hx
  obtain ⟨x, rfl, h⟩ := exists_integer_of_is_root_of_monic hmon (r := x) <| by simpa [map_ofNat] using hx
  simp only [coeff_add, coeff_sub, coeff_X_pow, OfNat.zero_ne_ofNat, ↓reduceIte, coeff_X_zero,
    sub_self, coeff_ofNat_zero, zero_add, algebraMap_int_eq, eq_intCast, map_add, map_sub, map_pow,
    aeval_X, map_ofNat] at h hx
  have : x.natAbs = 1 ∨ x.natAbs = 5 := by
    simp [← Int.natAbs_dvd_natAbs, Int.reduceAbs] at h
    refine (Nat.dvd_prime ?_).mp h
    decide
  rw [Int.natAbs_eq_iff, Int.natAbs_eq_iff] at this
  revert hx
  rcases this with (rfl|rfl) | (rfl|rfl)
  all_goals
    norm_num

[Johan Commelin]

And the version by Damiano

-- Damiano
example : Prime ((X^2 - X + 5) : ℤ[X]) := by
  rw [← irreducible_iff_prime]
  let f : ℤ →+* ZMod 2 := Int.castRingHom (ZMod 2)
  apply Polynomial.Monic.irreducible_of_irreducible_map f
  · monicity!
  suffices Irreducible (X^2 - X + 5 : (ZMod 2)[X]) by simpa [f]
  suffices Irreducible (X^2 + X + 1 : (ZMod 2)[X]) by
    convert this using 1
    rw [← sub_eq_zero]
    ring_nf -- we really need `ring` mod characteristic p, PR exists!
    have h20 : (2 : ZMod 2) = 0 := rfl
    have h40 : (4 : ZMod 2) = 0 := rfl
    rw [← Polynomial.C_inj, map_ofNat, map_zero] at h20 h40
    simp [h20, h40]
  -- decide -- haha! only serious
  -- norm_num -- haha! still serious
  rw [Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three]
  swap; apply le_of_eq; symm; compute_degree!
  swap; compute_degree!
  rw [Multiset.eq_zero_iff_forall_not_mem]
  intro x
  fin_cases x
  · norm_num
  · simp only [Nat.reduceAdd, Fin.mk_one, Fin.isValue, mem_roots', ne_eq, IsRoot.def, eval_add,
      eval_pow, eval_X, one_pow, eval_one, not_and]
    contrapose!
    intro h
    exfalso
    have : (1 + 1 : ZMod 2) = 0 := rfl
    rw [this, zero_add] at h
    exact one_ne_zero h

[Kevin Buzzard]

Nice! The joys of the weekend! Actually this probably informed you about how we might approach writing a tactic for this. Although I'm a bit conflicted between whether we should be hacking out something which works for small degree or actually attempting to get someone to implement a good algorithm for factoring polynomials in general. In other words do we want a toy model like the above (deals with degree 2 and small coefficients, which will satisfy most of the people who come here saying "how do you do this easy-looking question in lean"), something actually comparable to a CAS, or maybe we're just happy with the status quo and there being no algo at all because we're not attempting to be a CAS.

[Johan Commelin]

Eventually I would like something comparable to a CAS. But that's a big project. I think it's fine to have an underpowered tactic that is good enough for toy questions until the industrial strength version arrives

[Kevin Buzzard]

So you're saying "perfect is the enemy of good" applies even if we don't have an application beyond "satisfy new users who are still learning what the software does by asking questions like this". I guess we did the same for primality testing too -- some norm_num plugin that probably was nontrivial to write but only has toy applications.

[Johan Commelin]

It also makes it more likely that you can adapt Lean to undergrad algebra homework exercise sheets without too much trouble.

[Kevin Buzzard]

Yes this is true! Typically the homework that maths academics set will only have calculations which can be done by hand, so this is definitely an argument for automating as far as "can be done easily by hand", which is exactly what we have for primality testing right now.

[Riccardo Brasca]

I think a tactic for monic polynomials of degree 2 and 3 (with integer coefficients) would be great. Of course for things like maple this is completely trivial, but we need to start somewhere.

[Daniel Weber]

I'm currently working on proving Cohn's criterion, and assuming Buniakowski’s conjecture that gives a fairly simple method to prove irreducibility

[Johan Commelin]

@Daniel Weber are your proving Cohn's criterion wrt an arbitrary base $b$?

[Daniel Weber]

I'm proving theorem 1 from https://mast.queensu.ca/%7Emurty/monthly.pdf , which is slightly different

[Johan Commelin]

But also easier to apply, I think

[Daniel Weber]

Yes, it doesn't require positivity of the coefficients

[Damiano Testa]

This is great: thanks Johan for verifying all proofs! For fun, I golfed a little the argument that I suggested: it could be shortened more, but I think that as is, it is still fairly legible:

-- Damiano
example : Prime ((X^2 - X + 5) : ℤ[X]) := by
  apply irreducible_iff_prime.mp
  let f : ℤ →+* ZMod 2 := Int.castRingHom (ZMod 2)
  apply Monic.irreducible_of_irreducible_map f
  · monicity!
  simp only [Polynomial.map_add, Polynomial.map_sub, Polynomial.map_pow, map_X,
    Polynomial.map_ofNat]
  reduce_mod_char
  -- decide -- haha! only serious
  -- norm_num -- haha! still serious
  rw [irreducible_iff_roots_eq_zero_of_degree_le_three, Multiset.eq_zero_iff_forall_not_mem]
  · intro x
    fin_cases x <;>
      norm_num
    contrapose!
    decide
  · exact (Eq.symm (by compute_degree!)).le
  · compute_degree!

[Michael Stoll]

import Mathlib

open Polynomial

example : Prime ((X^2 - X + 5) : ℤ[X]) := by
  rw [← irreducible_iff_prime]
  apply Monic.irreducible_of_irreducible_map <| Int.castRingHom (ZMod 2)
  · monicity!
  simp only [Polynomial.map_add, Polynomial.map_sub, Polynomial.map_pow, map_X,
    Polynomial.map_ofNat]
  reduce_mod_char
  have hdeg : (X ^ 2 + X + 1 : (ZMod 2)[X]).natDegree = 2 := by compute_degree!
  rw [irreducible_iff_roots_eq_zero_of_degree_le_three, Multiset.eq_zero_iff_forall_not_mem]
  · intro x
    simp only [mem_roots', IsRoot.def, eval_add, eval_pow, eval_X, eval_one, not_and, not_imp_not]
    fin_cases x <;> norm_num
    decide
  all_goals omega

The first goal after the last rw should really be a job for decide as is...

[Daniel Weber]

I managed to prove theorem1 such that

example : Prime ((X^2 - X + 5) : ℤ[X]) := by
  apply irreducible_iff_prime.mp
  have t1 : (X^2 - X + 5 : ℤ[X]).natDegree = 2 := by compute_degree!
  have t2 : (X^2 - X + 5 : ℤ[X]).leadingCoeff = 1 := by monicity!
  apply theorem1 _ (by simp [t1]) 7
  · simp [H, t1, t2, range_succ, Int.norm_eq_abs]
    norm_num
  rw [irreducible_iff_prime, Int.prime_iff_natAbs_prime]
  norm_num

example : Prime ((X^4 + 6*X^2 + 1) : ℤ[X]) := by
  apply irreducible_iff_prime.mp
  have t1 : (X^4 + 6*X^2 + 1 : ℤ[X]).natDegree = 4 := by compute_degree!
  have t2 : (X^4 + 6*X^2 + 1 : ℤ[X]).leadingCoeff = 1 := by monicity!
  apply theorem1 _ (by simp [t1]) 8
  · simp [H, t1, t2, range_succ, Int.norm_eq_abs, coeff_one]
    norm_num
  rw [irreducible_iff_prime, Int.prime_iff_natAbs_prime]
  norm_num

https://gist.github.com/Command-Master/fec6acf0e422b9e326d5fa117b5f2ab8

[Damiano Testa]

The leadingCoeff = 1 goals can be proved by monicity!.

[Damiano Testa]

Btw, I think that it would be relatively straightforward to produce a tactic that proves irreducibility of polynomials of degree at most three, leaving around a goal of showing that the polynomial has no roots.

[Damiano Testa]

However, proving more generally irreducibility of higher degree polynomials would be much much harder.

[Johan Commelin]

Nice!

[Alain Chavarri Villarello]

Johan Commelin ha dicho:

Alain Chavarri Villarello do you know the status of the project, by chance?

Hi! I’m a couple of weeks late to this conversation :see_no_evil: . I’m not sure what the status of that project is, but in a different project I’ve been working on (formally verifying rings of integers link), we used lists as computable polynomials and formalized some certificates for polynomial irreducibility over finite fields and over the integers, including degree analysis and a prime witness certificate (similar in flavor to Theorem 1 that you mentioned, @Daniel Weber ). We didn’t write a tactic, but we have SageMath code that writes a Lean proof given a polynomial. Some examples of irreducibility proofs are available in DedekindProject4/ExamplesIrreducible.