Subadditivity of matrix rank and rank factorization

Over a field, the column space of A + B lies in the sum of the column spaces of A and B, so the rank of a sum of matrices is at most the sum of their ranks (Matrix.rank_add_le). Negation does not change the rank (Matrix.rank_neg), and scaling does not increase it, over any commutative semiring with the strong rank condition (Matrix.rank_smul_le). The natural matrix rank also agrees with the cardinal rank of Matrix.toLin' (Matrix.natCast_rank_eq_rank_toLin'), and a matrix of rank r factors through r-dimensional space (Matrix.exists_eq_mul_rank).

Main results

• Matrix.rank_add_le, Matrix.rank_sub_le: rank is subadditive.
• Matrix.rank_neg: negation preserves rank.
• Matrix.rank_smul_le: scaling does not increase rank.
• Matrix.natCast_rank_eq_rank_toLin': the natural matrix rank agrees with linear-map rank.
• Matrix.exists_eq_mul_rank: rank factorization A = C * D through Fin A.rank.

References

These are standard facts of linear algebra; they are used to compare the ranks of communication matrices in E. Kushilevitz and N. Nisan, Communication Complexity. Matrix.natCast_rank_eq_rank_toLin' is ported from LinearAlgebra/Rank.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

@[simp]

theorem Matrix.rank_neg {m : Type u_1} {n : Type u_2} [Fintype n] {R : Type u_4} [CommRing R] (A : Matrix m n R) : (-A).rank = A.rank

Negation does not change the rank of a matrix.

theorem Matrix.rank_smul_le {m : Type u_1} {n : Type u_2} [Fintype n] {R : Type u_4} [CommSemiring R] [StrongRankCondition R] (c : R) (A : Matrix m n R) : (c • A).rank ≤ A.rank

Scaling a matrix does not increase its rank, over any commutative semiring with the strong rank condition, such as a nontrivial commutative ring: c • A = A (c • 1).

theorem Matrix.rank_add_le {m : Type u_1} {n : Type u_2} {K : Type u_3} [Fintype n] [Field K] (A B : Matrix m n K) : (A + B).rank ≤ A.rank + B.rank

Subadditivity of rank: the rank of a sum of matrices over a field is at most the sum of their ranks.

theorem Matrix.rank_sub_le {m : Type u_1} {n : Type u_2} {K : Type u_3} [Fintype n] [Field K] (A B : Matrix m n K) : (A - B).rank ≤ A.rank + B.rank

The rank of a difference of matrices over a field is at most the sum of their ranks.

theorem Matrix.exists_eq_mul_rank {m : Type u_1} {n : Type u_2} {K : Type u_3} [Fintype n] [Field K] (A : Matrix m n K) : ∃ (C : Matrix m (Fin A.rank) K) (D : Matrix (Fin A.rank) n K), A = C * D

Rank factorization: a matrix with finitely many columns is the product of a matrix with A.rank columns and a matrix with A.rank rows. The first factor lists a basis of the column space; the second records the coordinates of each column in that basis.

theorem Matrix.natCast_rank_eq_rank_toLin' {m : Type u_1} {n : Type u_2} {K : Type u_3} [Fintype n] [Field K] [DecidableEq n] (M : Matrix m n K) : ↑M.rank = (toLin' M).rank

The natural rank of a finite matrix agrees with the cardinal rank of its linear map.