The rank of a Kronecker product

Over a field, a matrix of rank r factors through r-dimensional space (Matrix.exists_eq_mul_rank). Applying this to both factors of a Kronecker product and using Matrix.mul_kronecker_mul bounds the rank of A ⊗ₖ B by A.rank * B.rank (Matrix.rank_kronecker_le). Equality holds as well, but only the upper bound is proved here.

Main results

• Matrix.rank_kronecker_le: (A ⊗ₖ B).rank ≤ A.rank * B.rank.

References

These are standard facts of linear algebra. The Kronecker bound is the "≤" half of the multiplicativity of rank used for Claim 7(3) of N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, pp. 6–7.

theorem Matrix.rank_kronecker_le {K : Type u_1} [Field K] {l : Type u_2} {m : Type u_3} {n : Type u_4} {p : Type u_5} [Fintype m] [Fintype p] (A : Matrix l m K) (B : Matrix n p K) : (kroneckerMap (fun (x1 x2 : K) => x1 * x2) A B).rank ≤ A.rank * B.rank

The rank of a Kronecker product is at most the product of the ranks.