Matrices with values in a module

Stream: new members

[Boris Bilich]

If M is an R-module, then we can multiply n-by-m matrices with R-entries with m-by-k matrices with entries in M. Is this implemented in mathlib? It seems to me that Mathlib.Data.Matrix.Mulonly considers the case with entries in the same type.

[Violeta Hernández]

Is there a smul instance?

[Boris Bilich]

Violeta Hernández said:

Is there a smul instance?

Yes. I am formalizing abstract operator systems and in this theory multiplication of complex matrices with matrices with values in a vector space is all over the place.

[Weiyi Wang]

I think Violeta's question is "have you tried \smul instead of * and see if it works?". Not that we know it works. Just a guess

[Wang Jingting]

@loogle Matrix, |- SMul _ _

[loogle]

:search: Matrix.smul, ModularGroup.SLOnGLPos, and 6 more

[Wang Jingting]

It seems to me that we only have the scalar multiplication by an element in R for Matrix.smul

[Boris Bilich]

So, it seems to me that if there is an instance of HMul or HSMul α β γ and an instance AddCommSemigroup γ, there should be an instance of HMul (Matrix n m α) (Matrix m k β) (Matrix n k γ). Does it make sense to have it in mathlib?

[Snir Broshi]

Is there a way to cast the R matrix to an M matrix? There doesn't seem to be
Module R M → Module (Matrix n m R) (Matrix n m M)

[Kevin Buzzard]

I don't think that that's mathematically correct

[Kevin Buzzard]

And when you make these things correct then they'll probably either not be valid instances or will cause diamonds when R is itself a matrix ring so probably won't be acceptable in mathlib. They could be definitions though and locally switched on as instances