Rank inequalities for sums and block triangular matrices

Throughout, K is a field. The nullity of a matrix A is expressed as Module.finrank K (LinearMap.ker A.mulVecLin); by Matrix.rank_add_finrank_ker_mulVecLin it equals Fintype.card n - A.rank when A has columns indexed by n.

Main results

• Matrix.rank_add_le: (A + B).rank ≤ A.rank + B.rank.
• Matrix.rank_add_finrank_ker_mulVecLin: rank–nullity for matrices.
• Matrix.finrank_ker_mulVecLin_add_le: if U is invertible, the nullity of U + E is at most E.rank; Matrix.finrank_ker_mulVecLin_sub_mul_le: the nullity of U - P * Q is at most the number of columns of P.
• Matrix.finrank_ker_mulVecLin_fromBlocks_zero₂₁_le: the nullity of fromBlocks A B 0 D is at most the sum of the nullities of A and D.
• Matrix.rank_add_rank_le_rank_fromBlocks_zero₂₁: A.rank + D.rank ≤ (fromBlocks A B 0 D).rank.
• Matrix.rank_fromBlocks_zero₂₁_le_left, Matrix.rank_fromBlocks_zero₂₁_le_right: upper bounds for the rank of fromBlocks A B 0 D in terms of the rank of one diagonal block.

Related

Mathlib has LinearMap.rank_add_le (cardinal rank of linear maps) but no Matrix.rank_add_le. Independently, Matrix.rank_add_le and rank_add_rank_le_rank_fromBlocks_zero₂₁ over a field also appear in complexitylib (https://github.com/SamuelSchlesinger/complexitylib, Complexitylib/Algebraic/LinearAlgebra/MatrixRank/Internal.lean).

This file is the single home of these rank facts in this repository: FreeLocus and FreeLocusCertificate import them.

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

Subadditivity of the rank of matrices.

@[simp]

theorem Matrix.rank_neg {m : Type u_2} {n : Type u_3} {K : Type u_6} [Field K] [Fintype n] (A : Matrix m n K) : (-A).rank = A.rank

Negating a matrix does not change its rank.

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

The rank of a difference is at most the sum of the ranks.

theorem Matrix.rank_add_finrank_ker_mulVecLin {m : Type u_2} {n : Type u_3} {K : Type u_6} [Field K] [Fintype n] (A : Matrix m n K) : A.rank + Module.finrank K ↥A.mulVecLin.ker = Fintype.card n

Rank–nullity for matrices: the rank plus the dimension of the kernel of A.mulVecLin is the number of columns.

theorem Matrix.finrank_ker_mulVecLin_add_le {n : Type u_3} {K : Type u_6} [Field K] [Fintype n] [DecidableEq n] {U : Matrix n n K} (hU : IsUnit U) (E : Matrix n n K) : Module.finrank K ↥(U + E).mulVecLin.ker ≤ E.rank

If U is invertible, the nullity of U + E is at most the rank of E.

theorem Matrix.finrank_ker_mulVecLin_sub_le {n : Type u_3} {K : Type u_6} [Field K] [Fintype n] [DecidableEq n] {U : Matrix n n K} (hU : IsUnit U) (E : Matrix n n K) : Module.finrank K ↥(U - E).mulVecLin.ker ≤ E.rank

If U is invertible, the nullity of U - E is at most the rank of E.

theorem Matrix.finrank_ker_mulVecLin_sub_mul_le {n : Type u_3} {o : Type u_4} {K : Type u_6} [Field K] [Fintype n] [DecidableEq n] [Fintype o] {U : Matrix n n K} (hU : IsUnit U) (P : Matrix n o K) (Q : Matrix o n K) : Module.finrank K ↥(U - P * Q).mulVecLin.ker ≤ Fintype.card o

If U is invertible and P has columns indexed by o, the nullity of U - P * Q is at most Fintype.card o.

theorem Matrix.finrank_ker_mulVecLin_fromBlocks_zero₂₁_le {l : Type u_1} {n : Type u_3} {o : Type u_4} {p : Type u_5} {K : Type u_6} [Field K] [Fintype n] [Fintype o] (A : Matrix l n K) (B : Matrix l o K) (D : Matrix p o K) : Module.finrank K ↥(fromBlocks A B 0 D).mulVecLin.ker ≤ Module.finrank K ↥A.mulVecLin.ker + Module.finrank K ↥D.mulVecLin.ker

The nullity of a block upper triangular matrix is at most the sum of the nullities of its diagonal blocks.

theorem Matrix.rank_add_rank_le_rank_fromBlocks_zero₂₁ {l : Type u_1} {n : Type u_3} {o : Type u_4} {p : Type u_5} {K : Type u_6} [Field K] [Fintype n] [Fintype o] (A : Matrix l n K) (B : Matrix l o K) (D : Matrix p o K) : A.rank + D.rank ≤ (fromBlocks A B 0 D).rank

The rank of a block upper triangular matrix is at least the sum of the ranks of its diagonal blocks.

theorem Matrix.rank_fromBlocks_zero₂₁_le_left {l : Type u_1} {n : Type u_3} {o : Type u_4} {p : Type u_5} {K : Type u_6} [Field K] [Fintype n] [Fintype o] [Finite l] (A : Matrix l n K) (B : Matrix l o K) (D : Matrix p o K) : (fromBlocks A B 0 D).rank ≤ A.rank + Fintype.card o

The rank of fromBlocks A B 0 D is at most the rank of A plus the number of columns of D.

theorem Matrix.rank_fromBlocks_zero₂₁_le_right {l : Type u_1} {n : Type u_3} {o : Type u_4} {p : Type u_5} {K : Type u_6} [Field K] [Fintype n] [Fintype o] [Fintype l] [Finite p] (A : Matrix l n K) (B : Matrix l o K) (D : Matrix p o K) : (fromBlocks A B 0 D).rank ≤ Fintype.card l + D.rank

The rank of fromBlocks A B 0 D is at most the number of rows of A plus the rank of D.