Matrix rank: subadditivity, minors, semicontinuity, blocks, and deletions

Facts about Matrix.rank over a field K that Mathlib does not state directly. Ranks are natural numbers and all index types are finite.

• Subadditivity: Matrix.rank_add_le and Matrix.rank_sum_le.
• Minors: rank A ≥ k if and only if some k × k submatrix of A has nonzero determinant (Matrix.le_rank_iff_exists_det_submatrix_ne_zero); equivalently rank A ≤ r if and only if every (r + 1) × (r + 1) minor vanishes (Matrix.rank_le_iff_forall_det_submatrix_eq_zero). A nonzero minor indexed by any finite type ι gives card ι ≤ rank A (Matrix.card_le_rank_of_det_submatrix_ne_zero).
• Semicontinuity: over a topological field whose points are closed, the matrices of rank at most r form a closed set (Matrix.isClosed_setOf_rank_le), so rank is lower semicontinuous (Matrix.lowerSemicontinuous_rank): a limit of matrices of rank at most r has rank at most r.
• Block-triangular matrices: the rank of fromBlocks A B 0 D or fromBlocks A 0 C D is at least rank A + rank D, whatever the off-diagonal block and whether or not the diagonal blocks are square or invertible.
• Deleting rows and columns: restricting to the rows in the range of f and the columns in the range of g lowers the rank by at most the number of deleted rows plus the number of deleted columns (Matrix.rank_le_rank_submatrix_add, Matrix.rank_le_rank_submatrix_add_card_sub).

Rank is invariant under permuting rows and columns by Mathlib's Matrix.rank_submatrix (for equivalences) and Matrix.rank_reindex; Mathlib's Matrix.rank_submatrix_le says that deleting rows and columns does not increase rank.

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

Rank is subadditive.

theorem Matrix.rank_sum_le {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype n] {ι : Type u_6} (s : Finset ι) (A : ι → Matrix m n K) : (∑ i ∈ s, A i).rank ≤ ∑ i ∈ s, (A i).rank

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

theorem Matrix.card_le_rank_of_det_submatrix_ne_zero {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype n] {ι : Type u_6} [Fintype ι] [DecidableEq ι] (A : Matrix m n K) (f : ι → m) (g : ι → n) (h : (A.submatrix f g).det ≠ 0) : Fintype.card ι ≤ A.rank

A square submatrix indexed by ι with nonzero determinant forces card ι ≤ rank A.

theorem Matrix.exists_det_submatrix_ne_zero_of_le_rank {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype n] [Fintype m] {k : ℕ} (A : Matrix m n K) (hk : k ≤ A.rank) : ∃ (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ≠ 0

If k ≤ rank A, then some k × k minor of A is nonzero.

theorem Matrix.le_rank_iff_exists_det_submatrix_ne_zero {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype n] [Fintype m] (A : Matrix m n K) (k : ℕ) : k ≤ A.rank ↔ ∃ (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ≠ 0

Rank by minors. k ≤ rank A if and only if some k × k minor of A is nonzero.

theorem Matrix.rank_le_iff_forall_det_submatrix_eq_zero {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype n] [Fintype m] (A : Matrix m n K) (r : ℕ) : A.rank ≤ r ↔ ∀ (f : Fin (r + 1) → m) (g : Fin (r + 1) → n), (A.submatrix f g).det = 0

Rank by minors. rank A ≤ r if and only if every (r + 1) × (r + 1) minor of A vanishes.

theorem Matrix.isClosed_setOf_rank_le {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype n] [Fintype m] [TopologicalSpace K] [IsTopologicalRing K] [T1Space K] (r : ℕ) : IsClosed {A : Matrix m n K | A.rank ≤ r}

The matrices of rank at most r form a closed set.

theorem Matrix.lowerSemicontinuous_rank {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype n] [Fintype m] [TopologicalSpace K] [IsTopologicalRing K] [T1Space K] : LowerSemicontinuous fun (A : Matrix m n K) => A.rank

Lower semicontinuity of rank.

theorem Matrix.rank_add_rank_le_rank_fromBlocks_zero₂₁ {K : Type u_1} [Field K] {m₁ : Type u_6} {m₂ : Type u_7} {n₁ : Type u_8} {n₂ : Type u_9} [Fintype m₁] [Fintype m₂] [Fintype n₁] [Fintype n₂] (A : Matrix m₁ n₁ K) (B : Matrix m₁ n₂ K) (D : Matrix m₂ n₂ 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_add_rank_le_rank_fromBlocks_zero₁₂ {K : Type u_1} [Field K] {m₁ : Type u_6} {m₂ : Type u_7} {n₁ : Type u_8} {n₂ : Type u_9} [Fintype m₁] [Fintype m₂] [Fintype n₁] [Fintype n₂] (A : Matrix m₁ n₁ K) (C : Matrix m₂ n₁ K) (D : Matrix m₂ n₂ K) : A.rank + D.rank ≤ (fromBlocks A 0 C D).rank

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

theorem Matrix.rank_le_rank_submatrix_add {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} {m' : Type u_4} {n' : Type u_5} [Fintype n] [Fintype m] [Fintype m'] [Fintype n'] (A : Matrix m n K) (f : m' → m) (g : n' → n) : A.rank ≤ (A.submatrix f g).rank + Nat.card { i : m // i ∉ Set.range f } + Nat.card { j : n // j ∉ Set.range g }

Deleting rows and columns. Keeping the rows in the range of f and the columns in the range of g lowers the rank by at most the number of rows outside the range of f plus the number of columns outside the range of g.

theorem Matrix.rank_le_rank_submatrix_add_card_sub {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} {m' : Type u_4} {n' : Type u_5} [Fintype n] [Fintype m] [Fintype m'] [Fintype n'] (A : Matrix m n K) {f : m' → m} {g : n' → n} (hf : Function.Injective f) (hg : Function.Injective g) : A.rank ≤ (A.submatrix f g).rank + (Fintype.card m - Fintype.card m') + (Fintype.card n - Fintype.card n')

Deleting rows and columns, for injective reindexings: deleting card m - card m' rows and card n - card n' columns lowers the rank by at most their total number.