From 7bec33ee5947e69a0572549f84b728c9d398440a Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 26 Nov 2024 18:20:16 +0100 Subject: [PATCH] WIP --- src/monalg.v | 94 ++++++++++++++++++++++++++-------------------------- 1 file changed, 47 insertions(+), 47 deletions(-) diff --git a/src/monalg.v b/src/monalg.v index 66e8e70..57842fd 100644 --- a/src/monalg.v +++ b/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,18 +461,8 @@ 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. @@ -477,10 +470,11 @@ 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. @@ -488,7 +482,7 @@ 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.