search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.23k stars 185 forks source link

interaction of scalar and matrix multiplication #1976

Closed Alizter closed 1 month ago

Alizter commented 1 month ago

We show that scalar multiplication distributes over the first factor of matrix multiplication. We also clarify that something similar should hold for right multiplication and the right factor.

We also clarify an earlier comment about an R-algebra over a noncommutative ring R. It's not a priori clear what the definition should be in this case. R-matrices form an R-bimodule with a product that interacts with the left and right actions nicely. This might be a good candidate for a definition, but it is not clear if it is standard.

When the ring R is commutative then it is clear that this becomes the usual definition of an associative algebra. Equivalently, a map R -> Z(A) where A is the algebra and Z is the center.

Alizter commented 1 month ago

I think it should be possible to define matrices as a vector of columns. It might be worth trying if we move to defining them as functions as mentioned in #1979.