From 7f52199941bc85ee15219080a5a87e900469fbd8 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 | 356 +++++++++++++++++++++++++++------------------------ 1 file changed, 187 insertions(+), 169 deletions(-) diff --git a/src/monalg.v b/src/monalg.v index c958b5d..0695ac5 100644 --- a/src/monalg.v +++ b/src/monalg.v @@ -102,6 +102,7 @@ Export ConomialDefExports. (* -------------------------------------------------------------------- *) Section Monomial. + Context (M : monomType). Local Open Scope monom_scope. @@ -123,16 +124,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. @@ -148,18 +149,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} }. @@ -182,7 +186,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. @@ -215,8 +219,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. @@ -248,24 +255,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. @@ -284,45 +281,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. @@ -330,9 +305,42 @@ 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. @@ -348,18 +356,12 @@ 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. @@ -369,97 +371,66 @@ 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. +Section MalgZmodTheory. -HB.instance Definition _ k := GRing.isAdditive.Build G {malg G[K]} (mkmalgU k) - (monalgU_is_additive k). - -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 >>. @@ -483,21 +454,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. @@ -506,27 +478,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 := @@ -534,25 +506,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. @@ -562,7 +568,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 : @@ -630,7 +636,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))). @@ -664,15 +669,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). @@ -724,14 +729,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. @@ -796,6 +799,22 @@ 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 := @@ -805,11 +824,10 @@ 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. @@ -825,9 +843,7 @@ 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. @@ -949,7 +965,7 @@ 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]. +Definition monalgOver (S : {pred G}) := [qualify a g | monalgOver_pred S g]. End Def. Arguments monalgOver_pred _ _ _ _ /. @@ -1078,6 +1094,7 @@ 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. @@ -1482,6 +1499,7 @@ Proof. by case: m1 m2 => [[|? ?]] [[|? ?]]; rewrite !fmE. Qed. HB.instance Definition _ := Choice_isMonomialDef.Build (fmonom I) fmmulA fmmul1m fmmulm1 fmmul_eq1. + End FmonomCanonicals. (* -------------------------------------------------------------------- *)