From a09a371c598abcef811fd85930ea246ba159e5f2 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Mon, 20 Nov 2023 17:10:07 +0100 Subject: [PATCH] Generalize some results in monalg to nmodType and semiRingType --- src/monalg.v | 504 +++++++++++++++++++++++++++++---------------------- 1 file changed, 285 insertions(+), 219 deletions(-) diff --git a/src/monalg.v b/src/monalg.v index 297bc5c..66e8e70 100644 --- a/src/monalg.v +++ b/src/monalg.v @@ -106,6 +106,7 @@ Export ConomialDefExports. (* -------------------------------------------------------------------- *) Section Monomial. + Context (M : monomType). Local Open Scope monom_scope. @@ -117,6 +118,7 @@ Lemma unitmP (x y : M) : reflect (x == 1 /\ y == 1) (x * y == 1). Proof. by apply: (iffP eqP)=> [/unitm[-> ->]|[/eqP-> /eqP->]] //; rewrite mulm1. Qed. + End Monomial. #[export] @@ -127,16 +129,16 @@ Module Exports. HB.reexport. End Exports. Export Exports. (* -------------------------------------------------------------------- *) -Definition mmorphism (M : monomType) (S : ringType) (f : M -> S) := +Definition mmorphism (M : monomType) (S : semiRingType) (f : M -> S) := {morph f : x y / (x * y)%M >-> (x * y)%R} * (f 1%M = 1) : Prop. HB.mixin Record isMultiplicative - (M : monomType) (S : ringType) (apply : M -> S) := { + (M : monomType) (S : semiRingType) (apply : M -> S) := { mmorphism_subproof : mmorphism apply; }. #[mathcomp(axiom="multiplicative")] -HB.structure Definition MMorphism (M : monomType) (S : ringType) := +HB.structure Definition MMorphism (M : monomType) (S : semiRingType) := {f of isMultiplicative M S f}. Module MMorphismExports. @@ -152,18 +154,21 @@ Export MMorphismExports. (* -------------------------------------------------------------------- *) Section MMorphismTheory. -Variables (M : monomType) (S : ringType) (f : {mmorphism M -> S}). + +Context {M : monomType} {S : semiRingType} (f : {mmorphism M -> S}). Lemma mmorph1 : f 1%M = 1. Proof. exact: mmorphism_subproof.2. Qed. Lemma mmorphM : {morph f : x y / (x * y)%M >-> (x * y)%R}. Proof. exact: mmorphism_subproof.1. Qed. + End MMorphismTheory. (* -------------------------------------------------------------------- *) Section MalgDef. -Variable (K : choiceType) (G : zmodType). + +Context (K : choiceType) (G : nmodType). Record malg : predArgType := Malg { malg_val : {fsfun K -> G with 0} }. @@ -186,7 +191,7 @@ Notation "{ 'malg' K }" := {malg int[K]} : type_scope. (* -------------------------------------------------------------------- *) Section MalgBaseOp. -Context {K : choiceType} {G : zmodType}. +Context {K : choiceType} {G : nmodType}. Definition mcoeff (x : K) (g : {malg G[K]}) : G := malg_val g x. @@ -219,8 +224,11 @@ Notation "@ 'malgC' K G" := (@mkmalgU K G 1) Notation "c %:MP" := (malgC c) : ring_scope. (* -------------------------------------------------------------------- *) -Section MalgTheory. -Variable (K : choiceType) (G : zmodType). +Section MalgNmodTheory. + +Context {K : choiceType} {G : nmodType}. + +Implicit Types (g : {malg G[K]}) (k : K) (x y : G). Lemma mkmalgK (g : {fsfun K -> G with 0}) : malg_val (mkmalg g) = g. Proof. by []. Qed. @@ -252,24 +260,14 @@ Variant msupp_spec (g : {malg G[K]}) (k : K) : bool -> G -> Type := Lemma msuppP (g : {malg G[K]}) (k : K) : msupp_spec g k (k \in msupp g) g@_k. Proof. by rewrite /mcoeff; case: finsuppP => h; constructor. Qed. -End MalgTheory. - -(* -------------------------------------------------------------------- *) -Section MalgZMod. -Variable (K : choiceType) (G : zmodType). - -Implicit Types (g : {malg G[K]}) (k : K). +(* `{malg G[K]}` forms an N-module. *) Definition fgzero : {malg G[K]} := [malg x => [fmap] x]. -Definition fgopp g := [malg k in msupp g => - g@_k]. Definition fgadd g1 g2 := [malg k in msupp g1 `|` msupp g2 => g1@_k + g2@_k]. Lemma fgzeroE k : fgzero@_k = 0. Proof. by rewrite mcoeff_fnd !(in_fsetE, not_fnd). Qed. -Lemma fgoppE g k : (fgopp g)@_k = - g@_k. -Proof. by rewrite mcoeffE; case: msuppP; rewrite ?oppr0. Qed. - Lemma fgaddE g1 g2 k : (fgadd g1 g2)@_k = g1@_k + g2@_k. Proof. rewrite mcoeffE in_fsetE. @@ -288,45 +286,23 @@ Proof. by move=> x; apply/malgP=> k; rewrite fgaddE fgzeroE add0r. Qed. Lemma fgaddg0 : right_id fgzero fgadd. Proof. by move=> x; rewrite fgaddC fgadd0g. Qed. -Lemma fgaddNg : left_inverse fgzero fgopp fgadd. -Proof. by move=> x; apply/malgP=> k; rewrite !fgaddE fgzeroE fgoppE addNr. Qed. - -Lemma fgaddgN : right_inverse fgzero fgopp fgadd. -Proof. by move=> x; rewrite fgaddC fgaddNg. Qed. - -HB.instance Definition _ := GRing.isZmodule.Build (malg K G) - fgaddA fgaddC fgadd0g fgaddNg. -HB.instance Definition _ := GRing.Zmodule.on {malg G[K]}. -End MalgZMod. - -Section MAlgZModTheory. -Context {K : choiceType} {G : zmodType}. - -Implicit Types (g : {malg G[K]}) (k : K) (x y : G). - -Local Notation mcoeff := (@mcoeff K G) (only parsing). -Local Notation msupp := (@msupp K G). -Local Notation mkmalgU := (@mkmalgU K G) (only parsing). - -Let fgE := (fgzeroE, fgoppE, fgaddE). +HB.instance Definition _ := + GRing.isNmodule.Build {malg G[K]} fgaddA fgaddC fgadd0g. -(* -------------------------------------------------------------------- *) Lemma malgD_def g1 g2 : g1 + g2 = fgadd g1 g2. Proof. by []. Qed. -(* -------------------------------------------------------------------- *) -Lemma mcoeff_is_additive k: additive (mcoeff k). -Proof. by move=> g1 g2 /=; rewrite fgaddE fgoppE. (* !fgE *) Qed. +(* `mcoeff k` is semi-additive *) +Lemma mcoeff_is_semi_additive k: semi_additive (mcoeff k). +Proof. by split=> [|g1 g2] /=; rewrite (fgzeroE, fgaddE). Qed. -HB.instance Definition _ k := GRing.isAdditive.Build {malg G[K]} G (mcoeff k) - (mcoeff_is_additive k). +HB.instance Definition _ k := + GRing.isSemiAdditive.Build {malg G[K]} G (mcoeff k) + (mcoeff_is_semi_additive k). Lemma mcoeff0 k : 0@_k = 0 :> G . Proof. exact: raddf0. Qed. -Lemma mcoeffN k : {morph mcoeff k: x / - x} . Proof. exact: raddfN. Qed. Lemma mcoeffD k : {morph mcoeff k: x y / x + y}. Proof. exact: raddfD. Qed. -Lemma mcoeffB k : {morph mcoeff k: x y / x - y}. Proof. exact: raddfB. Qed. Lemma mcoeffMn k n : {morph mcoeff k: x / x *+ n} . Proof. exact: raddfMn. Qed. -Lemma mcoeffMNn k n : {morph mcoeff k: x / x *- n} . Proof. exact: raddfMNn. Qed. Lemma mcoeffU k x k' : << x *g k >>@_k' = x *+ (k == k'). Proof. by rewrite mcoeff_fnd fnd_set fnd_fmap0; case: eqVneq. Qed. @@ -334,13 +310,45 @@ Proof. by rewrite mcoeff_fnd fnd_set fnd_fmap0; case: eqVneq. Qed. Lemma mcoeffUU k x : << x *g k >>@_k = x. Proof. by rewrite mcoeffU eqxx. Qed. -Let mcoeffsE := (mcoeff0, mcoeffU, mcoeffB, mcoeffD, mcoeffN, mcoeffMn). +Let mcoeffsE := (mcoeff0, mcoeffU, mcoeffD, mcoeffMn). -(* -------------------------------------------------------------------- *) +(* `mkmalgU k` is semi-additive *) +Lemma monalgU_is_semi_additive k : semi_additive (mkmalgU k). +Proof. +by split=> [|x1 x2] /=; apply/malgP=> k'; rewrite !mcoeffsE (mul0rn, mulrnDl). +Qed. + +HB.instance Definition _ k := + GRing.isSemiAdditive.Build G {malg G[K]} (mkmalgU k) + (monalgU_is_semi_additive k). + +Lemma monalgU0 k : << 0 *g k >> = 0 . Proof. exact: raddf0. Qed. +Lemma monalgUD k : {morph mkmalgU k: x y / x + y}. Proof. exact: raddfD. Qed. +Lemma monalgUMn k n : {morph mkmalgU k: x / x *+ n} . Proof. exact: raddfMn. Qed. + +Lemma monalgU_eq0 x k: (<< x *g k >> == 0) = (x == 0). +Proof. +apply/eqP/eqP => [/(congr1 (mcoeff k))|->]; last by rewrite monalgU0. +by rewrite !mcoeffsE eqxx. +Qed. + +Lemma monalgEw (g : {malg G[K]}) (domg : {fset K}) : msupp g `<=` domg -> + g = \sum_(k <- domg) << g@_k *g k >>. +Proof. +move/fsubsetP=> le_gd; apply/malgP=> k; have [/le_gd kg|k_notin_g] := msuppP. + rewrite raddf_sum (big_fsetD1 k) //= mcoeffUU big1_fset ?addr0 // => k'. + by rewrite in_fsetD1 mcoeffU; case: eqP. +rewrite raddf_sum /= big1_fset // => k' _ _. +by rewrite mcoeffU; case: eqP k_notin_g => // <- /mcoeff_outdom ->. +Qed. + +Lemma monalgE (g : {malg G[K]}) : g = \sum_(k <- msupp g) << g@_k *g k >>. +Proof. exact/monalgEw. Qed. + +(* msupp *) Lemma msupp0 : msupp 0 = fset0 :> {fset K}. Proof. -apply/fsetP=> k; rewrite in_fset0; apply/negbTE. -by rewrite -mcoeff_eq0 mcoeff0. +by apply/fsetP=> k; rewrite in_fset0; apply/negbTE; rewrite -mcoeff_eq0 mcoeff0. Qed. Lemma msuppU k x : msupp << x *g k >> = if x == 0 then fset0 else [fset k]. @@ -352,118 +360,81 @@ Qed. Lemma msuppU_le {k x} : msupp << x *g k >> `<=` [fset k]. Proof. by rewrite msuppU; case: eqP. Qed. -Lemma msuppN g : msupp (-g) = msupp g. -Proof. by apply/fsetP=> k; rewrite -!mcoeff_neq0 mcoeffN oppr_eq0. Qed. - Lemma msuppD_le g1 g2 : msupp (g1 + g2) `<=` msupp g1 `|` msupp g2. Proof. apply/fsubsetP=> k; rewrite in_fsetU -mcoeff_neq0 mcoeffD. by case: (msuppP g1); case: (msuppP g2); rewrite //= addr0 eqxx. Qed. -Lemma msuppB_le g1 g2 : msupp (g1 - g2) `<=` msupp g1 `|` msupp g2. -Proof. by rewrite -[msupp g2]msuppN; apply/msuppD_le. Qed. - Lemma msuppD g1 g2 : [disjoint msupp g1 & msupp g2] -> msupp (g1 + g2) = msupp g1 `|` msupp g2. Proof. move=> dj_g1g2; apply/fsetP=> k; move/fdisjointP/(_ k): dj_g1g2. rewrite in_fsetU -!mcoeff_neq0 mcoeffD negbK. -have [->|] //= := eqVneq (g1@_k) 0; first by rewrite add0r. +have [->|] //= := eqVneq g1@_k 0; first by rewrite add0r. by move=> + /(_ isT) /eqP ->; rewrite addr0. Qed. -Lemma msuppB g1 g2 : [disjoint msupp g1 & msupp g2] -> - msupp (g1 - g2) = msupp g1 `|` msupp g2. -Proof. by move=> dj_g1g2; rewrite msuppD msuppN. Qed. - Lemma msuppMn_le g n : msupp (g *+ n) `<=` msupp g. Proof. apply/fsubsetP=> k; rewrite -!mcoeff_neq0 mcoeffMn. by apply/contra_neq => ->; rewrite mul0rn. Qed. -Lemma msuppMNm_le g n : msupp (g *- n) `<=` msupp g. -Proof. by rewrite msuppN msuppMn_le. Qed. +End MalgNmodTheory. (* -------------------------------------------------------------------- *) -Lemma monalgU_is_additive k : additive (mkmalgU k). -Proof. by move=> x1 x2 /=; apply/malgP=> k'; rewrite !mcoeffsE mulrnBl. Qed. - -HB.instance Definition _ k := GRing.isAdditive.Build G {malg G[K]} (mkmalgU k) - (monalgU_is_additive k). +Section MalgZmodTheory. -Lemma monalgU0 k : << (0 : G) *g k >> = 0 . Proof. exact: raddf0. Qed. -Lemma monalgUN k : {morph mkmalgU k: x / - x} . Proof. exact: raddfN. Qed. -Lemma monalgUD k : {morph mkmalgU k: x y / x + y}. Proof. exact: raddfD. Qed. -Lemma monalgUB k : {morph mkmalgU k: x y / x - y}. Proof. exact: raddfB. Qed. -Lemma monalgUMn k n : {morph mkmalgU k: x / x *+ n} . Proof. exact: raddfMn. Qed. -Lemma monalgUMNn k n : {morph mkmalgU k: x / x *- n} . Proof. exact: raddfMNn. Qed. +Context {K : choiceType} {G : zmodType}. -Lemma monalgU_eq0 x k: (<< x *g k >> == 0) = (x == 0). -Proof. -apply/eqP/eqP => [/(congr1 (mcoeff k))|->]; last by rewrite monalgU0. -by rewrite !mcoeffsE eqxx. -Qed. +Implicit Types (g : {malg G[K]}) (k : K) (x y : G). -Definition monalgUE := - (monalgU0, monalgUB, monalgUD, monalgUN, monalgUMn). +Definition fgopp g := [malg k in msupp g => - g@_k]. -(* -------------------------------------------------------------------- *) -Lemma monalgEw (g : {malg G[K]}) (domg : {fset K}) : msupp g `<=` domg -> - g = \sum_(k <- domg) << g@_k *g k >>. -Proof. -move/fsubsetP=> le_gd; apply/malgP=> k; have [/le_gd kg|k_notin_g] := msuppP. - rewrite raddf_sum (big_fsetD1 k) //= mcoeffUU big1_fset ?addr0 // => k'. - by rewrite in_fsetD1 mcoeffU; case: eqP. -rewrite raddf_sum /= big1_fset // => k' _ _. -by rewrite mcoeffU; case: eqP k_notin_g => // <- /mcoeff_outdom ->. -Qed. +Lemma fgoppE g k : (fgopp g)@_k = - g@_k. +Proof. by rewrite [LHS]mcoeffE; case: msuppP; rewrite // oppr0. Qed. -Lemma monalgE (g : {malg G[K]}) : g = \sum_(k <- msupp g) << g@_k *g k >>. -Proof. exact/monalgEw. Qed. -End MAlgZModTheory. +Lemma fgaddNg : left_inverse 0 fgopp +%R. +Proof. by move=> x; apply/malgP => k; rewrite fgaddE fgoppE addNr fgzeroE. Qed. -(* -------------------------------------------------------------------- *) -Section MalgMonomTheory. -Context {K : monomType} {G : zmodType}. +Lemma fgaddgN : right_inverse 0%R fgopp +%R. +Proof. by move=> x; rewrite addrC fgaddNg. Qed. -(* -------------------------------------------------------------------- *) -Lemma msuppC (c : G) : - msupp c%:MP = (if c == 0 then fset0 else [fset 1%M]) :> {fset K}. -Proof. exact/msuppU. Qed. +HB.instance Definition _ := GRing.Nmodule_isZmodule.Build {malg G[K]} fgaddNg. -Lemma msuppC_le (c : G) : msupp c%:MP `<=` ([fset 1%M] : {fset K}). -Proof. by rewrite msuppC; case: eqP=> _; rewrite ?fsubset_refl // fsub0set. Qed. +Lemma mcoeffN k : {morph mcoeff k: x / - x} . Proof. exact: raddfN. Qed. +Lemma mcoeffB k : {morph mcoeff k: x y / x - y}. Proof. exact: raddfB. Qed. +Lemma mcoeffMNn k n : {morph mcoeff k: x / x *- n} . Proof. exact: raddfMNn. Qed. -Lemma mcoeffC (c : G) k : c%:MP@_k = c *+ (k == 1%M :> K). -Proof. by rewrite mcoeffU eq_sym. Qed. +Lemma monalgUN k : {morph mkmalgU k: x / - x} . Proof. exact: raddfN. Qed. +Lemma monalgUB k : {morph mkmalgU k: x y / x - y}. Proof. exact: raddfB. Qed. +Lemma monalgUMNn k n : {morph mkmalgU k: x / x *- n} . Proof. exact: raddfMNn. Qed. -Lemma mcoeffC0 (k : K) : 0%:MP@_k = 0 :> G. -Proof. by rewrite mcoeffC mul0rn. Qed. +Definition monalgUE := + (@monalgU0 K G, monalgUB, @monalgUD K G, monalgUN, @monalgUMn K G). -Lemma msuppC0 : msupp (0 : G)%:MP = fset0 :> {fset K}. -Proof. by rewrite msuppC eqxx. Qed. +Lemma msuppN g : msupp (-g) = msupp g. +Proof. by apply/fsetP=> k; rewrite -!mcoeff_neq0 mcoeffN oppr_eq0. Qed. -Lemma malgC0E : 0%:MP = 0 :> {malg G[K]}. -Proof. by apply/malgP=> k; rewrite mcoeffC0 mcoeff0. Qed. +Lemma msuppB_le g1 g2 : msupp (g1 - g2) `<=` msupp g1 `|` msupp g2. +Proof. by rewrite -[msupp g2]msuppN; apply/msuppD_le. Qed. -Lemma malgCK : cancel malgC (@mcoeff K G 1%M). -Proof. by move=> c; rewrite mcoeffC eqxx mulr1n. Qed. +Lemma msuppB g1 g2 : [disjoint msupp g1 & msupp g2] -> + msupp (g1 - g2) = msupp g1 `|` msupp g2. +Proof. by move=> dj_g1g2; rewrite msuppD msuppN. Qed. -Lemma malgC_eq (c1 c2 : G) : (c1%:MP == c2%:MP :> {malg G[K]}) = (c1 == c2). -Proof. by apply/eqP/eqP=> [|->//] /malgP/(_ 1%M); rewrite !mcoeffU eqxx. Qed. +Lemma msuppMNm_le g n : msupp (g *- n) `<=` msupp g. +Proof. by rewrite msuppN msuppMn_le. Qed. -Lemma msupp_eq0 (g : {malg G[K]}) : (msupp g == fset0) = (g == 0). -Proof. -apply/eqP/eqP=> [/fsetP z_g|->]; last exact: msupp0. -by apply/malgP=> i; rewrite mcoeff0 mcoeff_outdom // z_g. -Qed. -End MalgMonomTheory. +End MalgZmodTheory. (* -------------------------------------------------------------------- *) -Section MAlgLMod. -Context (K : choiceType) (R : ringType). +Section MalgSemiRingTheory. + +Context {K : choiceType} {R : semiRingType}. + +Implicit Types (g : {malg R[K]}). Definition fgscale c g : {malg R[K]} := \sum_(k <- msupp g) << c * g@_k *g k >>. @@ -471,7 +442,7 @@ Local Notation "c *:g g" := (fgscale c g) (at level 40, left associativity). Lemma fgscaleE c g k : (c *:g g)@_k = c * g@_k. Proof. -rewrite {2}[g]monalgE !raddf_sum mulr_sumr. +rewrite [g in RHS]monalgE !raddf_sum mulr_sumr. by apply/eq_bigr=> /= i _; rewrite !mcoeffU mulrnAr. Qed. @@ -487,21 +458,22 @@ Proof. by apply/malgP=> k; rewrite !(mcoeffD, fgscaleE) mulrDr. Qed. Lemma fgscaleDl g c1 c2: (c1 + c2) *:g g = c1 *:g g + c2 *:g g. Proof. by apply/malgP=> x; rewrite !(mcoeffD, fgscaleE) mulrDl. Qed. -HB.instance Definition _ := GRing.Zmodule_isLmodule.Build R (malg K R) - fgscaleA fgscale1r fgscaleDr fgscaleDl. -HB.instance Definition _ := GRing.Lmodule.on {malg R[K]}. -End MAlgLMod. +End MalgSemiRingTheory. (* -------------------------------------------------------------------- *) -Section MAlgLModTheory. +Section MalgRingTheory. + Context {K : choiceType} {R : ringType}. Implicit Types (g : {malg R[K]}). +(* TODO: Add a semi-module structure and generalize this section *) +HB.instance Definition _ := GRing.Zmodule_isLmodule.Build R {malg R[K]} + fgscaleA fgscale1r fgscaleDr fgscaleDl. + Lemma malgZ_def c g : c *: g = fgscale c g. Proof. by []. Qed. -(* -------------------------------------------------------------------- *) Lemma mcoeffZ c g k : (c *: g)@_k = c * g@_k. Proof. exact/fgscaleE. Qed. @@ -510,27 +482,27 @@ Proof. exact/fgscaleE. Qed. (* GRing.isLinear.Build R [lmodType R of {malg R[K]}] R *%R (mcoeff m) *) (* (fun c g => mcoeffZ c g m). *) -(* -------------------------------------------------------------------- *) Lemma msuppZ_le c g : msupp (c *: g) `<=` msupp g. Proof. apply/fsubsetP=> k; rewrite -!mcoeff_neq0 mcoeffZ. by apply/contraTneq=> ->; rewrite mulr0 negbK. Qed. -End MAlgLModTheory. + +End MalgRingTheory. (* -------------------------------------------------------------------- *) -Section MAlgLModTheoryIntegralDomain. -Context {K : choiceType} {R : idomainType}. +Section MalgLmodTheoryIntegralDomain. -Implicit Types (g : {malg R[K]}). +Context {K : choiceType} {R : idomainType}. -(* -------------------------------------------------------------------- *) -Lemma msuppZ c g : msupp (c *: g) = if c == 0 then fset0 else msupp g. +Lemma msuppZ (c : R) (g : {malg R[K]}) : + msupp (c *: g) = if c == 0 then fset0 else msupp g. Proof. case: eqP=> [->|/eqP nz_c]; first by rewrite scale0r msupp0. by apply/fsetP=> k; rewrite -!mcoeff_neq0 mcoeffZ mulf_eq0 negb_or nz_c. Qed. -End MAlgLModTheoryIntegralDomain. + +End MalgLmodTheoryIntegralDomain. (* -------------------------------------------------------------------- *) Definition mcoeffsE := @@ -538,25 +510,59 @@ Definition mcoeffsE := @mcoeffN, @mcoeffMn, @mcoeffZ). (* -------------------------------------------------------------------- *) -Section MAlgRingType. -Context (K : monomType) (R : ringType). +Section MalgMonomTheory. + +Context {K : monomType} {G : nmodType}. + +Lemma msuppC (c : G) : + msupp c%:MP = (if c == 0 then fset0 else [fset 1%M]) :> {fset K}. +Proof. exact: msuppU. Qed. + +Lemma msuppC_le (c : G) : msupp c%:MP `<=` ([fset 1%M] : {fset K}). +Proof. exact: msuppU_le. Qed. + +Lemma mcoeffC (c : G) k : c%:MP@_k = c *+ (k == 1%M :> K). +Proof. by rewrite mcoeffU eq_sym. Qed. + +Lemma mcoeffC0 (k : K) : 0%:MP@_k = 0 :> G. +Proof. by rewrite mcoeffC mul0rn. Qed. + +Lemma msuppC0 : msupp (0 : G)%:MP = fset0 :> {fset K}. +Proof. by rewrite msuppC eqxx. Qed. + +Lemma malgC0E : 0%:MP = 0 :> {malg G[K]}. +Proof. exact: monalgU0. Qed. + +Lemma malgCK : cancel malgC (@mcoeff K G 1). +Proof. by move=> c; rewrite mcoeffC eqxx. Qed. + +Lemma malgC_inj : injective (@malgC K G). +Proof. exact: can_inj malgCK. Qed. + +Lemma malgC_eq (c1 c2 : G) : (c1%:MP == c2%:MP :> {malg G[K]}) = (c1 == c2). +Proof. by apply/eqP/eqP => [/malgC_inj|->//]. Qed. + +Lemma msupp_eq0 (g : {malg G[K]}) : (msupp g == fset0) = (g == 0). +Proof. +apply/eqP/eqP=> [/fsetP z_g|->]; last exact: msupp0. +by apply/malgP=> i; rewrite mcoeff0 mcoeff_outdom // z_g. +Qed. + +End MalgMonomTheory. + +(* -------------------------------------------------------------------- *) +Section MalgSemiRingType. + +Context (K : monomType) (R : semiRingType). Implicit Types (g : {malg R[K]}) (k l : K). -Definition fgone : {malg R[K]} := << 1%M >>. +Definition fgone : {malg R[K]} := << 1 >>. Local Notation "g1 *M_[ k1 , k2 ] g2" := - << g1@_k1%M * g2@_k2%M *g (k1 * k2)%M >> + << g1@_k1 * g2@_k2 *g (k1 * k2) >> (at level 40, no associativity, format "g1 *M_[ k1 , k2 ] g2"). -Local Notation "g1 *gM_[ k2 ] g2" := - (\sum_(k1 <- msupp g1) g1 *M_[k1, k2] g2) - (at level 40, no associativity, only parsing). - -Local Notation "g1 *Mg_[ k1 ] g2" := - (\sum_(k2 <- msupp g2) g1 *M_[k1, k2] g2) - (at level 40, no associativity, only parsing). - Definition fgmul g1 g2 : {malg R[K]} := \sum_(k1 <- msupp g1) \sum_(k2 <- msupp g2) g1 *M_[k1, k2] g2. @@ -566,7 +572,7 @@ Proof. by []. Qed. Lemma fgmulr g1 g2 : fgmul g1 g2 = \sum_(k2 <- msupp g2) \sum_(k1 <- msupp g1) g1 *M_[k1, k2] g2. -Proof. by rewrite fgmull exchange_big. Qed. +Proof. exact: exchange_big. Qed. (* big_fset_incl has (op : com_law idx) as first non automatic argument *) Lemma fgmullw (d1 d2 : {fset K}) g1 g2 : @@ -634,7 +640,6 @@ move=> g; rewrite fgmulgU [RHS]monalgE. by apply/eq_bigr=> k _; rewrite mulr1 mulm1. Qed. - Lemma fgmulgDl : left_distributive fgmul +%R. Proof. move=> g1 g2 g; rewrite [in RHS](fgmullwl (fsubsetUl _ (msupp g2))). @@ -668,15 +673,15 @@ Qed. Lemma fgoner_eq0 : fgone != 0. Proof. by apply/eqP/malgP=> /(_ 1%M) /eqP; rewrite !mcoeffsE oner_eq0. Qed. -HB.instance Definition _ := GRing.Zmodule_isRing.Build (malg K R) - fgmulA fgmul1g fgmulg1 fgmulgDl fgmulgDr fgoner_eq0. -HB.instance Definition _ := GRing.Ring.on {malg R[K]}. +HB.instance Definition _ := GRing.Nmodule_isSemiRing.Build {malg R[K]} + fgmulA fgmul1g fgmulg1 fgmulgDl fgmulgDr fgmul0g fgmulg0 fgoner_eq0. -End MAlgRingType. +End MalgSemiRingType. (* -------------------------------------------------------------------- *) -Section MAlgRingTheory. -Context (K : monomType) (R : ringType). +Section MalgSemiRingTheory. + +Context {K : monomType} {R : semiRingType}. Implicit Types (g : {malg R[K]}) (k l : K). @@ -728,14 +733,12 @@ Proof. exact: mcoeffMrw. Qed. Lemma mcoeff1 k : 1@_k = (k == 1%M)%:R :> R. Proof. by rewrite mcoeffC. Qed. -Lemma mul_malgC c g : c%:MP * g = c *: g. +Lemma mcoeffCM c g k : (c%:MP * g)@_k = c * g@_k :> R. Proof. -by rewrite malgM_def malgZ_def fgmulUg; apply/eq_bigr=> /= k _; rewrite mul1m. +rewrite [_ * _ in LHS]fgmulUg [g in RHS]monalgE !raddf_sum /= mulr_sumr. +by apply/eq_bigr=> k' _; rewrite mul1m !mcoeffU mulrnAr. Qed. -Lemma mcoeffCM c g k : (c%:MP * g)@_k = c * g@_k :> R. -Proof. by rewrite mul_malgC mcoeffZ. Qed. - Lemma msuppM_le_finType g1 g2 k : k \in msupp (g1 * g2) -> exists (k1 : msupp g1) (k2 : msupp g2), k = (val k1 * val k2)%M. @@ -800,6 +803,23 @@ HB.instance Definition _ := GRing.isMultiplicative.Build {malg R[K]} R (@mcoeff K R 1%M) mcoeff1g_is_multiplicative. +End MalgSemiRingTheory. + +(* -------------------------------------------------------------------- *) +Section MalgRingTheory. + +Context {K : monomType} {R : ringType}. + +Implicit Types (g : {malg R[K]}) (k l : K). + +HB.instance Definition _ := GRing.SemiRing.on {malg R[K]}. + +Lemma mul_malgC c g : c%:MP * g = c *: g. +Proof. +rewrite malgM_def malgZ_def fgmulUg. +by apply/eq_bigr=> /= k _; rewrite mul1m. +Qed. + (* FIXME: building Linear instance here so as to not trigger the creation of a LRMorphism that fails on above command (but is built just below anyway) *) HB.instance Definition _ m := @@ -809,15 +829,15 @@ HB.instance Definition _ m := Lemma fgscaleAl c g1 g2 : c *: (g1 * g2) = (c *: g1) * g2. Proof. by rewrite -!mul_malgC mulrA. Qed. -HB.instance Definition _ := GRing.Lmodule_isLalgebra.Build R (malg K R) +HB.instance Definition _ := GRing.Lmodule_isLalgebra.Build R {malg R[K]} fgscaleAl. -HB.instance Definition _ := GRing.Lalgebra.on {malg R[K]}. -End MAlgRingTheory. +End MalgRingTheory. (* -------------------------------------------------------------------- *) Section MalgComRingType. -Context (K : conomType) (R : comRingType). + +Context {K : conomType} {R : comRingType}. Lemma fgmulC : @commutative {malg R[K]} _ *%R. Proof. @@ -829,70 +849,80 @@ Qed. HB.instance Definition _ := GRing.Ring_hasCommutativeMul.Build (malg K R) fgmulC. -HB.instance Definition _ := GRing.Lalgebra_isComAlgebra.Build R (malg K R). - -HB.instance Definition _ := GRing.ComAlgebra.on {malg R[K]}. +HB.instance Definition _ := GRing.Lalgebra_isComAlgebra.Build R {malg R[K]}. End MalgComRingType. (* -------------------------------------------------------------------- *) Section MalgMorphism. Section Defs. -Context (K : choiceType) (G : zmodType) (S : ringType). + +Context {K : choiceType} {G : nmodType} {S : semiRingType}. Context (f : G -> S) (h : K -> S). Definition mmap g := \sum_(k <- msupp g) f g@_k * h k. Lemma mmapE g : mmap g = \sum_(k <- msupp g) f g@_k * h k. Proof. by []. Qed. + End Defs. Local Notation "g ^[ f , h ]" := (mmap f h g). -Section BaseTheory. -Context (K : choiceType) (G : zmodType) (S : ringType). -Context {f : {additive G -> S}} {h : K -> S}. +Section SemiAdditive. + +Context {K : choiceType} {G : nmodType} {S : semiRingType}. Lemma mmapEw (d : {fset K}) g : msupp g `<=` d -> + forall (f : {additive G -> S}) (h : K -> S), g^[f, h] = \sum_(k <- d) f g@_k * h k. Proof. -move=> le; rewrite [LHS](big_fset_incl _ le) => //= x xd /mcoeff_outdom ->. +move=> le f h; rewrite [LHS](big_fset_incl _ le) => //= x xd /mcoeff_outdom ->. by rewrite raddf0 mul0r. Qed. -Lemma mmapU (c : G) (m : K) : mmap f h << c *g m >> = f c * h m. +Lemma mmapU (f : {additive G -> S}) (h : K -> S) (c : G) (m : K) : + mmap f h << c *g m >> = f c * h m. Proof. by rewrite (mmapEw msuppU_le) big_seq_fset1 mcoeffUU. Qed. -End BaseTheory. -Section Additive. -Context (K : choiceType) (G : zmodType) (S : ringType). -Context {f : {additive G -> S}} {h : K -> S}. +Context (f : {additive G -> S}) (h : K -> S). -Lemma mmap_is_additive : additive (mmap f h). +Lemma mmap_is_semi_additive : semi_additive (mmap f h). Proof. -move=> g1 g2 /=; pose_big_fset K E; rewrite 3?(mmapEw (d := E)) //. - by rewrite -sumrB; apply/eq_bigr=> k _; rewrite !raddfB /= mulrBl. +split=> [|g1 g2]; first by rewrite /mmap msupp0 big_seq_fset0. +pose_big_fset K E. + rewrite 3?(mmapEw (d := E)) //; rewrite -big_split. + by apply/eq_bigr=> k _; rewrite !raddfD /= mulrDl. by close. Qed. -HB.instance Definition _ := GRing.isAdditive.Build {malg G[K]} S (mmap f h) - mmap_is_additive. +HB.instance Definition _ := GRing.isSemiAdditive.Build {malg G[K]} S (mmap f h) + mmap_is_semi_additive. + +Lemma mmap0 : mmap f h 0 = 0 . Proof. exact: raddf0. Qed. +Lemma mmapD : {morph mmap f h: x y / x + y}. Proof. exact: raddfD. Qed. +Lemma mmapMn n : {morph mmap f h: x / x *+ n} . Proof. exact: raddfMn. Qed. + +End SemiAdditive. + +Section Additive. + +Context {K : choiceType} {G : zmodType} {S : ringType}. +Context (f : {additive G -> S}) (h : K -> S). -Local Notation mmap := (mmap f h). +Lemma mmapN : {morph mmap f h: x / - x} . Proof. exact: raddfN. Qed. +Lemma mmapB : {morph mmap f h: x y / x - y}. Proof. exact: raddfB. Qed. +Lemma mmapMNn n : {morph mmap f h: x / x *- n} . Proof. exact: raddfMNn. Qed. -Lemma mmap0 : mmap 0 = 0 . Proof. exact: raddf0. Qed. -Lemma mmapN : {morph mmap: x / - x} . Proof. exact: raddfN. Qed. -Lemma mmapD : {morph mmap: x y / x + y}. Proof. exact: raddfD. Qed. -Lemma mmapB : {morph mmap: x y / x - y}. Proof. exact: raddfB. Qed. -Lemma mmapMn n : {morph mmap: x / x *+ n} . Proof. exact: raddfMn. Qed. -Lemma mmapMNn n : {morph mmap: x / x *- n} . Proof. exact: raddfMNn. Qed. End Additive. +(* TODO: generalize following sections to semirings *) Section CommrMultiplicative. -Context (K : monomType) (R : ringType) (S : ringType). -Context {f : {rmorphism R -> S}} {h : {mmorphism K -> S}}. -Implicit Types (g : {malg R[K]}). +Context {K : monomType} {R : ringType} {S : ringType}. +Context (f : {rmorphism R -> S}) (h : {mmorphism K -> S}). + +Implicit Types (c : R) (g : {malg R[K]}). Lemma mmapZ c g : (c *: g)^[f,h] = f c * g^[f,h]. Proof. @@ -915,14 +945,14 @@ rewrite malgME raddf_sum mulr_suml /=; apply: eq_bigr=> i _. rewrite raddf_sum mulr_sumr /=; apply: eq_bigr=> j _. by rewrite mmapU /= rmorphM mmorphM -mulrA [X in _*X=_]mulrA commr_f !mulrA. Qed. + End CommrMultiplicative. (* -------------------------------------------------------------------- *) Section Multiplicative. -Context (K : monomType) (R : ringType) (S : comRingType). -Context {f : {rmorphism R -> S}} {h : {mmorphism K -> S}}. -Implicit Types (g : {malg R[K]}). +Context {K : monomType} {R : ringType} {S : comRingType}. +Context (f : {rmorphism R -> S}) (h : {mmorphism K -> S}). Lemma mmap_is_multiplicative : multiplicative (mmap f h). Proof. by apply/commr_mmap_is_multiplicative=> g m m'; apply/mulrC. Qed. @@ -930,11 +960,13 @@ Proof. by apply/commr_mmap_is_multiplicative=> g m m'; apply/mulrC. Qed. HB.instance Definition _ := GRing.isMultiplicative.Build {malg R[K]} S (mmap f h) mmap_is_multiplicative. + End Multiplicative. (* -------------------------------------------------------------------- *) Section Linear. -Context (K : monomType) (R : comRingType) {h : {mmorphism K -> R}}. + +Context {K : monomType} {R : comRingType} (h : {mmorphism K -> R}). Lemma mmap_is_linear : scalable_for *%R (mmap idfun h). Proof. by move=> /= c g; rewrite -mul_malgC rmorphM /= mmapC. Qed. @@ -944,22 +976,27 @@ HB.instance Definition _ := mmap_is_linear. End Linear. +(* /TODO *) End MalgMorphism. (* -------------------------------------------------------------------- *) Section MonalgOver. Section Def. -Context {K : choiceType} {G : zmodType}. -Definition monalgOver_pred (S : {pred G}) := - fun g : {malg G[K]} => all (fun m => g@_m \in S) (msupp g). -Definition monalgOver (S : {pred G}) := [qualify a g| monalgOver_pred S g]. +Context {K : choiceType} {G : nmodType}. + +Definition monalgOver_pred (S : {pred G}) : {pred {malg G[K]}} := + fun g => all (fun m => g@_m \in S) (msupp g). +Definition monalgOver (S : {pred G}) := [qualify a g | monalgOver_pred S g]. + End Def. + Arguments monalgOver_pred _ _ _ _ /. (* -------------------------------------------------------------------- *) Section Theory. -Context (K : choiceType) (G : zmodType). + +Context (K : choiceType) (G : nmodType). Local Notation monalgOver := (@monalgOver K G). @@ -985,7 +1022,8 @@ End Theory. (* -------------------------------------------------------------------- *) Section MonalgOverAdd. -Context (K : choiceType) (G : zmodType) (S : addrClosed G). + +Context (K : choiceType) (G : nmodType) (S : addrClosed G). Implicit Types (g : {malg G[K]}). @@ -1005,10 +1043,12 @@ Qed. HB.instance Definition _ := GRing.isAddClosed.Build _ (monalgOver_pred S) monalgOver_addr_closed. + End MonalgOverAdd. (* -------------------------------------------------------------------- *) Section MonalgOverOpp. + Context (K : choiceType) (G : zmodType) (zmodS : zmodClosed G). Local Notation monalgOver := (@monalgOver K G). @@ -1021,10 +1061,13 @@ Qed. HB.instance Definition _ := GRing.isOppClosed.Build _ (monalgOver_pred zmodS) monalgOver_oppr_closed. + End MonalgOverOpp. (* -------------------------------------------------------------------- *) +(* TODO: generalize to R : semiRingType *) Section MonalgOverSemiring. + Context (K : monomType) (R : ringType) (S : semiringClosed R). Local Notation monalgOver := (@monalgOver K R). @@ -1061,14 +1104,15 @@ Proof. move=> g /monalgOverP Sg v Sv; rewrite mmapE rpred_sum //. by move=> /= k; rewrite rpredM. Qed. + End MonalgOverSemiring. +(* /TODO *) -Section MonalgOverRing. -Context (K : monomType) (R : ringType) (ringS : subringClosed R). +HB.instance Definition _ + (K : monomType) (R : ringType) (ringS : subringClosed R) := + GRing.isMulClosed.Build _ (monalgOver_pred ringS) + (monalgOver_mulr_closed K ringS). -HB.instance Definition _ := GRing.isMulClosed.Build _ (monalgOver_pred ringS) - (monalgOver_mulr_closed K ringS). -End MonalgOverRing. End MonalgOver. Arguments monalgOver_pred _ _ _ _ /. @@ -1082,12 +1126,14 @@ HB.mixin Record isMeasure (M : monomType) (mf : M -> nat) := { #[short(type="measure")] HB.structure Definition Measure (M : monomType) := {mf of isMeasure M mf}. +#[deprecated(since="multinomials 2.2.0", note="Use Measure.clone instead.")] Notation "[ 'measure' 'of' f ]" := (Measure.clone _ f _) (at level 0, only parsing) : form_scope. (* -------------------------------------------------------------------- *) Section MMeasure. -Context (M : monomType) (G : zmodType) (mf : measure M). + +Context (M : monomType) (G : nmodType) (mf : measure M). Implicit Types (g : {malg G[M]}). @@ -1117,9 +1163,6 @@ rewrite mmeasureE msuppC; case: (_ == 0)=> /=. by rewrite big_nil. by rewrite big_seq_fset1 mf0. Qed. -Lemma mmeasureN g : mmeasure (-g) = mmeasure g. -Proof. by rewrite mmeasureE msuppN. Qed. - Lemma mmeasureD_le g1 g2 : (mmeasure (g1 + g2) <= maxn (mmeasure g1) (mmeasure g2))%N. Proof. @@ -1151,10 +1194,16 @@ Proof. by rewrite -mmeasure_eq0 -lt0n => /prednK. Qed. Lemma mmeasure_msupp0 g : (mmeasure g == 0%N) = (msupp g == fset0). Proof. by rewrite mmeasure_eq0 msupp_eq0. Qed. + End MMeasure. +Lemma mmeasureN M (G : zmodType) (mf : measure M) (g : {malg G[M]}) : + mmeasure mf (- g) = mmeasure mf g. +Proof. by rewrite mmeasureE msuppN. Qed. + (* -------------------------------------------------------------------- *) Section CmonomDef. + Context (I : choiceType). Record cmonom : predArgType := CMonom { cmonom_val : {fsfun of _ : I => 0%N} }. @@ -1165,6 +1214,7 @@ Fact cmonom_key : unit. Proof. by []. Qed. Definition cmonom_of_fsfun k := locked_with k CMonom. Canonical cmonom_unlockable k := [unlockable fun cmonom_of_fsfun k]. + End CmonomDef. Notation "{ 'cmonom' I }" := (cmonom I) : type_scope. @@ -1179,6 +1229,7 @@ Notation "[ 'cmonom' E | i : P ]" := (* -------------------------------------------------------------------- *) Section CmonomCanonicals. + Context (I : choiceType). HB.instance Definition _ := [isNew for @cmonom_val I]. @@ -1241,6 +1292,7 @@ Qed. HB.instance Definition _ := Choice_isMonomialDef.Build (cmonom I) mulcmA mul0cm mulcm0 mulcm_eq0. HB.instance Definition _ := MonomialDef_isConomialDef.Build (cmonom I) mulcmC. + End CmonomCanonicals. (* -------------------------------------------------------------------- *) @@ -1252,6 +1304,7 @@ Definition mnmwgt {n} (m : cmonom 'I_n) := (* -------------------------------------------------------------------- *) Section CmonomTheory. + Context {I : choiceType}. Implicit Types (m : cmonom I) (i : I). @@ -1343,10 +1396,12 @@ Proof. by rewrite -!mdeg_eq0 mdegM addn_eq0. Qed. Lemma cm1_eq1 i : (U_(i) == 1)%M = false. Proof. by rewrite -mdeg_eq0 mdegU. Qed. + End CmonomTheory. (* -------------------------------------------------------------------- *) Section MWeight. + Context (n : nat). Implicit Types (m : 'X_{1..n}). @@ -1385,6 +1440,7 @@ Qed. Lemma mnmwgt_eq0 m : (mnmwgt m == 0%N) = (m == 1%M). Proof. exact/mf_eq0. Qed. + End MWeight. (* -------------------------------------------------------------------- *) @@ -1392,7 +1448,8 @@ Notation msize := (@mmeasure _ _ mdeg). Notation mweight := (@mmeasure _ _ mnmwgt). Section MSize. -Context (I : choiceType) (G : zmodType). + +Context (I : choiceType) (G : nmodType). Implicit Types (m : cmonom I) (g : {malg G[cmonom I]}). @@ -1411,13 +1468,17 @@ Definition msize0 := @mmeasure0 _ G mdeg. Definition msizeC := @mmeasureC _ G mdeg. Definition msizeD_le := @mmeasureD_le _ G mdeg. Definition msize_sum := @mmeasure_sum _ G mdeg. -Definition msizeN := @mmeasureN _ G mdeg. Definition msize_eq0 := @mmeasure_eq0 _ G mdeg. Definition msize_msupp0 := @mmeasure_msupp0 _ G mdeg. + End MSize. +Definition msizeN (I : choiceType) (G : zmodType) := + @mmeasureN (cmonom I) G mdeg. + (* -------------------------------------------------------------------- *) Section FmonomDef. + Context (I : choiceType). Record fmonom : predArgType := FMonom { fmonom_val : seq I }. @@ -1428,6 +1489,7 @@ Fact fmonom_key : unit. Proof. by []. Qed. Definition fmonom_of_seq k := locked_with k FMonom. Canonical fmonom_unlockable k := [unlockable fun fmonom_of_seq k]. + End FmonomDef. Notation "{ 'fmonom' I }" := (fmonom I) : type_scope. @@ -1436,6 +1498,7 @@ Local Notation mkfmonom s := (fmonom_of_seq fmonom_key s). (* -------------------------------------------------------------------- *) Section FmonomCanonicals. + Context (I : choiceType). HB.instance Definition _ := [isNew for @fmonom_val I]. @@ -1482,6 +1545,7 @@ Proof. by case: m1 m2 => [[|? ?]] [[|? ?]]; rewrite !fmE. Qed. HB.instance Definition _ := Choice_isMonomialDef.Build (fmonom I) fmmulA fmmul1m fmmulm1 fmmul_eq1. + End FmonomCanonicals. (* -------------------------------------------------------------------- *) @@ -1489,6 +1553,7 @@ Definition fdeg (I : choiceType) (m : fmonom I) := size m. (* -------------------------------------------------------------------- *) Section FmonomTheory. + Context {I : choiceType}. Implicit Types (m : fmonom I). @@ -1540,4 +1605,5 @@ Proof. by rewrite -!fdeg_eq0 fdegM addn_eq0. Qed. Lemma fm1_eq1 i : (U_(i) == 1)%M = false. Proof. by rewrite -fdeg_eq0 fdegU. Qed. + End FmonomTheory.