Ssreflect Users Discussion List

[Cyril <>]

Dear Xavier,

On 23/05/2018 11:44, Xavier Allamigeon wrote:
> Dear MathComp-list,
>
> I was wondering whether there is a way to manipulate matrices over a 
> subring and mix them with matrices over the original ring.
>
> More precisely, suppose that R has type ringType, and that R' is a 
> subtype of R equipped with a structure of subring (provided by 
> SubRingPred). Then, M[R']_(m,n) should be a subgroup of M[R]_(m,n), but 
> I don't see any construction in MathComp to get this structure.
> For instance, if A, B : M[R']_(m,n), and C : M[R]_(n,p), then I would 
> like to recover that
> A *m C + B *m C = (A + B) *m C
> where the addition on the RHS is then one over M[R']_(m,n).
> I cannot even find any default coercion from M[R']_(m,n) to M[R]_(m,n). 
> Should it be defined by hand?
>
> In my case, R' turns out to be a field, and I really need to exploit 
> this special structure since then I'll be able to use the properties 
> defined in mxalgebra.
>
> Any hint?

Whenever you want to show something that requires to work on 'M[R'] 
because R' is a field, I guess that in the current state of the library, 
you must work on R'. But try to do so in a delimited way, and you may 
then use map_mx to explicitly coerce from R' to R.

However, when mixing both R and R', the best practice is to always work 
in the "biggest type" R as often a possible, and use directly the 
characteristic predicate you use to build R' instead of R' itself.
To that end, you then need the analogous of polyOver, which I started 
defining here:
https://github.com/CohenCyril/spectral/blob/master/theories/spectral.v#L684-L746 
(mxOver).

Best regards,
--
Cyril
PS: Sorry for the duplicate