Rank of matrices

The rank of a matrix A is defined to be the rank of range of the linear map corresponding to A. This definition does not depend on the choice of basis, see Matrix.rank_eq_finrank_range_toLin.

Main declarations

• Matrix.rank: the rank of a matrix

noncomputable def Matrix.rank {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] (A : Matrix m n R) : ℕ

The rank of a matrix is the rank of its image.

Equations

• A.rank = Module.finrank R ↥(LinearMap.range A.mulVecLin)

@[simp]

theorem Matrix.rank_one {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [StrongRankCondition R] [DecidableEq n] : Matrix.rank 1 = Fintype.card n

@[simp]

theorem Matrix.rank_zero {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [Nontrivial R] : Matrix.rank 0 = 0

theorem Matrix.rank_le_card_width {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [StrongRankCondition R] (A : Matrix m n R) : A.rank ≤ Fintype.card n

theorem Matrix.rank_le_width {R : Type u_5} [CommRing R] [StrongRankCondition R] {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) : A.rank ≤ n

theorem Matrix.rank_mul_le_left {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} [Fintype n] [Fintype o] [CommRing R] [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) : (A * B).rank ≤ A.rank

theorem Matrix.rank_mul_le_right {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} [Fintype n] [Fintype o] [CommRing R] [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) : (A * B).rank ≤ B.rank

theorem Matrix.rank_mul_le {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} [Fintype n] [Fintype o] [CommRing R] [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) : (A * B).rank ≤ A.rank ⊓ B.rank

theorem Matrix.rank_unit {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [StrongRankCondition R] [DecidableEq n] (A : (Matrix n n R)ˣ) : (↑A).rank = Fintype.card n

theorem Matrix.rank_of_isUnit {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [StrongRankCondition R] [DecidableEq n] (A : Matrix n n R) (h : IsUnit A) : A.rank = Fintype.card n

@[simp]

theorem Matrix.rank_mul_eq_left_of_isUnit_det {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [DecidableEq n] (A : Matrix n n R) (B : Matrix m n R) (hA : IsUnit A.det) : (B * A).rank = B.rank

Right multiplying by an invertible matrix does not change the rank

@[simp]

theorem Matrix.rank_mul_eq_right_of_isUnit_det {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [Fintype m] [DecidableEq m] (A : Matrix m m R) (B : Matrix m n R) (hA : IsUnit A.det) : (A * B).rank = B.rank

Left multiplying by an invertible matrix does not change the rank

theorem Matrix.rank_submatrix_le {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [StrongRankCondition R] [Fintype m] (f : n → m) (e : n ≃ m) (A : Matrix m m R) : (A.submatrix f ⇑e).rank ≤ A.rank

Taking a subset of the rows and permuting the columns reduces the rank.

theorem Matrix.rank_reindex {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [Fintype m] (e₁ e₂ : m ≃ n) (A : Matrix m m R) : ((Matrix.reindex e₁ e₂) A).rank = A.rank

@[simp]

theorem Matrix.rank_submatrix {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [Fintype m] (A : Matrix m m R) (e₁ e₂ : n ≃ m) : (A.submatrix ⇑e₁ ⇑e₂).rank = A.rank

theorem Matrix.rank_eq_finrank_range_toLin {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [Finite m] [DecidableEq n] {M₁ : Type u_6} {M₂ : Type u_7} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (A : Matrix m n R) (v₁ : Basis m R M₁) (v₂ : Basis n R M₂) : A.rank = Module.finrank R ↥(LinearMap.range ((Matrix.toLin v₂ v₁) A))

theorem Matrix.rank_le_card_height {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] [Fintype m] [StrongRankCondition R] (A : Matrix m n R) : A.rank ≤ Fintype.card m

theorem Matrix.rank_le_height {R : Type u_5} [CommRing R] [StrongRankCondition R] {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) : A.rank ≤ m

theorem Matrix.rank_eq_finrank_span_cols {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [CommRing R] (A : Matrix m n R) : A.rank = Module.finrank R ↥(Submodule.span R (Set.range A.transpose))

The rank of a matrix is the rank of the space spanned by its columns.

theorem Matrix.rank_diagonal {m : Type u_2} {R : Type u_5} [Field R] [Fintype m] [DecidableEq m] [DecidableEq R] (w : m → R) : (Matrix.diagonal w).rank = Fintype.card { i : m // w i ≠ 0 }

The rank of a diagnonal matrix is the count of non-zero elements on its main diagonal

Lemmas about transpose and conjugate transpose

This section contains lemmas about the rank of Matrix.transpose and Matrix.conjTranspose.

Unfortunately the proofs are essentially duplicated between the two; ℚ is a linearly-ordered ring but can't be a star-ordered ring, while ℂ is star-ordered (with open ComplexOrder) but not linearly ordered. For now we don't prove the transpose case for ℂ.

TODO: the lemmas Matrix.rank_transpose and Matrix.rank_conjTranspose current follow a short proof that is a simple consequence of Matrix.rank_transpose_mul_self and Matrix.rank_conjTranspose_mul_self. This proof pulls in unnecessary assumptions on R, and should be replaced with a proof that uses Gaussian reduction or argues via linear combinations.

theorem Matrix.ker_mulVecLin_conjTranspose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Fintype m] [Field R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) : LinearMap.ker (A.conjTranspose * A).mulVecLin = LinearMap.ker A.mulVecLin

theorem Matrix.rank_conjTranspose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Fintype m] [Field R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) : (A.conjTranspose * A).rank = A.rank

@[simp]

theorem Matrix.rank_conjTranspose {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Fintype m] [Field R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) : A.conjTranspose.rank = A.rank

TODO: prove this in greater generality.

@[simp]

theorem Matrix.rank_self_mul_conjTranspose {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Fintype m] [Field R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) : (A * A.conjTranspose).rank = A.rank

theorem Matrix.ker_mulVecLin_transpose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Fintype m] [LinearOrderedField R] (A : Matrix m n R) : LinearMap.ker (A.transpose * A).mulVecLin = LinearMap.ker A.mulVecLin

theorem Matrix.rank_transpose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Fintype m] [LinearOrderedField R] (A : Matrix m n R) : (A.transpose * A).rank = A.rank

@[simp]

theorem Matrix.rank_transpose {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Field R] [Fintype m] (A : Matrix m n R) : A.transpose.rank = A.rank

@[simp]

theorem Matrix.rank_self_mul_transpose {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [LinearOrderedField R] [Fintype m] (A : Matrix m n R) : (A * A.transpose).rank = A.rank

theorem Matrix.rank_eq_finrank_span_row {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Field R] [Finite m] (A : Matrix m n R) : A.rank = Module.finrank R ↥(Submodule.span R (Set.range A))

The rank of a matrix is the rank of the space spanned by its rows.

theorem LinearIndependent.rank_matrix {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Field R] [Fintype m] {M : Matrix m n R} (h : LinearIndependent R M) : M.rank = Fintype.card m

theorem Matrix.rank_add_rank_le_card_of_mul_eq_zero {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_5} [Fintype n] [Field R] [Finite l] [Fintype m] {A : Matrix l m R} {B : Matrix m n R} (hAB : A * B = 0) : A.rank + B.rank ≤ Fintype.card m