(Z/6Z)[X]

Stream: maths

[Kenny Lau]

In #Is there code for X? > diagonalizable linear maps @Aaron Liu and I stumbled upon a very strange ring which is Z/6Z, and the equally strange (Z/6Z)[X], and now I have a conjecture:

Conjecture: there are no irreducible elements in (Z/6Z)[X]

is this true?

[Kenny Lau]

import Mathlib

open Polynomial

theorem not_irreducible_of_polynomial_zmod_6
    (p : (ZMod 6)[X]) : ¬ Irreducible p := by
  sorry

[Kevin Buzzard]

This ring is presumably just a product of the rings $\Z/2[X]$ and $\Z/3[X]$ so one could ask the more general question about a product of two PIDs. Is (irreducible,1) irreducible in such a thing? Sounds to me like it might be, so maybe I'm suggesting $1+2X$ as a counterexample?

[Kenny Lau]

that makes sense, i think that works

[Aaron Liu]

Tactic `decide` proved that the proposition
  ∀ (a b c d : ZMod 6), a * c = 0 → b * d = 1 → a * d + b * c = 2 → False
is false

[Kenny Lau]

well but the factors could be quadratic

[Kenny Lau]

e.g. (2x+3)(3x+2) = x

[Aaron Liu]

no that's not what I mean

[Kenny Lau]

also irreducible doesn't mean no factorisation exists, it means that if it factorises as ab then a or b must be unit

[Aaron Liu]

oh I guess I forgot to clean out the units

[Aaron Liu]

ok the factors can't both be linear

[Aaron Liu]

they also can't both be quadratic

[Aaron Liu]

probably convinced now

[Junyan Xu]

Is (irreducible,1) irreducible in such a thing?

This is proven here.