Library mathcomp.algebra.qpoly
From HB Require Import structures.
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.
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.
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_pred := fun p : {poly R} ⇒ size p ≤ n.
Arguments poly_of_size_pred _ /.
Definition poly_of_size := [qualify a p | poly_of_size_pred p].
Lemma npoly_submod_closed : submod_closed poly_of_size.
End poly_of_size.
Arguments poly_of_size_pred _ _ /.
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).
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_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 (Phant {poly_n R}).
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.
Arguments poly_of_size_pred _ _ _ /.
Section npoly_theory.
Context (R : ringType) {n : nat}.
Lemma polyn_is_linear : linear (@polyn _ _ _ : {poly_n R} → _).
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.
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.
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.
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).
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_additive : additive (qpolyC h).
Lemma qpolyC_is_multiplicative : multiplicative (qpolyC h).
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).
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.
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.
Lemma irreducible_poly_coprime (A : idomainType) (p q : {poly A}) :
irreducible_poly p → coprimep p q = ~~(p %| q)%R.
End Field.