Extracting block out of a matrix

Stream: new members

[Vivek Rajesh Joshi]

If I have a Fin-indexed mxn matrix, given some indices i and j, how do I extract the block matrix starting from (i,j) upto (m,n) from the original matrix? I tried using Matrix.toBlock but it isn't giving me Fin-indexed matrix, and I can't figure out how to construct a submatrix from the way it has been defined.

[Yaël Dillies]

Vivek Rajesh Joshi said:

I tried using Matrix.toBlock but it isn't giving me Fin-indexed matrix

Why is that a problem?

[Vivek Rajesh Joshi]

It isn't exactly a problem, just a matter of convenience. In my code so far I've been working with Fin-indexed matrices, so if I can continue that it would be nice. If that isn't possible, I'll try to work with these matrices going forward.

[Eric Wieser]

The general answer is "use docs#Matrix.submatrix", which leaves you the job of constructing the maps you want between the index types

[Eric Wieser]

This should hopefully make it obvious why using Fin here can be annoying, as the map from Fin j to Fin (i + j + k) is a bit fiddly to write down

[Iris Rotarescu]

(deleted)

[Vivek Rajesh Joshi]

So if I want to take the bottom right 2x2 block out of a 3x3 matrix, should I give both the reindex maps as 0 -> 1, 1 -> 1, 2 -> 2?

[Eric Wieser]

Going from a big matrix to a small matrix means your indexing map goes from the small index to the big index; so that map is backwards

[Vivek Rajesh Joshi]

Wouldn't I then have to map 1 to both 0 and 1?

[Vivek Rajesh Joshi]

Never mind, I figured it out. Thanks for the help!

[Mitchell Lee]

The reindexing map is called docs#Finset.orderEmbOfFin

[Mitchell Lee]

I think that it would usually be better not to use Fin-indexed matrices, however.