Subadditivity of matrix rank

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).

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.

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.

@[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.