Library mathcomp.field.qfpoly
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.
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 explicitely.
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.
Canonical qfpoly_eqType := [eqType of {poly %/ h with hI}].
Canonical qfpoly_choiceType := [choiceType of {poly %/ h with hI}].
Canonical qfpoly_zmodType := [zmodType of {poly %/ h with hI}].
Canonical qfpoly_ringType := [ringType of {poly %/ h with hI}].
End iDomain.
Section finIDomain.
Variable R : finIdomainType.
Variable h : {poly R}.
Hypothesis hI : monic_irreducible_poly h.
Canonical qfpoly_finZmodType := [finZmodType of {poly %/ h with hI}].
Canonical qfpoly_finRingType := [finRingType of {poly %/ h with hI}].
End finIDomain.
Section Field.
Variable R : fieldType.
Variable h : {poly R}.
Local Notation hQ := (mk_monic h).
Hypothesis hI : monic_irreducible_poly h.
Canonical qfpoly_unitRingType := [unitRingType of {poly %/ h with hI}].
Canonical qfpoly_comRingType := [comRingType of {poly %/ h with hI}].
Canonical qfpoly_comUnitRingType := [comUnitRingType of {poly %/ h with hI}].
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}.
Definition qpoly_fieldUnitMixin := FieldUnitMixin qpoly_mulVp qpoly_inv0.
Lemma qpoly_fieldMixin : GRing.Field.mixin_of [unitRingType of {poly %/ h}].
Definition qpoly_fieldIdomainMixin := FieldIdomainMixin qpoly_fieldMixin.
Canonical qpoly_idomainType :=
Eval hnf in IdomainType {poly %/ h with hI} qpoly_fieldIdomainMixin.
Canonical qpoly_fieldType :=
Eval hnf in FieldType {poly %/ h with hI} qpoly_fieldMixin.
Canonical qpoly_unitAlgType :=
Eval hnf in [unitAlgType R of {poly %/ h with hI}].
Canonical qpoly_falgType := [FalgType R of {poly %/ h with hI}].
Canonical qpoly_fieldExtType := [fieldExtType R of {poly %/ h with hI}].
End Field.
Section FinField.
Variable R : finFieldType.
Variable h : {poly R}.
Local Notation hQ := (mk_monic h).
Canonical qpoly_finUnitRingType :=
Eval hnf in [finUnitRingType of {poly %/ h}].
Canonical qpoly_finComUnitRingType :=
Eval hnf in [finComUnitRingType of {poly %/ h}].
Hypothesis hI : monic_irreducible_poly h.
Canonical qfpoly_finUnitRingType :=
Eval hnf in [finUnitRingType of {poly %/ h with hI}].
Canonical qfpoly_finComRingType :=
Eval hnf in [comRingType of {poly %/ h with hI}].
Canonical qfpoly_finComUnitRingType :=
Eval hnf in [comUnitRingType of {poly %/ h with hI}].
Canonical qpoly_finIdomainType :=
Eval hnf in [finIdomainType of {poly %/ h with hI}].
Canonical qpoly_finFieldType :=
Eval hnf in [finFieldType of {poly %/ h with hI}].
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.