Generalize mmap

[pi8027]

Before this change, mmap f h : {malg R[K]} -> S was canonically a semiring morphism under the context:

K : monomType
R : pzSemiRingType
S : *com*PzSemiRingType
f : {rmorphism R -> S}
h : {mmorphism K -> S}

and it was not general enough. For example, S cannot be square matrices as they are not commutative.

In this PR, mmap (GRing.in_alg _) h is canonically a semiring morphism under the context:

K : monomType
R : pzSemiRingType
S : semiAlgType R
h : {mmorphism K -> S}

which minimizes the commutativity assumption.

Unfortunately, it currently lacks an easy way to get this semiring morphism instance under the former context.

[CohenCyril]

This piece of the new telescope

Context {R : pzSemiRingType} {S : semiAlgType R}.

is equivalent to

Context {R : pzSemiRingType} {S : nzSemiRingType} (f : {rmorphism R -> S}).
Hypothesis comm_f : forall a x, GRing.comm (f a) x.

So, unless I miss something, this new context is less general...

Indeed

From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra.
Import GRing.Theory.
Local Open Scope ring_scope.

Section AlgToMor.
Context {R : pzSemiRingType} {S : semiAlgType R}.
Check (in_alg _ : R -> S) : {rmorphism R -> S}.
Check S : nzSemiRingType.
Check S : lSemiAlgType R.
Lemma commr_in_alg (a : R) (x : S) : GRing.comm (a%:A) x.
Proof. by rewrite /GRing.comm mulr_algl mulr_algr. Qed.
End AlgToMor.

HB.factory Record NZSemiRing_isAlg {R : pzSemiRingType}
  S of GRing.NzSemiRing S := {
    in_alg : {rmorphism R -> S};
    commr_in_alg : forall a x, GRing.comm (in_alg a) x
  }.
HB.builders Context R S of NZSemiRing_isAlg R S.
Let scale : R -> S -> S := fun x y => in_alg x * y.
Local Infix "*:" := scale.
Let scalerA (a b : R) (v : S) : a *: (b *: v) = (a * b) *: v.
Proof. by rewrite /scale rmorphM mulrA. Qed.
Let scale0r (v : S) : 0 *: v = 0.
Proof. by rewrite /scale rmorph0 mul0r. Qed.
Let scale1r : left_id 1 scale.
Proof. by move=> x; rewrite /scale rmorph1 mul1r. Qed.
Let scalerDr : right_distributive scale +%R.
Proof. by move=> x; exact: mulrDr. Qed.
Let scalerDl (v : S) : {morph scale^~ v : a b / a + b >-> a + b}.
Proof. by move=> a b; rewrite /scale rmorphD mulrDl. Qed.
HB.instance Definition _ := @GRing.Nmodule_isLSemiModule.Build
  R S scale scalerA scale0r scale1r scalerDr scalerDl.
Let scaleEmorph : *:%R = scale. Proof. by []. Qed.
Let scalerAl (a : R) (u v : S) : (a *: (u * v))%R = a *: u * v.
Proof. exact: mulrA. Qed.
HB.instance Definition _ :=
  GRing.LSemiModule_isLSemiAlgebra.Build R S scalerAl.
Let scalerAr (k : R) (x y : S) : (k *: (x * y))%R = x * (k *: y).
Proof. by rewrite !scaleEmorph /scale !commr_in_alg mulrA. Qed.
HB.instance Definition _ := GRing.LSemiAlgebra_isSemiAlgebra.Build R S scalerAr.
HB.end.

[pi8027]

If what you mean by "less general" is the difference between pz and nz, we should fix it in MathComp by introducing potentially-zero algebra structures (math-comp/math-comp#1386).

The main issue with the old CommrMultiplicative section is that the commr_f hypothesis makes the instance unusable. However, the version I proposed applies only to mmap in_alg _ where in_alg x := x *: 1, which might be a bit too specific. Another way out is to define a special ring morphism structure extended with the commutativity of scalars (bundling the commr_f hypothesis in the ring morphism structure), but it looks a bit too ad-hoc.