Multiplying sparse infinite matricies.

Stream: Is there code for X?

[Wrenna Robson]

In theory, would it be possible to define matrix multiplication for infinite matrices where enough of the entries are zero that you only have finitely supported sums? Like, if row i of M has finitely many non-zero entries, and column j of N has finitely many non-zero entries, then entry ij of MN is defined in terms of a sum of finitely many non-zero entries. So as long as every row of M has finitely many non-zero entries (that is to say, for all i, j -> M i j is a finitely supported function) and vice-versa for N and columns, you can perform the multiplication, no?

Do we already have the machinery to do this?

[Eric Wieser]

You could write the multiplication using tsum I guess

[Yaël Dillies]

Let me also mention #11656, that does exactly this for locally finite orders.

[Wrenna Robson]

Oh, that's cool.

[Kevin Buzzard]

You only need one of (every row of M has finitely many non-zero entries) and (every column of N has finitely many non-zero entries) to be able to do the multiplication. You see this with matrices representing finite rank maps. Columns are all finitely supported but rows are not in general (e.g. the projection sending each $e_i$ to $e_1$ has matrix with first line all 1s, but you can still multiply it by another finite rank matrix).

[Wrenna Robson]

Oh, so you do, yes.

[Wrenna Robson]

I suppose what this correspond to is: if you have something of type f : m → n →₀ α, you can turn this into a matrix M : m → n → α by M i j = f i j or you can turn it into M : n → m → α via M j i = f i j.

What we're talking about here, then, are operations (m → n →₀ α) → matrix n k → matrix m k and matrix m n → (k → n →₀ α) → matrix m k?