Library mathcomp.algebra.qpoly
From mathcomp
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.
From mathcomp
Require Import bigop binomial finset finfun ssralg countalg finalg poly polydiv.
From mathcomp
Require Import perm fingroup matrix mxalgebra mxpoly vector countalg.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.
From mathcomp
Require Import bigop binomial finset finfun ssralg countalg finalg poly polydiv.
From mathcomp
Require Import perm fingroup matrix mxalgebra mxpoly vector countalg.
This file defines the algebras R[X]/<p> and their theory.
It mimics the zmod file for polynomials
First, it defines polynomials of bounded size (equivalent of 'I_n),
gives it a structure of choice, finite and countable ring, ..., and
lmodule, when possible.
Internally, the construction uses poly_rV and rVpoly, but they should not
be exposed.
We provide two bases: the 'X^i and the lagrange polynomials.
{poly_n R} == the type of polynomial of size at most n
irreducibleb p == boolean decision procedure for irreducibility
of a bounded size polynomial over a finite idomain
Considering {poly_n F} over a field F, it is a vectType and
'nX^i == 'X^i as an element of {poly_n R}
polynX == [tuple 'X^0, ..., 'X^(n - 1) ], basis of {poly_n R}
x.-lagrange == lagrange basis of {poly_n R} wrt x : nat -> F
x.-lagrange_ i == the ith lagrange polynomial wrt the sampling points x
Second, it defines polynomials quotiented by a poly (equivalent of 'Z_p),
as bounded polynomial. As we are aiming to build a ring structure we need
the polynomial to be monic and of size greater than one. If it is not the
case we quotient by 'X
mk_monic p == the actual polynomial on which we quotient
if p is monic and dof size > 1 it is p otherwise 'X
{poly %/ p} == defined as {poly_(size (mk_poly p)).-1 R} on which
there is a ring structure
in_qpoly q == turn the polynomial q into an element of {poly %/ p} by
taking a modulo
'qX == in_qpoly 'X
The last part that defines the field structure when the quotient is an
irreducible polynomial is defined in field/qfpoly
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_' n R }"
(at level 0, n at level 2, format "'{poly_' n R }").
Reserved Notation "''nX^' i" (at level 3, i at level 2, format "''nX^' i").
Reserved Notation "x .-lagrange" (at level 2, format "x .-lagrange").
Reserved Notation "x .-lagrange_" (at level 2, format "x .-lagrange_").
Reserved Notation "'qX" (at level 0).
Reserved Notation "{ 'poly' '%/' p }"
(at level 0, p at level 2, format "{ 'poly' '%/' p }").
Section poly_of_size_zmod.
Context {R : ringType}.
Implicit Types (phR : phant R) (n : nat).
Section poly_of_size.
Variable (n : nat).
Definition poly_of_size :=
[qualify a p | size (p : {poly R}) ≤ n].
Fact poly_of_size_key : pred_key poly_of_size.
Canonical poly_of_size_keyd := KeyedQualifier poly_of_size_key.
Lemma npoly_submod_closed : submod_closed poly_of_size.
Canonical npoly_opprPred := OpprPred npoly_submod_closed.
Canonical npoly_addrPred := AddrPred npoly_submod_closed.
Canonical npoly_zmodPred := ZmodPred npoly_submod_closed.
Canonical npoly_submodPred := SubmodPred npoly_submod_closed.
End poly_of_size.
Section npoly.
Record npoly_of phR n : predArgType := NPoly_of {
polyn :> {poly R};
_ : polyn \is a poly_of_size n
}.
Variable (n : nat).
Local Notation "'{poly_' n R }" := (@npoly_of (Phant R) n).
Canonical npoly_subType := [subType for @polyn (Phant R) n].
Lemma npoly_is_a_poly_of_size (p : {poly_n R}) : val p \is a poly_of_size n.
Hint Resolve npoly_is_a_poly_of_size : core.
Lemma size_npoly (p : {poly_n R}) : size p ≤ n.
Hint Resolve size_npoly : core.
Definition npoly_eqMixin := [eqMixin of {poly_n R} by <:].
Canonical npoly_eqType := EqType {poly_n R} npoly_eqMixin.
Definition npoly_choiceMixin := [choiceMixin of {poly_n R} by <:].
Canonical npoly_choiceType := ChoiceType {poly_n R} npoly_choiceMixin.
Definition npoly_zmodMixin := [zmodMixin of {poly_n R} by <:].
Canonical npoly_zmodType := ZmodType {poly_n R} npoly_zmodMixin.
Definition npoly_lmodMixin := [lmodMixin of {poly_n R} by <:].
Canonical npoly_lmodType := LmodType R {poly_n R} npoly_lmodMixin.
Definition npoly_rV : {poly_n R} → 'rV[R]_n := poly_rV \o val.
Definition rVnpoly : 'rV[R]_n → {poly_n R} :=
insubd (0 : {poly_n R}) \o rVpoly.
Arguments rVnpoly /.
Arguments npoly_rV /.
Lemma npoly_rV_K : cancel npoly_rV rVnpoly.
Lemma rVnpolyK : cancel rVnpoly npoly_rV.
Hint Resolve npoly_rV_K rVnpolyK : core.
Lemma npoly_vect_axiom : Vector.axiom n {poly_n R}.
Definition npoly_vect_mixin := VectMixin npoly_vect_axiom.
Canonical npoly_vect_type := VectType R {poly_n R} npoly_vect_mixin.
End npoly.
End poly_of_size_zmod.
Notation "'{poly_' n R }" := (npoly_of (Phant R) n) : type_scope.
Notation NPoly := (NPoly_of (Phant _)).
#[global]
Hint Resolve size_npoly npoly_is_a_poly_of_size : core.
Definition npoly_countMixin (R : countRingType) n :=
[countMixin of {poly_n R} by <:].
Canonical npoly_countType (R : countRingType) n :=
CountType {poly_n R} (@npoly_countMixin R n).
Canonical npoly_subCountType (R : countRingType) n :=
[subCountType of {poly_n R}].
Section npoly_fin.
Variable (R : finRingType) (n : nat).
Definition npoly_finMixin (R : finRingType) (n : nat) :=
CanFinMixin (@npoly_rV_K [ringType of R] n).
Canonical npoly_finType (R : finRingType) n :=
FinType {poly_n R} (@npoly_finMixin R n).
Canonical npoly_subFinType := [subFinType of {poly_n R}].
End npoly_fin.
Section npoly_theory.
Context (R : ringType) {n : nat}.
Lemma polyn_is_linear : linear (@polyn _ _ _ : {poly_n R} → _).
Canonical polyn_additive := Additive polyn_is_linear.
Canonical polyn_linear := Linear polyn_is_linear.
Canonical npoly (E : nat → R) : {poly_n R} :=
@NPoly_of _ (Phant R) _ (\poly_(i < n) E i) (size_poly _ _).
Fact size_npoly0 : size (0 : {poly R}) ≤ n.
Definition npoly0 := NPoly (size_npoly0).
Fact npolyp_key : unit.
Definition npolyp : {poly R} → {poly_n R} :=
locked_with npolyp_key (npoly \o (nth 0)).
Definition npoly_of_seq := npolyp \o Poly.
Lemma npolyP (p q : {poly_n R}) : nth 0 p =1 nth 0 q ↔ p = q.
Lemma coef_npolyp (p : {poly R}) i : (npolyp p)`_i = if i < n then p`_i else 0.
Lemma big_coef_npoly (p : {poly_n R}) i : n ≤ i → p`_i = 0.
Lemma npolypK (p : {poly R}) : size p ≤ n → npolyp p = p :> {poly R}.
Lemma coefn_sum (I : Type) (r : seq I) (P : pred I)
(F : I → {poly_n R}) (k : nat) :
(\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k.
End npoly_theory.
Arguments npoly {R} n E.
Arguments npolyp {R} n p.
Section fin_npoly.
Variable R : finRingType.
Variable n : nat.
Implicit Types p q : {poly_n R}.
Definition npoly_enum : seq {poly_n R} :=
if n isn't n.+1 then [:: npoly0 _] else
pmap insub [seq \poly_(i < n.+1) c (inord i) | c : (R ^ n.+1)%type].
Lemma npoly_enum_uniq : uniq npoly_enum.
Lemma mem_npoly_enum p : p \in npoly_enum.
Lemma card_npoly : #|{poly_n R}| = (#|R| ^ n)%N.
End fin_npoly.
Section Irreducible.
Variable R : finIdomainType.
Variable p : {poly R}.
Definition irreducibleb :=
((1 < size p) &&
[∀ q : {poly_((size p).-1) R},
(Pdiv.Ring.rdvdp q p)%R ==> (size q ≤ 1)])%N.
Lemma irreducibleP : reflect (irreducible_poly p) irreducibleb.
End Irreducible.
Section Vspace.
Variable (K : fieldType) (n : nat).
Lemma dim_polyn : \dim (fullv : {vspace {poly_n K}}) = n.
Definition npolyX : n.-tuple {poly_n K} := [tuple npolyp n 'X^i | i < n].
Notation "''nX^' i" := (tnth npolyX i).
Lemma npolyXE (i : 'I_n) : 'nX^i = 'X^i :> {poly _}.
Lemma nth_npolyX (i : 'I_n) : npolyX`_i = 'nX^i.
Lemma npolyX_free : free npolyX.
Lemma npolyX_full : basis_of fullv npolyX.
Lemma npolyX_coords (p : {poly_n K}) i : coord npolyX i p = p`_i.
Lemma npolyX_gen (p : {poly K}) : (size p ≤ n)%N →
p = \sum_(i < n) p`_i *: 'nX^i.
Section lagrange.
Variables (x : nat → K).
Notation lagrange_def := (fun i :'I_n ⇒
let k := i in let p := \prod_(j < n | j != k) ('X - (x j)%:P)
in (p.[x k]^-1)%:P × p).
Fact lagrange_key : unit.
Definition lagrange := locked_with lagrange_key
[tuple npolyp n (lagrange_def i) | i < n].
Notation lagrange_ := (tnth lagrange).
Hypothesis n_gt0 : (0 < n)%N.
Hypothesis x_inj : injective x.
Let lagrange_def_sample (i j : 'I_n) : (lagrange_def i).[x j] = (i == j)%:R.
Let size_lagrange_def i : size (lagrange_def i) = n.
Lemma lagrangeE i : lagrange_ i = lagrange_def i :> {poly _}.
Lemma nth_lagrange (i : 'I_n) : lagrange`_i = lagrange_ i.
Lemma size_lagrange_ i : size (lagrange_ i) = n.
Lemma size_lagrange : size lagrange = n.
Lemma lagrange_sample (i j : 'I_n) : (lagrange_ i).[x j] = (i == j)%:R.
Lemma lagrange_free : free lagrange.
Lemma lagrange_full : basis_of fullv lagrange.
Lemma lagrange_coords (p : {poly_n K}) i : coord lagrange i p = p.[x i].
Lemma lagrange_gen (p : {poly K}) : (size p ≤ n)%N →
p = \sum_(i < n) p.[x i]%:P × lagrange_ i.
End lagrange.
End Vspace.
Notation "''nX^' i" := (tnth (npolyX _) i) : ring_scope.
Notation "x .-lagrange" := (lagrange x) : ring_scope.
Notation "x .-lagrange_" := (tnth x.-lagrange) : ring_scope.
Section Qpoly.
Variable R : ringType.
Variable h : {poly R}.
Definition mk_monic :=
if (1 < size h)%N && (h \is monic) then h else 'X.
Definition qpoly := {poly_(size mk_monic).-1 R}.
End Qpoly.
Notation "{ 'poly' '%/' p }" := (qpoly p) : type_scope.
Section QpolyProp.
Variable R : ringType.
Variable h : {poly R}.
Lemma monic_mk_monic : (mk_monic h) \is monic.
Lemma size_mk_monic_gt1 : (1 < size (mk_monic h))%N.
Lemma size_mk_monic_gt0 : (0 < size (mk_monic h))%N.
Lemma mk_monic_neq0 : mk_monic h != 0.
Lemma size_mk_monic (p : {poly %/ h}) : size p < size (mk_monic h).
standard inject
Lemma poly_of_size_mod p :
rmodp p (mk_monic h) \is a poly_of_size (size (mk_monic h)).-1.
Definition in_qpoly p : {poly %/ h} := NPoly_of _ (poly_of_size_mod p).
Lemma in_qpoly_small (p : {poly R}) :
size p < size (mk_monic h) → in_qpoly p = p :> {poly R}.
Lemma in_qpoly0 : in_qpoly 0 = 0.
Lemma in_qpolyD p q : in_qpoly (p + q) = in_qpoly p + in_qpoly q.
Lemma in_qpolyZ a p : in_qpoly (a *: p) = a *: in_qpoly p.
Fact in_qpoly_is_linear : linear in_qpoly.
Canonical in_qpoly_additive := Additive in_qpoly_is_linear.
Canonical in_qpoly_linear := Linear in_qpoly_is_linear.
Lemma qpolyC_proof k :
(k%:P : {poly R}) \is a poly_of_size (size (mk_monic h)).-1.
Definition qpolyC k : {poly %/ h} := NPoly_of _ (qpolyC_proof k).
Lemma qpolyCE k : qpolyC k = k%:P :> {poly R}.
Lemma qpolyC0 : qpolyC 0 = 0.
Definition qpoly1 := qpolyC 1.
Definition qpoly_mul (q1 q2 : {poly %/ h}) : {poly %/ h} :=
in_qpoly ((q1 : {poly R}) × q2).
Lemma qpoly_mul1z : left_id qpoly1 qpoly_mul.
Lemma qpoly_mulz1 : right_id qpoly1 qpoly_mul.
Lemma qpoly_nontrivial : qpoly1 != 0.
Definition qpolyX := in_qpoly 'X.
Notation "'qX" := qpolyX.
Lemma qpolyXE : 2 < size h → h \is monic → 'qX = 'X :> {poly R}.
End QpolyProp.
Notation "'qX" := (qpolyX _) : ring_scope.
Lemma mk_monic_X (R : ringType) : mk_monic 'X = 'X :> {poly R}.
Lemma mk_monic_Xn (R : ringType) n : mk_monic 'X^n = 'X^n.-1.+1 :> {poly R}.
Lemma card_qpoly (R : finRingType) (h : {poly R}):
#|{poly %/ h}| = #|R| ^ (size (mk_monic h)).-1.
Lemma card_monic_qpoly (R : finRingType) (h : {poly R}):
1 < size h → h \is monic → #|{poly %/ h}| = #|R| ^ (size h).-1.
Section QRing.
Variable A : comRingType.
Variable h : {poly A}.
rmodp p (mk_monic h) \is a poly_of_size (size (mk_monic h)).-1.
Definition in_qpoly p : {poly %/ h} := NPoly_of _ (poly_of_size_mod p).
Lemma in_qpoly_small (p : {poly R}) :
size p < size (mk_monic h) → in_qpoly p = p :> {poly R}.
Lemma in_qpoly0 : in_qpoly 0 = 0.
Lemma in_qpolyD p q : in_qpoly (p + q) = in_qpoly p + in_qpoly q.
Lemma in_qpolyZ a p : in_qpoly (a *: p) = a *: in_qpoly p.
Fact in_qpoly_is_linear : linear in_qpoly.
Canonical in_qpoly_additive := Additive in_qpoly_is_linear.
Canonical in_qpoly_linear := Linear in_qpoly_is_linear.
Lemma qpolyC_proof k :
(k%:P : {poly R}) \is a poly_of_size (size (mk_monic h)).-1.
Definition qpolyC k : {poly %/ h} := NPoly_of _ (qpolyC_proof k).
Lemma qpolyCE k : qpolyC k = k%:P :> {poly R}.
Lemma qpolyC0 : qpolyC 0 = 0.
Definition qpoly1 := qpolyC 1.
Definition qpoly_mul (q1 q2 : {poly %/ h}) : {poly %/ h} :=
in_qpoly ((q1 : {poly R}) × q2).
Lemma qpoly_mul1z : left_id qpoly1 qpoly_mul.
Lemma qpoly_mulz1 : right_id qpoly1 qpoly_mul.
Lemma qpoly_nontrivial : qpoly1 != 0.
Definition qpolyX := in_qpoly 'X.
Notation "'qX" := qpolyX.
Lemma qpolyXE : 2 < size h → h \is monic → 'qX = 'X :> {poly R}.
End QpolyProp.
Notation "'qX" := (qpolyX _) : ring_scope.
Lemma mk_monic_X (R : ringType) : mk_monic 'X = 'X :> {poly R}.
Lemma mk_monic_Xn (R : ringType) n : mk_monic 'X^n = 'X^n.-1.+1 :> {poly R}.
Lemma card_qpoly (R : finRingType) (h : {poly R}):
#|{poly %/ h}| = #|R| ^ (size (mk_monic h)).-1.
Lemma card_monic_qpoly (R : finRingType) (h : {poly R}):
1 < size h → h \is monic → #|{poly %/ h}| = #|R| ^ (size h).-1.
Section QRing.
Variable A : comRingType.
Variable h : {poly A}.
Ring operations
Lemma qpoly_mulC : commutative (@qpoly_mul A h).
Lemma qpoly_mulA : associative (@qpoly_mul A h).
Lemma qpoly_mul_addr : right_distributive (@qpoly_mul A h) +%R.
Lemma qpoly_mul_addl : left_distributive (@qpoly_mul A h) +%R.
Definition qpoly_ringMixin :=
ComRingMixin qpoly_mulA qpoly_mulC (@qpoly_mul1z _ h) qpoly_mul_addl
(@qpoly_nontrivial _ h).
Canonical qpoly_ringType := Eval hnf in RingType {poly %/ h} qpoly_ringMixin.
Canonical npoly_ringType := Eval hnf in RingType {poly_ _ A} qpoly_ringMixin.
Canonical qpoly_comRingType := Eval hnf in ComRingType {poly %/ h} qpoly_mulC.
Canonical npoly_comRingType := Eval hnf in ComRingType {poly_ _ A} qpoly_mulC.
Lemma in_qpoly1 : in_qpoly h 1 = 1.
Lemma in_qpolyM q1 q2 : in_qpoly h (q1 × q2) = in_qpoly h q1 × in_qpoly h q2.
Fact in_qpoly_multiplicative : multiplicative (in_qpoly h).
Canonical in_qpoly_rmorphism := AddRMorphism in_qpoly_multiplicative.
Lemma poly_of_qpoly_sum I (r : seq I) (P1 : pred I) (F : I → {poly %/ h}) :
((\sum_(i <- r | P1 i) F i) =
\sum_(p <- r | P1 p) ((F p) : {poly A}) :> {poly A})%R.
Lemma poly_of_qpolyD (p q : {poly %/ h}) :
p + q= (p : {poly A}) + q :> {poly A}.
Lemma qpolyC_natr p : (p%:R : {poly %/ h}) = p%:R :> {poly A}.
Lemma char_qpoly : [char {poly %/ h}] =i [char A].
Lemma poly_of_qpolyM (p q : {poly %/ h}) :
p × q = rmodp ((p : {poly A}) × q) (mk_monic h) :> {poly A}.
Lemma poly_of_qpolyX (p : {poly %/ h}) n :
p ^+ n = rmodp ((p : {poly A}) ^+ n) (mk_monic h) :> {poly A}.
Lemma qpolyCN (a : A) : qpolyC h (- a) = -(qpolyC h a).
Lemma qpolyCD : {morph (qpolyC h) : a b / a + b >-> a + b}%R.
Lemma qpolyCM : {morph (qpolyC h) : a b / a × b >-> a × b}%R.
Lemma qpolyC_is_rmorphism : rmorphism (qpolyC h).
Canonical qpolyC_rmorphism := RMorphism qpolyC_is_rmorphism.
Definition qpoly_scale k (p : {poly %/ h}) : {poly %/ h} := (k *: p)%R.
Fact qpoly_scaleA a b p :
qpoly_scale a (qpoly_scale b p) = qpoly_scale (a × b) p.
Fact qpoly_scale1l : left_id 1%R qpoly_scale.
Fact qpoly_scaleDr a : {morph qpoly_scale a : p q / (p + q)%R}.
Fact qpoly_scaleDl p : {morph qpoly_scale^~ p : a b / a + b}%R.
Fact qpoly_scaleAl a p q : qpoly_scale a (p × q) = (qpoly_scale a p × q).
Fact qpoly_scaleAr a p q : qpoly_scale a (p × q) = p × (qpoly_scale a q).
Canonical qpoly_lalgType :=
Eval hnf in LalgType A ({poly %/ h}) qpoly_scaleAl.
Canonical npoly_lalgType :=
Eval hnf in LalgType A ({poly_ _ _}) qpoly_scaleAl.
Canonical qpoly_algType := AlgType A {poly %/ h} qpoly_scaleAr.
Canonical npoly_algType := AlgType A {poly_ _ _} qpoly_scaleAr.
Lemma poly_of_qpolyZ (p : {poly %/ h}) a :
a *: p = a *: (p : {poly A}) :> {poly A}.
End QRing.
Section Field.
Variable R : fieldType.
Variable h : {poly R}.
Local Notation hQ := (mk_monic h).
Definition qpoly_inv (p : {poly %/ h}) :=
if coprimep hQ p then let v : {poly %/ h} := in_qpoly h (egcdp hQ p).2 in
((lead_coef (v × p)) ^-1 *: v) else p.
Ugly
Lemma qpoly_mulVz (p : {poly %/ h}) : coprimep hQ p → (qpoly_inv p × p = 1)%R.
Lemma qpoly_mulzV (p : {poly %/ h}) :
coprimep hQ p → (p × (qpoly_inv p) = 1)%R.
Lemma qpoly_intro_unit (p q : {poly %/ h}) : (q × p = 1)%R → coprimep hQ p.
Lemma qpoly_inv_out (p : {poly %/ h}) : ~~ coprimep hQ p → qpoly_inv p = p.
Definition qpoly_unitRingMixin :=
ComUnitRingMixin qpoly_mulVz qpoly_intro_unit qpoly_inv_out.
Canonical qpoly_unitRingType :=
Eval hnf in UnitRingType {poly %/ h} qpoly_unitRingMixin.
Canonical npoly_unitRingType :=
Eval hnf in UnitRingType {poly_ _ _} qpoly_unitRingMixin.
Canonical qpoly_comUnitRingType :=
Eval hnf in [comUnitRingType of {poly %/ h}].
Lemma irreducible_poly_coprime (A : idomainType) (p q : {poly A}) :
irreducible_poly p → coprimep p q = ~~(p %| q)%R.
End Field.
Lemma qpoly_mulzV (p : {poly %/ h}) :
coprimep hQ p → (p × (qpoly_inv p) = 1)%R.
Lemma qpoly_intro_unit (p q : {poly %/ h}) : (q × p = 1)%R → coprimep hQ p.
Lemma qpoly_inv_out (p : {poly %/ h}) : ~~ coprimep hQ p → qpoly_inv p = p.
Definition qpoly_unitRingMixin :=
ComUnitRingMixin qpoly_mulVz qpoly_intro_unit qpoly_inv_out.
Canonical qpoly_unitRingType :=
Eval hnf in UnitRingType {poly %/ h} qpoly_unitRingMixin.
Canonical npoly_unitRingType :=
Eval hnf in UnitRingType {poly_ _ _} qpoly_unitRingMixin.
Canonical qpoly_comUnitRingType :=
Eval hnf in [comUnitRingType of {poly %/ h}].
Lemma irreducible_poly_coprime (A : idomainType) (p q : {poly A}) :
irreducible_poly p → coprimep p q = ~~(p %| q)%R.
End Field.