Rank of Kronecker products

Main results

• LinearMap.finrank_range_tensorProductMap: over a field, dim range (f ⊗ g) = dim range f · dim range g.
• Matrix.rank_kronecker: (A ⊗ₖ B).rank = A.rank * B.rank over a field.
• Matrix.rank_piKronecker: the k-th Kronecker power piKronecker k A (indexed by k-tuples) has rank A.rank ^ k.
• Matrix.rank_kronecker_one: (A ⊗ₖ (1 : Matrix p p K)).rank = Fintype.card p * A.rank.

The general statement goes through linear maps: with standard bases A ⊗ₖ B is the matrix of TensorProduct.map (toLin A) (toLin B) (Matrix.toLin_kronecker), and map f g factors as the surjection map f.rangeRestrict g.rangeRestrict followed by the inclusion range f ⊗ range g → P ⊗ Q, which is injective because vector spaces are flat.

theorem LinearMap.finrank_range_tensorProductMap {K : Type u_1} [Field K] {M : Type u_2} {N : Type u_3} {P : Type u_4} {Q : Type u_5} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q] [Module K M] [Module K N] [Module K P] [Module K Q] [FiniteDimensional K M] [FiniteDimensional K N] (f : M →ₗ[K] P) (g : N →ₗ[K] Q) : Module.finrank K ↥(TensorProduct.map f g).range = Module.finrank K ↥f.range * Module.finrank K ↥g.range

Over a field, the image of f ⊗ g has dimension dim range f · dim range g.

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

The rank of a Kronecker product is the product of the ranks (over a field).

theorem Matrix.rank_kronecker_one {m : Type u_1} {n : Type u_2} {p : Type u_3} {K : Type u_4} [Field K] [Fintype n] [Fintype p] [DecidableEq p] (A : Matrix m n K) : (kroneckerMap (fun (x1 x2 : K) => x1 * x2) A 1).rank = Fintype.card p * A.rank

The rank of A ⊗ₖ 1 is Fintype.card p times the rank of A.

def Matrix.piKronecker {α : Type u_5} {β : Type u_6} {R : Type u_7} [CommMonoid R] (k : ℕ) (A : Matrix α β R) : Matrix (Fin k → α) (Fin k → β) R

The k-th Kronecker power of A, indexed by tuples: entry ∏ i, A (r i) (c i).

Equations

• Matrix.piKronecker k A r c = ∏ i : Fin k, A (r i) (c i)

theorem Matrix.piKronecker_succ {α : Type u_5} {β : Type u_6} {R : Type u_7} [CommMonoid R] (k : ℕ) (A : Matrix α β R) : piKronecker (k + 1) A = (kroneckerMap (fun (x1 x2 : R) => x1 * x2) A (piKronecker k A)).submatrix ⇑(Fin.consEquiv fun (x : Fin (k + 1)) => α).symm ⇑(Fin.consEquiv fun (x : Fin (k + 1)) => β).symm

theorem Matrix.rank_piKronecker {α : Type u_5} {β : Type u_6} {K : Type u_7} [Field K] [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (k : ℕ) (A : Matrix α β K) : (piKronecker k A).rank = A.rank ^ k