WIP

src/monalg.v

@@ -449,7 +449,10 @@ Qed.
 Lemma fgscaleA c1 c2 g : c1 *:g (c2 *:g g) = (c1 * c2) *:g g.
 Proof. by apply/malgP=> x; rewrite !fgscaleE mulrA. Qed.
 
-Lemma fgscale1r D: 1 *:g D = D.
+Lemma fgscale0r g : 0 *:g g = 0.
+Proof. by apply/malgP=> k; rewrite fgscaleE mul0r mcoeff0. Qed.
+
+Lemma fgscale1r g : 1 *:g g = g.
 Proof. by apply/malgP=> k; rewrite !fgscaleE mul1r. Qed.
 
 Lemma fgscaleDr c g1 g2 : c *:g (g1 + g2) = c *:g g1 + c *:g g2.
@@ -458,37 +461,28 @@ 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.
 
-End MalgSemiRingTheory.
-
-(* -------------------------------------------------------------------- *)
-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.
+HB.instance Definition _ := GRing.Nmodule_isLSemiModule.Build R {malg R [K]}
+  fgscaleA fgscale0r 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.
 
-(* FIXME: make the production of a LRMorphism fail below *)
-(* HB.instance Definition _ m := *)
-(*   GRing.isLinear.Build R [lmodType R of {malg R[K]}] R *%R (mcoeff m) *)
-(*     (fun c g => mcoeffZ c g m). *)
+(* FIXME: this instance has to be declared after the RMorphism instance of    *)
+(* [mcoeff 1%M] to produce the LRMorphism instance.                           *)
+(* HB.instance Definition _ k := *)
+(*   GRing.isSemilinear.Build R {malg R[K]} R *%R (mcoeff k) *)
+(*     (fun c g => mcoeffZ c g k, mcoeffD k). *)
 
 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 MalgRingTheory.
+End MalgSemiRingTheory.
 
 (* -------------------------------------------------------------------- *)
 Section MalgLmodTheoryIntegralDomain.
@@ -586,8 +580,8 @@ move=> k _ /mcoeff_outdom g1k.
 by rewrite big1 => // k' _; rewrite g1k mul0r monalgU0.
 Qed.
 
-Lemma fgmulrw (d1 d2 : {fset K}) g1 g2 : msupp g1 `<=` d1 -> msupp g2 `<=` d2
-  -> fgmul g1 g2 = \sum_(k2 <- d2) \sum_(k1 <- d1) g1 *M_[k1, k2] g2.
+Lemma fgmulrw (d1 d2 : {fset K}) g1 g2 : msupp g1 `<=` d1 -> msupp g2 `<=` d2 ->
+  fgmul g1 g2 = \sum_(k2 <- d2) \sum_(k1 <- d1) g1 *M_[k1, k2] g2.
 Proof. by move=> le_d1 le_d2; rewrite (fgmullw le_d1 le_d2) exchange_big. Qed.
 
 Definition fgmullwl (d1 : {fset K}) {g1 g2} (le : msupp g1 `<=` d1) :=
@@ -678,6 +672,10 @@ HB.instance Definition _ := GRing.Nmodule_isSemiRing.Build {malg R[K]}
 
 End MalgSemiRingType.
 
+(* TODO: HB.saturate *)
+HB.instance Definition _ (K : monomType) (R : ringType) :=
+  GRing.SemiRing.on {malg R[K]}.
+
 (* -------------------------------------------------------------------- *)
 Section MalgSemiRingTheory.
 
@@ -799,45 +797,39 @@ rewrite !raddf_sum !big1 ?addr0 //= => k; rewrite in_fsetD1 => /andP [ne1_k _].
 by rewrite mcoeffU mul1m (negbTE ne1_k).
 Qed.
 
+(* FIXME: this instance declaration fails if the [Linear] instance is         *)
+(* declared first.                                                            *)
 HB.instance Definition _ :=
-  GRing.isMultiplicative.Build {malg R[K]} R (@mcoeff K R 1%M)
+  GRing.isMultiplicative.Build {malg R[K]} R (mcoeff 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 :=
-  GRing.isScalable.Build R {malg R[K]} R *%R (mcoeff m)
-    (fun c => (mcoeffZ c)^~ 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 R[K]}
-  fgscaleAl.
+HB.instance Definition _ :=
+  GRing.LSemiModule_isLSemiAlgebra.Build R {malg R[K]} fgscaleAl.
 
-End MalgRingTheory.
+End MalgSemiRingTheory.
+
+(* FIXME: the [Linear] instance moved from above *)
+HB.instance Definition _ (K : choiceType) (R : semiRingType) k :=
+  GRing.isScalable.Build R {malg R[K]} R *%R (mcoeff k)
+    (fun c g => mcoeffZ c g k).
+
+(* FIXME: HB.saturate? *)
+HB.instance Definition _ (K : monomType) (R : semiRingType) :=
+  GRing.Linear.on (mcoeff 1%M : {malg R[K]} -> R).
 
 (* -------------------------------------------------------------------- *)
-Section MalgComRingType.
+Section MalgComSemiRingType.
 
-Context {K : conomType} {R : comRingType}.
+Context {K : conomType} {R : comSemiRingType}.
 
 Lemma fgmulC : @commutative {malg R[K]} _ *%R.
 Proof.
@@ -846,12 +838,20 @@ apply/eq_bigr=> /= k1 _; apply/eq_bigr=> /= k2 _.
 by rewrite mulrC [X in X==k]mulmC.
 Qed.
 
-HB.instance Definition _ := GRing.Ring_hasCommutativeMul.Build (malg K R)
-  fgmulC.
+HB.instance Definition _ :=
+  GRing.SemiRing_hasCommutativeMul.Build {malg R[K]} fgmulC.
+
+HB.instance Definition _ :=
+  GRing.LSemiAlgebra_isComSemiAlgebra.Build R {malg R[K]}.
 
-HB.instance Definition _ := GRing.Lalgebra_isComAlgebra.Build R {malg R[K]}.
+End MalgComSemiRingType.
 
-End MalgComRingType.
+(* FIXME: HB.saturate *)
+HB.instance Definition _ (K : monomType) (R : ringType) :=
+  GRing.Lmodule.on {malg R[K]}.
+HB.instance Definition _ (K : conomType) (R : comRingType) :=
+  GRing.Lmodule.on {malg R[K]}.
+(* /FIXME *)
 
 (* -------------------------------------------------------------------- *)
 Section MalgMorphism.