Library mathcomp.field.qfpoly
From HB Require Import structures.
From mathcomp
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.
From mathcomp
Require Import div bigop binomial finset finfun ssralg countalg finalg.
From mathcomp
Require Import poly polydiv qpoly perm fingroup falgebra fieldext finfield
galois.
From mathcomp
Require Import finalg zmodp matrix vector.
From mathcomp
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.
From mathcomp
Require Import div bigop binomial finset finfun ssralg countalg finalg.
From mathcomp
Require Import poly polydiv qpoly perm fingroup falgebra fieldext finfield
galois.
From mathcomp
Require Import finalg zmodp matrix vector.
This file extends the algebras R[X]/<p> defined in qpoly with the field
when p is irreducible
It defines the new field on top of {qpoly p}. As irreducible is in general
decidable in general, this is done by giving a proof explicitly.
monic_irreducible_poly p == proof that p is monic and irreducible
{poly %/ p with mi} == defined as {poly %/ p} where mi is proof of
monic_irreducible_poly p
It also defines the discrete logarithm with a primitive polynomial on a
finite field
primitive_poly p == p is a primitive polynomial
qlogp q == is the discrete log of q where q is an element of
the quotient field with respect to a primitive
polynomial p
plogp p q == is the discrete log of q with respect to p in {poly F}
this makes only sense if p is a primitive polynomial of
size > 2
Set Implicit Arguments.
Import GRing.Theory.
Import Pdiv.CommonRing.
Import Pdiv.RingMonic.
Import Pdiv.Field.
Import FinRing.Theory.
Local Open Scope ring_scope.
Reserved Notation "{ 'poly' '%/' p 'with' mi }"
(at level 0, p at level 2, mi at level 10,
format "{ 'poly' '%/' p 'with' mi }").
Section DomainDef.
Variable R : idomainType.
Variable h : {poly R}.
Definition monic_irreducible_poly (p : {poly R}) :=
((irreducible_poly p) × (p \is monic))%type.
Hypothesis hI : monic_irreducible_poly h.
Definition qfpoly : monic_irreducible_poly h → predArgType :=
fun⇒ {poly %/ h}.
End DomainDef.
Notation "{ 'poly' '%/' p 'with' hi }" := (@qfpoly _ p hi).
Section iDomain.
Variable R : idomainType.
Variable h : {poly R}.
Hypothesis hI : monic_irreducible_poly h.
End iDomain.
Section finIDomain.
Variable R : finIdomainType.
Variable h : {poly R}.
Hypothesis hI : monic_irreducible_poly h.
End finIDomain.
Section Field.
Variable R : fieldType.
Variable h : {poly R}.
Local Notation hQ := (mk_monic h).
Hypothesis hI : monic_irreducible_poly h.
Lemma mk_monicE : mk_monic h = h.
Lemma coprimep_unit (p : {poly %/ h}) : p != 0%R → coprimep hQ p.
Lemma qpoly_mulVp (p : {poly %/ h}) : p != 0%R → (qpoly_inv p × p = 1)%R.
Lemma qpoly_inv0 : qpoly_inv 0%R = 0%R :> {poly %/ h}.
End Field.
Section FinField.
Variable R : finFieldType.
Variable h : {poly R}.
Local Notation hQ := (mk_monic h).
Hypothesis hI : monic_irreducible_poly h.
Lemma card_qfpoly : #|{poly %/ h with hI}| = #|R| ^ (size h).-1.
Lemma card_qfpoly_gt1 : 1 < #|{poly %/ h with hI}|.
End FinField.
Section inPoly.
Variable R : comRingType.
Variable h : {poly R}.
Lemma in_qpoly_comp_horner (p q : {poly R}) :
in_qpoly h (p \Po q) =
(map_poly (qpolyC h) p).[in_qpoly h q].
Lemma map_poly_div_inj : injective (map_poly (qpolyC h)).
End inPoly.
Section finPoly.
Unfortunately we need some duplications so inference
propagates qfpoly :-( )
Definition qfpoly_const (R : idomainType) (h : {poly R})
(hMI : monic_irreducible_poly h) : R → {poly %/ h with hMI} :=
qpolyC h.
Lemma map_fpoly_div_inj (R : idomainType) (h : {poly R})
(hMI : monic_irreducible_poly h) :
injective (map_poly (qfpoly_const hMI)).
End finPoly.
Section Splitting.
Variable F : finFieldType.
Variable h : {poly F}.
Hypothesis hI : monic_irreducible_poly h.
Definition qfpoly_splitting_field_type :=
FinSplittingFieldType F {poly %/ h with hI}.
End Splitting.
Section PrimitivePoly.
Variable F : finFieldType.
Variable h : {poly F}.
Hypothesis sh_gt2 : 2 < size h.
Let sh_gt1 : 1 < size h.
Definition primitive_poly (p: {poly F}) :=
let v := #|{poly %/ p}|.-1 in
[&& p \is monic,
irreducibleb p,
p %| 'X^v - 1 &
[∀ n : 'I_v, (p %| 'X^n - 1) ==> (n == 0%N :> nat)]].
Lemma primitive_polyP (p : {poly F}) :
reflect
(let v := #|{poly %/ p}|.-1 in
[/\ monic_irreducible_poly p,
p %| 'X^v - 1 &
∀ n, 0 < n < v → ~~ (p %| 'X^n - 1)])
(primitive_poly p).
Hypothesis Hh : primitive_poly h.
Lemma primitive_mi : monic_irreducible_poly h.
Lemma primitive_poly_in_qpoly_eq0 p : (in_qpoly h p == 0) = (h %| p).
Local Notation qT := {poly %/ h with primitive_mi}.
Lemma card_primitive_qpoly : #|{poly %/ h}|= #|F| ^ (size h).-1.
Lemma qX_neq0 : 'qX != 0 :> qT.
Lemma qX_in_unit : ('qX : qT) \in GRing.unit.
Definition gX : {unit qT} := FinRing.unit _ qX_in_unit.
Lemma dvdp_order n : (h %| 'X^n - 1) = (gX ^+ n == 1)%g.
Lemma gX_order : #[gX]%g = (#|qT|).-1.
Lemma gX_all : <[gX]>%g = [set: {unit qT}]%G.
Let pred_card_qT_gt0 : 0 < #|qT|.-1.
Definition qlogp (p : qT) : nat :=
odflt (Ordinal pred_card_qT_gt0) (pick [pred i in 'I_ _ | ('qX ^+ i == p)]).
Lemma qlogp_lt p : qlogp p < #|qT|.-1.
Lemma qlogp_qX (p : qT) : p != 0 → 'qX ^+ (qlogp p) = p.
Lemma qX_order_card : 'qX ^+ (#|qT|).-1 = 1 :> qT.
Lemma qX_order_dvd (i : nat) : 'qX ^+ i = 1 :> qT → (#|qT|.-1 %| i)%N.
Lemma qlogp0 : qlogp 0 = 0%N.
Lemma qlogp1 : qlogp 1 = 0%N.
Lemma qlogp_eq0 (q : qT) : (qlogp q == 0%N) = (q == 0) || (q == 1).
Lemma qX_exp_neq0 i : 'qX ^+ i != 0 :> qT.
Lemma qX_exp_inj i j :
i < #|qT|.-1 → j < #|qT|.-1 → 'qX ^+ i = 'qX ^+ j :> qT → i = j.
Lemma powX_eq_mod i j : i = j %[mod #|qT|.-1] → 'qX ^+ i = 'qX ^+ j :> qT.
Lemma qX_expK i : i < #|qT|.-1 → qlogp ('qX ^+ i) = i.
Lemma qlogpD (q1 q2 : qT) :
q1 != 0 → q2 != 0 →qlogp (q1 × q2) = ((qlogp q1 + qlogp q2) %% #|qT|.-1)%N.
End PrimitivePoly.
Section Plogp.
Variable F : finFieldType.
Definition plogp (p q : {poly F}) :=
if boolP (primitive_poly p) is AltTrue Hh then
qlogp ((in_qpoly p q) : {poly %/ p with primitive_mi Hh})
else 0%N.
Lemma plogp_lt (p q : {poly F}) : 2 < size p → plogp p q < #|{poly %/ p}|.-1.
Lemma plogp_X (p q : {poly F}) :
2 < size p → primitive_poly p → ~~ (p %| q) → p %| q - 'X ^+ plogp p q.
Lemma plogp0 (p : {poly F}) : 2 < size p → plogp p 0 = 0%N.
Lemma plogp1 (p : {poly F}) : 2 < size p → plogp p 1 = 0%N.
Lemma plogp_div_eq0 (p q : {poly F}) :
2 < size p → (p %| q) → plogp p q = 0%N.
Lemma plogpD (p q1 q2 : {poly F}) :
2 < size p → primitive_poly p → ~~ (p %| q1) → ~~ (p %| q2) →
plogp p (q1 × q2) = ((plogp p q1 + plogp p q2) %% #|{poly %/ p}|.-1)%N.
End Plogp.
(hMI : monic_irreducible_poly h) : R → {poly %/ h with hMI} :=
qpolyC h.
Lemma map_fpoly_div_inj (R : idomainType) (h : {poly R})
(hMI : monic_irreducible_poly h) :
injective (map_poly (qfpoly_const hMI)).
End finPoly.
Section Splitting.
Variable F : finFieldType.
Variable h : {poly F}.
Hypothesis hI : monic_irreducible_poly h.
Definition qfpoly_splitting_field_type :=
FinSplittingFieldType F {poly %/ h with hI}.
End Splitting.
Section PrimitivePoly.
Variable F : finFieldType.
Variable h : {poly F}.
Hypothesis sh_gt2 : 2 < size h.
Let sh_gt1 : 1 < size h.
Definition primitive_poly (p: {poly F}) :=
let v := #|{poly %/ p}|.-1 in
[&& p \is monic,
irreducibleb p,
p %| 'X^v - 1 &
[∀ n : 'I_v, (p %| 'X^n - 1) ==> (n == 0%N :> nat)]].
Lemma primitive_polyP (p : {poly F}) :
reflect
(let v := #|{poly %/ p}|.-1 in
[/\ monic_irreducible_poly p,
p %| 'X^v - 1 &
∀ n, 0 < n < v → ~~ (p %| 'X^n - 1)])
(primitive_poly p).
Hypothesis Hh : primitive_poly h.
Lemma primitive_mi : monic_irreducible_poly h.
Lemma primitive_poly_in_qpoly_eq0 p : (in_qpoly h p == 0) = (h %| p).
Local Notation qT := {poly %/ h with primitive_mi}.
Lemma card_primitive_qpoly : #|{poly %/ h}|= #|F| ^ (size h).-1.
Lemma qX_neq0 : 'qX != 0 :> qT.
Lemma qX_in_unit : ('qX : qT) \in GRing.unit.
Definition gX : {unit qT} := FinRing.unit _ qX_in_unit.
Lemma dvdp_order n : (h %| 'X^n - 1) = (gX ^+ n == 1)%g.
Lemma gX_order : #[gX]%g = (#|qT|).-1.
Lemma gX_all : <[gX]>%g = [set: {unit qT}]%G.
Let pred_card_qT_gt0 : 0 < #|qT|.-1.
Definition qlogp (p : qT) : nat :=
odflt (Ordinal pred_card_qT_gt0) (pick [pred i in 'I_ _ | ('qX ^+ i == p)]).
Lemma qlogp_lt p : qlogp p < #|qT|.-1.
Lemma qlogp_qX (p : qT) : p != 0 → 'qX ^+ (qlogp p) = p.
Lemma qX_order_card : 'qX ^+ (#|qT|).-1 = 1 :> qT.
Lemma qX_order_dvd (i : nat) : 'qX ^+ i = 1 :> qT → (#|qT|.-1 %| i)%N.
Lemma qlogp0 : qlogp 0 = 0%N.
Lemma qlogp1 : qlogp 1 = 0%N.
Lemma qlogp_eq0 (q : qT) : (qlogp q == 0%N) = (q == 0) || (q == 1).
Lemma qX_exp_neq0 i : 'qX ^+ i != 0 :> qT.
Lemma qX_exp_inj i j :
i < #|qT|.-1 → j < #|qT|.-1 → 'qX ^+ i = 'qX ^+ j :> qT → i = j.
Lemma powX_eq_mod i j : i = j %[mod #|qT|.-1] → 'qX ^+ i = 'qX ^+ j :> qT.
Lemma qX_expK i : i < #|qT|.-1 → qlogp ('qX ^+ i) = i.
Lemma qlogpD (q1 q2 : qT) :
q1 != 0 → q2 != 0 →qlogp (q1 × q2) = ((qlogp q1 + qlogp q2) %% #|qT|.-1)%N.
End PrimitivePoly.
Section Plogp.
Variable F : finFieldType.
Definition plogp (p q : {poly F}) :=
if boolP (primitive_poly p) is AltTrue Hh then
qlogp ((in_qpoly p q) : {poly %/ p with primitive_mi Hh})
else 0%N.
Lemma plogp_lt (p q : {poly F}) : 2 < size p → plogp p q < #|{poly %/ p}|.-1.
Lemma plogp_X (p q : {poly F}) :
2 < size p → primitive_poly p → ~~ (p %| q) → p %| q - 'X ^+ plogp p q.
Lemma plogp0 (p : {poly F}) : 2 < size p → plogp p 0 = 0%N.
Lemma plogp1 (p : {poly F}) : 2 < size p → plogp p 1 = 0%N.
Lemma plogp_div_eq0 (p q : {poly F}) :
2 < size p → (p %| q) → plogp p q = 0%N.
Lemma plogpD (p q1 q2 : {poly F}) :
2 < size p → primitive_poly p → ~~ (p %| q1) → ~~ (p %| q2) →
plogp p (q1 × q2) = ((plogp p q1 + plogp p q2) %% #|{poly %/ p}|.-1)%N.
End Plogp.