An irreducibility criterion
Let p be a (positive) prime number. Our goal is to prove that if an integer polynomial is irreducible over the prime field Fp, then it is irreducible over Z.Definition zx := (cpoly_cring Z_as_CRing).
Definition fpx := (cpoly_cring fp).
Fixpoint zxfpx (p:zx) : fpx :=
match p with
| cpoly_zero => (cpoly_zero fp : fpx)
| cpoly_linear c p1 => (zfp c)[+X*](zxfpx p1)
end.
Definition P (f g:zx):= f[=]g -> (zxfpx f)[=](zxfpx g).
Lemma fpxeq_wd : forall f g:zx, f[=]g -> (zxfpx f)[=](zxfpx g).
Lemmas
In this section we prove the lemmas we will need, about integer polynomials, viewed over a prime field.Lemma mult_zero : forall (R:CRing)(f:cpoly_cring R),
(cpoly_mult_op R f (cpoly_zero R))[=](cpoly_zero R).
Lemma fp_resp_zero : zxfpx(cpoly_zero Z_as_CRing)[=](cpoly_zero fp).
Lemma fpx_resp_mult_cr : forall (c:Z_as_CRing)(f:zx),
(cpoly_mult_cr_cs fp (zxfpx f) (zfp c)) [=]
(zxfpx (cpoly_mult_cr_cs _ f c)).
Lemma fpx_resp_plus : forall f g:zx,
(cpoly_plus_op fp (zxfpx f) (zxfpx g))[=]
(zxfpx (cpoly_plus_op _ f g)).
Lemma fpx_resp_mult : forall f g:zx,
(cpoly_mult_op fp (zxfpx f) (zxfpx g)) [=]
(zxfpx (cpoly_mult_op _ f g)).
Lemma fpx_resp_coef : forall (f:zx)(n:nat), (zfp (nth_coeff n f))
[=] (nth_coeff n (zxfpx f)).
Working towards the criterion
Definitions
We prove the criterion for monic integers of degree greater than 1. This property is first defined, so that reducibility can be defined next. We then prove that a reducible integer polynomial is reducible over Fp. Finally irreducibility is defined.Definition degree_ge_monic (R:CRing)(n:nat)(f:(cpoly_cring R)) :=
{m:nat | (n >= m)%nat | monic m f}.
Lemma fpx_resp_deggemonic : forall (f:zx)(n:nat),
degree_ge_monic _ n f -> degree_ge_monic _ n (zxfpx f).
Definition reducible (R:CRing)(f:(cpoly_cring R)) :=
degree_ge_monic R 2%nat f and
{g:(cpoly_cring R) | degree_ge_monic R 1%nat g |
{h:(cpoly_cring R) | degree_ge_monic R 1%nat h |
f[=](cpoly_mult_op R g h) }}.
Lemma fpx_resp_red : forall f:zx, (reducible _ f)->(reducible fp (zxfpx f)).
Definition irreducible (R:CRing)(f:(cpoly_cring R)) :=
~ (reducible R f).