Skip to content

Commit 0b9f898

Browse files
proux01proux01
committed
Add mrshift
1 parent 442529c commit 0b9f898

File tree

2 files changed

+229
-0
lines changed

2 files changed

+229
-0
lines changed

‎src/mpoly.v‎

Lines changed: 199 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,8 @@
4444
(* using Emn : m = n *)
4545
(* mwiden p == the canonical injection (ring morphism) from *)
4646
(* {mpoly R[n]} to {mpoly R[n.+1]} *)
47+
(* mrshift m p == the injection (ring morphism) from {mpoly R[n]} *)
48+
(* to {mpoly R[m+n]} that maps each 'X_i to 'X_(i+m) *)
4749
(* mpolyC c, c%:MP == the constant multivariate polynomial c *)
4850
(* 'X_i == the variable i, for i : 'I_n *)
4951
(* 'X_[m] == the monomial m as a multivariate polynomial *)
@@ -4070,6 +4072,203 @@ Proof. by rewrite /mpwiden map_polyZ. Qed.
40704072

40714073
End MWiden.
40724074

4075+
(* -------------------------------------------------------------------- *)
4076+
Section MRshift.
4077+
Context {R : ringType} {n : nat}.
4078+
4079+
Definition mrshift (m : nat) (p : {mpoly R[n]}) : {mpoly R[m + n]} :=
4080+
mmap (@mpolyC _ _) (fun i => 'X_(rshift m i)) p.
4081+
4082+
Definition mnmrshift (m : nat) (mn : 'X_{1..n}) : 'X_{1..m + n} :=
4083+
[multinom of nseq m 0%N ++ mn].
4084+
4085+
Lemma mnmrshift_l m mn (i : 'I_m) : mnmrshift m mn (lshift n i) = 0%N.
4086+
Proof.
4087+
by case: mn => mn; rewrite (mnm_nth 0%N)/= nth_cat size_nseq nth_nseq ltn_ord.
4088+
Qed.
4089+
4090+
Lemma mnmrshift_r m mn (i : 'I_n) : mnmrshift m mn (rshift m i) = mn i.
4091+
Proof.
4092+
case: mn => mn; rewrite !(mnm_nth 0%N)/=.
4093+
by rewrite nth_cat size_nseq ltnNge leq_addr addKn.
4094+
Qed.
4095+
4096+
Lemma mnmrshift0 m : mnmrshift m 0 = 0%MM.
4097+
Proof.
4098+
apply/mnmP => i; rewrite mnmE (mnm_nth 0%N)/= nth_cat size_nseq.
4099+
case: ltnP => im; first by rewrite nth_nseq; case: ifP.
4100+
case: n i im => [|n'] i im; first by rewrite enum_ord0 nth_nil.
4101+
by rewrite (nth_map 0)// size_enum_ord ltn_psubLR.
4102+
Qed.
4103+
4104+
Lemma mnmrshiftD m mn1 mn2 :
4105+
mnmrshift m (mn1 + mn2) = (mnmrshift m mn1 + mnmrshift m mn2)%MM.
4106+
Proof.
4107+
apply/mnmP => i; rewrite mnmDE !multinomE !(tnth_nth 0%N) !nth_cat size_nseq /=.
4108+
case: ltnP => im; first by rewrite nth_nseq im.
4109+
case: n mn1 mn2 i im => [|n'] mn1 mn2 i im.
4110+
by rewrite enum_ord0 tuple0 !nth_nil tuple0 nth_nil.
4111+
have imn' : (i - m < n'.+1)%N by rewrite ltn_psubLR.
4112+
by rewrite (nth_map 0) ?mnm_tnth ?(tnth_nth 0%N) ?nth_enum_ord ?size_enum_ord.
4113+
Qed.
4114+
4115+
Lemma mnmrshift_sum m (I : Type) (r : seq I) P F :
4116+
mnmrshift m (\sum_(x <- r | P x) (F x))
4117+
= (\sum_(x <- r | P x) (mnmrshift m (F x)))%MM.
4118+
Proof. exact/big_morph/mnmrshift0/mnmrshiftD. Qed.
4119+
4120+
Lemma mnmrshift1 m i : (mnmrshift m U_(i) = U_(rshift m i))%MM.
4121+
Proof.
4122+
apply/mnmP => j; rewrite /mnmrshift !mnmE multinomE (tnth_nth 0%N)/=.
4123+
rewrite nth_cat size_nseq; case: ltnP => jm; apply/esym/eqP.
4124+
by rewrite nth_nseq jm eqb0; apply: contra_ltnN jm => /eqP<-; apply: leq_addr.
4125+
case: n i j jm => [[]//|n'] i j jm; rewrite (nth_map 0); last first.
4126+
by rewrite ltn_subLR// size_enum_ord ltn_ord.
4127+
apply/eqP; congr (nat_of_bool _); apply/eqP/eqP.
4128+
- by move=> <-; rewrite addKn nth_ord_enum.
4129+
- move=> ->; apply/val_inj; rewrite /= nth_enum_ord ?subnKC//.
4130+
by rewrite ltn_subLR ?ltn_ord.
4131+
Qed.
4132+
4133+
Lemma inj_mnmrshift m : injective (mnmrshift m).
4134+
Proof.
4135+
move=> m1 m2 /mnmP h; apply/mnmP => i.
4136+
by move: (h (rshift m i)); rewrite !mnmrshift_r.
4137+
Qed.
4138+
4139+
Lemma mrshift0n (p : {mpoly R[n]}) : mrshift 0 p = p.
4140+
Proof.
4141+
rewrite [RHS]mpolyE; apply: eq_bigr => m _.
4142+
by rewrite mul_mpolyC; congr (_ *: _); rewrite mpolyXE_id.
4143+
Qed.
4144+
4145+
Lemma mrshift_is_additive m : additive (mrshift m).
4146+
Proof. exact/mmap_is_additive. Qed.
4147+
4148+
Lemma mrshift0 m : mrshift m 0 = 0. Proof. exact: raddf0. Qed.
4149+
Lemma mrshiftN m : {morph mrshift m: x / - x}. Proof. exact: raddfN. Qed.
4150+
Lemma mrshiftD m : {morph mrshift m: x y / x + y}. Proof. exact: raddfD. Qed.
4151+
Lemma mrshiftB m : {morph mrshift m: x y / x - y}. Proof. exact: raddfB. Qed.
4152+
Lemma mrshiftMn m k : {morph mrshift m: x / x *+ k}. Proof. exact: raddfMn. Qed.
4153+
Lemma mrshiftMNn m k : {morph mrshift m: x / x *- k}.
4154+
Proof. exact: raddfMNn. Qed.
4155+
4156+
HB.instance Definition _ m :=
4157+
GRing.isAdditive.Build {mpoly R[n]} {mpoly R[m + n]} (mrshift m)
4158+
(mrshift_is_additive m).
4159+
4160+
Lemma mrshift_is_multiplicative m : multiplicative (mrshift m).
4161+
Proof.
4162+
apply/commr_mmap_is_multiplicative=> [i p|p mn mn']; first exact/commr_mpolyX.
4163+
rewrite /= /mmap1; elim/big_rec: _ => /= [|i q _]; first exact/commr1.
4164+
exact/commrM/commrX/commr_mpolyX.
4165+
Qed.
4166+
4167+
HB.instance Definition _ m :=
4168+
GRing.isMultiplicative.Build {mpoly R[n]} {mpoly R[m + n]} (mrshift m)
4169+
(mrshift_is_multiplicative m).
4170+
4171+
Lemma mrshift1 m : mrshift m 1 = 1.
4172+
Proof. exact: rmorph1. Qed.
4173+
4174+
Lemma mrshiftM m : {morph mrshift m: x y / x * y}.
4175+
Proof. exact: rmorphM. Qed.
4176+
4177+
Lemma mrshiftC m c : mrshift m c%:MP = c%:MP.
4178+
Proof. by rewrite /mrshift mmapC. Qed.
4179+
4180+
Lemma mrshiftN1 m : mrshift m (-1) = -1.
4181+
Proof. by rewrite raddfN /= mrshiftC. Qed.
4182+
4183+
Lemma mrshiftX m mn : mrshift m 'X_[mn] = 'X_[mnmrshift m mn].
4184+
Proof.
4185+
rewrite /mrshift mmapX /mmap1 /= (mpolyXE _ 1); apply/esym.
4186+
rewrite (eq_bigr (fun i => 'X_i ^+ (mnmrshift m mn i))); last first.
4187+
by move=> i _; rewrite perm1.
4188+
rewrite big_split_ord/=; under eq_bigr => i _ do rewrite mnmrshift_l expr0.
4189+
by rewrite prodr_const expr1n mul1r; apply: eq_bigr => i _; rewrite mnmrshift_r.
4190+
Qed.
4191+
4192+
Lemma mrshiftZ m c p : mrshift m (c *: p) = c *: mrshift m p.
4193+
Proof. by rewrite /mrshift mmapZ /= mul_mpolyC. Qed.
4194+
4195+
Lemma mrshiftE m (p : {mpoly R[n]}) (k : nat) : msize p <= k ->
4196+
mrshift m p = \sum_(mn : 'X_{1..n < k}) (p@_mn *: 'X_[mnmrshift m mn]).
4197+
Proof.
4198+
move=> h; rewrite {1}[p](mpolywE (k := k)) //.
4199+
rewrite raddf_sum /=; apply/eq_bigr => mn _.
4200+
by rewrite mrshiftZ mrshiftX.
4201+
Qed.
4202+
4203+
Lemma mrshift_mnmrshift m p mn : (mrshift m p)@_(mnmrshift m mn) = p@_mn.
4204+
Proof.
4205+
rewrite (mrshiftE m (k := msize p)) // raddf_sum /=.
4206+
rewrite [X in _=X@__](mpolywE (k := msize p)) //.
4207+
rewrite raddf_sum /=; apply/eq_bigr=> i _.
4208+
by rewrite !mcoeffZ !mcoeffX inj_eq //; apply/inj_mnmrshift.
4209+
Qed.
4210+
4211+
Lemma inj_mrshift m : injective (mrshift m).
4212+
Proof.
4213+
move=> m1 m2 /mpolyP h; apply/mpolyP => mn.
4214+
by move: (h (mnmrshift m mn)); rewrite !mrshift_mnmrshift.
4215+
Qed.
4216+
4217+
Definition mprshift m (p : {poly {mpoly R[n]}}) : {poly {mpoly R[m + n]}} :=
4218+
map_poly (mrshift m) p.
4219+
4220+
Lemma mprshift_is_additive m : additive (mprshift m).
4221+
Proof. exact: map_poly_is_additive. Qed.
4222+
4223+
HB.instance Definition _ m :=
4224+
GRing.isAdditive.Build {poly {mpoly R[n]}} {poly {mpoly R[m + n]}}
4225+
(mprshift m) (mprshift_is_additive m).
4226+
4227+
Lemma mprshift_is_multiplicative m : multiplicative (mprshift m).
4228+
Proof. exact: map_poly_is_multiplicative. Qed.
4229+
4230+
HB.instance Definition _ m :=
4231+
GRing.isMultiplicative.Build {poly {mpoly R[n]}} {poly {mpoly R[m + n]}}
4232+
(mprshift m) (mprshift_is_multiplicative m).
4233+
4234+
Lemma mprshiftX m : mprshift m 'X = 'X.
4235+
Proof. by rewrite /mprshift map_polyX. Qed.
4236+
4237+
Lemma mprshiftC m c : mprshift m c%:P = (mrshift m c)%:P.
4238+
Proof. by rewrite /mprshift map_polyC. Qed.
4239+
4240+
Lemma mprshiftZ m c p : mprshift m (c *: p) = mrshift m c *: (mprshift m p).
4241+
Proof. by rewrite /mprshift map_polyZ. Qed.
4242+
4243+
End MRshift.
4244+
4245+
Lemma mnmrshiftDn {m n n'} (mn : 'X_{1..m}) : mnmrshift (n + n') mn
4246+
= mnmcast (addnA n n' m) (mnmrshift n (mnmrshift n' mn)).
4247+
Proof.
4248+
apply/mnmP => i; rewrite mnmcastE.
4249+
case: (split_ordP i) => {}i ->; last first.
4250+
by rewrite mnmrshift_r rshiftDn cast_ord_comp cast_ord_id !mnmrshift_r.
4251+
rewrite mnmrshift_l; case: (split_ordP i) => {}i ->; last first.
4252+
by rewrite lshift_rshift cast_ord_comp cast_ord_id mnmrshift_r mnmrshift_l.
4253+
by rewrite -lshiftDn mnmrshift_l.
4254+
Qed.
4255+
4256+
Lemma mrshiftDn {R m n n'} (p : {mpoly R[m]}) :
4257+
mrshift (n + n') p = mpcast (addnA _ _ _) (mrshift n (mrshift n' p)).
4258+
Proof.
4259+
rewrite [p]mpolyE rmorph_sum/= !(rmorph_sum (mrshift n'))/=.
4260+
rewrite (rmorph_sum (mrshift n)) (rmorph_sum (mpcast _))/=.
4261+
apply: eq_bigr => mn _; rewrite !mrshiftZ !mrshiftX mpcastZ mpcastX.
4262+
by rewrite mnmrshiftDn.
4263+
Qed.
4264+
4265+
Lemma mpcast_mrshiftDn {R m n1 n2 n3}
4266+
(eq_n' : n1 + (n2 + m) = n3) (eq_n : n1 + n2 + m = n3) (p : {mpoly R[m]}) :
4267+
mpcast eq_n (mrshift (n1 + n2) p) = mpcast eq_n' (mrshift n1 (mrshift n2 p)).
4268+
Proof.
4269+
by rewrite mrshiftDn mpcast_comp [etrans _ _](nat_irrelevance _ eq_n').
4270+
Qed.
4271+
40734272
(* -------------------------------------------------------------------- *)
40744273
Section MPolyUni.
40754274
Context (n : nat) (R : ringType).

‎src/ssrcomplements.v‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -310,3 +310,33 @@ Qed.
310310

311311
End WFTuple.
312312
End WF.
313+
314+
(* TODO: add to fintype.v *)
315+
Lemma rshiftDn {n n' m} (i : 'I_m) :
316+
rshift (n + n') i = cast_ord (addnA _ _ _) (rshift n (rshift n' i)).
317+
Proof. by apply: val_inj => /=; rewrite addnA. Qed.
318+
319+
(* TODO: add to fintype.v *)
320+
Lemma lshiftDn {m n n'} (i : 'I_m) :
321+
lshift (n + n') i = cast_ord (esym (addnA _ _ _)) (lshift n' (lshift n i)).
322+
Proof. exact: val_inj. Qed.
323+
324+
(* TODO: add to fintype.v *)
325+
Lemma lshift_lshift {m n n'} (i : 'I_m) :
326+
lshift n' (lshift n i) = cast_ord (addnA _ _ _) (lshift (n + n') i).
327+
Proof. exact: val_inj. Qed.
328+
329+
(* TODO: add to fintype.v *)
330+
Lemma rshift_rshift {n n' m} (i : 'I_m) :
331+
rshift n (rshift n' i) = cast_ord (esym (addnA _ _ _)) (rshift (n + n') i).
332+
Proof. by apply: val_inj => /=; rewrite addnA. Qed.
333+
334+
(* TODO: add to fintype.v *)
335+
Lemma lshift_rshift {m n n'} (i : 'I_n) :
336+
lshift n' (rshift m i) = cast_ord (addnA _ _ _) (rshift m (lshift n' i)).
337+
Proof. exact: val_inj. Qed.
338+
339+
(* TODO: add to fintype.v *)
340+
Lemma rshift_lshift {m n n'} (i : 'I_n) : rshift m (lshift n' i)
341+
= cast_ord (esym (addnA _ _ _)) (lshift n' (rshift m i)).
342+
Proof. exact: val_inj. Qed.

0 commit comments

Comments
 (0)