Rank of a matrix as number of pure tensors

Stream: Is there code for X?

[Yaël Dillies]

Do we have the fact that docs#Matrix.rank (or docs#LinearMap.rank, I'm not too bothered) is the minimum number of summands in the decomposition of the matrix into pure tensors?

[Eric Wieser]

What's the lean spelling of "pure tensor" here?

[Yaël Dillies]

By pure tensor, I mean fun i j ↦ f i * g j : Matrix m n α

[Eric Wieser]

So docs#Matrix.vecMulVec ?

[Yaël Dillies]

Didn't know it had a name, but yes

[Junyan Xu]

One inequality is trivial by docs#LinearMap.rank_finset_sum_le because the pure tensors have rank one or zero. For the other inequality, you get a decomposition into pure tensors once you put the matrix into Smith normal form. However mathlib's docs#Submodule.smithNormalForm etc. don't take a LinearMap as input, and I see no obvious way to make use of them. However, over a field, you can take the kernel of your linear map and find a complement of it, and the linear map will map the complement isomorphically onto the range, and you get a decomposition by choosing a basis of the complement, which is mapped to a basis of the range.

[Yaël Dillies]

Ahah, I was worrying about the direction you claimed to be trivial and thought the direction you claimed to be harder was trivial.

[Yaël Dillies]

By which I mean that I don't think you need the Smith normal form. If the matrix M has full rank, then ∑ i, vecMulVec (indicator {i}) (M i) is a decomposition into pure tensors of the correct size. If the matrix doesn't have full rank, I'm pretty sure you can do something similar by picking a basis of M.range and pulling back along M.

[Yaël Dillies]

Does that sound reasonable, Junyan?

[Junyan Xu]

If the matrix M has full rank, then ∑ i, vecMulVec (indicator {i}) (M i) is a decomposition into pure tensors of the correct size.

That's a good point! But thinking in terms of linear maps, if you have a surjective linear map from a higher dimensional space to a lower dimensional space, I think you still need to choose a subspace of the first space that maps isomorphically to the second space, and a complementary subspace that maps to 0, in order to use something like ∑ i, vecMulVec (indicator {i}) (M i).

[Yaël Dillies]

Yep, which is part of the information you get from the SNF, but the SNF gives you much more along the way. Is there a simpler result in this direction?

[Junyan Xu]

For the result in terms of LinearMap, I would define pure tensors using Set.image2 of docs#LinearMap.smulRight (there are also dualTensorHom and LinearMap.smulRightₗ but they're more complicated). Then, I'd take a basis of the kernel and use docs#Basis.extend, then apply the linear map to both sides of docs#Basis.sum_repr to obtain a decomposition into pure tensors, after removing the zero terms (basis elements that are in the kernel) and replacing Basis.repr by docs#Basis.coord. (Probably we should state a lemma that a finite basis of M induces a decomposition of a linear map out of M into pure tensors.)