Matrix rank: proof internals

Proofs behind Complexitylib.Algebraic.LinearAlgebra.MatrixRank: subadditivity, the characterization of rank by nonvanishing square minors, closedness of the bounded-rank locus, block-triangular lower bounds, and the effect of deleting rows and columns.

theorem Algebraic.MatrixRank.Internal.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

theorem Algebraic.MatrixRank.Internal.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

theorem Algebraic.MatrixRank.Internal.exists_linearIndependent_rows {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), LinearIndependent K (A.submatrix f id).row

If k ≤ rank A, some k rows of A are linearly independent.

theorem Algebraic.MatrixRank.Internal.exists_det_submatrix_ne_zero {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, some k × k minor of A is nonzero.

theorem Algebraic.MatrixRank.Internal.card_le_rank_of_det_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 nonzero square minor indexed by ι bounds the rank below by card ι.

theorem Algebraic.MatrixRank.Internal.rank_le_iff_forall_det_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

theorem Algebraic.MatrixRank.Internal.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}

theorem Algebraic.MatrixRank.Internal.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 ≤ (Matrix.fromBlocks A B 0 D).rank

theorem Algebraic.MatrixRank.Internal.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 ≤ (Matrix.fromBlocks A 0 C D).rank

theorem Algebraic.MatrixRank.Internal.rank_le_rank_submatrix_rows_add {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} {m' : Type u_4} [Fintype n] [Fintype m] [Fintype m'] (A : Matrix m n K) (f : m' → m) : A.rank ≤ (A.submatrix f id).rank + Nat.card { i : m // i ∉ Set.range f }

Keeping only the rows in the range of f loses at most one unit of rank per deleted row.

theorem Algebraic.MatrixRank.Internal.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 }

theorem Algebraic.MatrixRank.Internal.natCard_not_mem_range {α : Type u_10} {β : Type u_11} [Fintype α] [Fintype β] {f : α → β} (hf : Function.Injective f) : Nat.card { i : β // i ∉ Set.range f } = Fintype.card β - Fintype.card α