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
• Matrix.cRank: the rank of a matrix as a cardinal
• Matrix.eRank: the rank of a matrix as a term in ℕ∞.

Main results

• Matrix.rank_eq_finrank_range_toLin: the rank equals the dimension of the range of the corresponding linear map, and is therefore independent of the choice of bases.
• Matrix.rank_eq_finrank_span_cols, Matrix.rank_eq_finrank_span_row: the rank equals the dimension of the space spanned by the columns (resp. rows).
• Matrix.rank_transpose: transposing a matrix does not change its rank.
• Matrix.rank_mul_le: the rank of A * B is at most the rank of A and at most the rank of B.
• Matrix.rank_mul_eq_left_of_isUnit_det, Matrix.rank_mul_eq_right_of_isUnit_det: multiplying by an invertible matrix does not change the rank.
• Matrix.exists_rank_normal_form: every square matrix over a field can be brought, by left and right multiplication by invertible matrices, into the block form fromBlocks 1 0 0 0, where the identity block has size equal to the rank of the matrix.

noncomputable def Matrix.cRank {m : Type um} {n : Type un} {R : Type uR} [Semiring R] (A : Matrix m n R) : Cardinal.{max uR um}

The rank of a matrix, defined as the dimension of its column space, as a cardinal.

Equations

• A.cRank = Module.rank R ↥(Submodule.span R (Set.range A.col))

@[simp]

theorem Matrix.cRank_subsingleton {m : Type um} {n : Type un} {R : Type uR} [Semiring R] [Subsingleton R] (A : Matrix m n R) : A.cRank = 1

theorem Matrix.cRank_toNat_eq_finrank {m : Type um} {n : Type un} {R : Type uR} [Semiring R] (A : Matrix m n R) : Cardinal.toNat A.cRank = Module.finrank R ↥(Submodule.span R (Set.range A.col))

theorem Matrix.lift_cRank_submatrix_le {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [Semiring R] (A : Matrix m n R) (r : m₀ → m) (c : n₀ → n) : Cardinal.lift.{um, max uR um₀} (A.submatrix r c).cRank ≤ Cardinal.lift.{um₀, max uR um} A.cRank

theorem Matrix.cRank_submatrix_le {n : Type un} {n₀ : Type un₀} {R : Type uR} [Semiring R] {m m₀ : Type um} (A : Matrix m n R) (r : m₀ → m) (c : n₀ → n) : (A.submatrix r c).cRank ≤ A.cRank

A special case of lift_cRank_submatrix_le for when m₀ and m are in the same universe.

theorem Matrix.cRank_le_card_height {m : Type um} {n : Type un} {R : Type uR} [Semiring R] [StrongRankCondition R] [Fintype m] (A : Matrix m n R) : A.cRank ≤ ↑(Fintype.card m)

theorem Matrix.cRank_le_card_width {m : Type um} {n : Type un} {R : Type uR} [Semiring R] [StrongRankCondition R] [Fintype n] (A : Matrix m n R) : A.cRank ≤ ↑(Fintype.card n)

noncomputable def Matrix.eRank {m : Type um} {n : Type un} {R : Type uR} [Semiring R] (A : Matrix m n R) : ℕ∞

The rank of a matrix, defined as the dimension of its column space, as a term in ℕ∞.

Equations

• A.eRank = Cardinal.toENat A.cRank

@[simp]

theorem Matrix.eRank_subsingleton {m : Type um} {n : Type un} {R : Type uR} [Semiring R] [Subsingleton R] (A : Matrix m n R) : A.eRank = 1

theorem Matrix.eRank_toNat_eq_finrank {m : Type um} {n : Type un} {R : Type uR} [Semiring R] (A : Matrix m n R) : A.eRank.toNat = Module.finrank R ↥(Submodule.span R (Set.range A.col))

theorem Matrix.eRank_submatrix_le {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [Semiring R] (A : Matrix m n R) (r : m₀ → m) (c : n₀ → n) : (A.submatrix r c).eRank ≤ A.eRank

theorem Matrix.eRank_le_card_width {m : Type um} {n : Type un} {R : Type uR} [Semiring R] [StrongRankCondition R] (A : Matrix m n R) : A.eRank ≤ ENat.card n

theorem Matrix.eRank_le_card_height {m : Type um} {n : Type un} {R : Type uR} [Semiring R] [StrongRankCondition R] (A : Matrix m n R) : A.eRank ≤ ENat.card m

noncomputable def Matrix.rank {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommSemiring R] (A : Matrix m n R) : ℕ

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

Equations

• A.rank = Module.finrank R ↥A.mulVecLin.range

@[simp]

theorem Matrix.rank_subsingleton {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommSemiring R] [Subsingleton R] (A : Matrix m n R) : A.rank = 1

@[simp]

theorem Matrix.cRank_one {m : Type um} {R : Type uR} [Semiring R] [Nontrivial R] [DecidableEq m] [StrongRankCondition R] : cRank 1 = Cardinal.lift.{uR, um} (Cardinal.mk m)

@[simp]

theorem Matrix.eRank_one {m : Type um} {R : Type uR} [Semiring R] [Nontrivial R] [DecidableEq m] [StrongRankCondition R] : eRank 1 = ENat.card m

@[simp]

theorem Matrix.rank_one {n : Type un} {R : Type uR} [Fintype n] [CommSemiring R] [DecidableEq n] [StrongRankCondition R] : rank 1 = Fintype.card n

@[simp]

theorem Matrix.rank_zero {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommSemiring R] [Nontrivial R] : rank 0 = 0

@[simp]

theorem Matrix.cRank_zero {R : Type uR} {m : Type u_1} {n : Type u_2} [Semiring R] [Nontrivial R] : cRank 0 = 0

@[simp]

theorem Matrix.eRank_zero {R : Type uR} {m : Type u_1} {n : Type u_2} [Semiring R] [Nontrivial R] : eRank 0 = 0

theorem Matrix.rank_le_card_width {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommSemiring R] [StrongRankCondition R] (A : Matrix m n R) : A.rank ≤ Fintype.card n

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

theorem Matrix.rank_mul_le_left {m : Type um} {n : Type un} {o : Type uo} {R : Type uR} [Fintype n] [Fintype o] [CommSemiring 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 um} {n : Type un} {o : Type uo} {R : Type uR} [Fintype n] [Fintype o] [CommSemiring 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 um} {n : Type un} {o : Type uo} {R : Type uR} [Fintype n] [Fintype o] [CommSemiring R] [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) : (A * B).rank ≤ min A.rank B.rank

theorem Matrix.rank_vecMulVec_le {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommSemiring R] [StrongRankCondition R] (w : m → R) (v : n → R) : (vecMulVec w v).rank ≤ 1

theorem Matrix.rank_unit {n : Type un} {R : Type uR} [Fintype n] [DecidableEq n] [CommSemiring R] [StrongRankCondition R] (A : (Matrix n n R)ˣ) : (↑A).rank = Fintype.card n

theorem Matrix.rank_of_isUnit {n : Type un} {R : Type uR} [Fintype n] [DecidableEq n] [CommSemiring R] [StrongRankCondition R] (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 um} {n : Type un} [Fintype n] {R : Type u_1} [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 um} {n : Type un} [Fintype n] {R : Type u_1} [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 um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [Fintype n] [CommSemiring R] [StrongRankCondition R] [Fintype n₀] (A : Matrix m n R) (r : m₀ → m) (c : n₀ → n) : (A.submatrix r c).rank ≤ A.rank

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

theorem Matrix.rank_reindex {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [Fintype n] [Fintype n₀] [CommSemiring R] (em : m ≃ m₀) (en : n ≃ n₀) (A : Matrix m n R) : ((reindex em en) A).rank = A.rank

@[simp]

theorem Matrix.rank_submatrix {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [Fintype n] [Fintype n₀] [CommSemiring R] (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) : (A.submatrix ⇑em ⇑en).rank = A.rank

@[simp]

theorem Matrix.lift_cRank_submatrix {m : Type um} {m₀ : Type um₀} {n₀ : Type un₀} {R : Type uR} {n : Type un} [Semiring R] (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) : Cardinal.lift.{um, max uR um₀} (A.submatrix ⇑em ⇑en).cRank = Cardinal.lift.{um₀, max uR um} A.cRank

@[simp]

theorem Matrix.cRank_submatrix {m : Type um} {n₀ : Type un₀} {R : Type uR} {m₀ : Type um} {n : Type un} [Semiring R] (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) : (A.submatrix ⇑em ⇑en).cRank = A.cRank

A special case of lift_cRank_submatrix for when the row types are in the same universe.

theorem Matrix.lift_cRank_reindex {m : Type um} {m₀ : Type um₀} {n₀ : Type un₀} {R : Type uR} {n : Type un} [Semiring R] (A : Matrix m n R) (em : m ≃ m₀) (en : n ≃ n₀) : Cardinal.lift.{um, max uR um₀} ((reindex em en) A).cRank = Cardinal.lift.{um₀, max uR um} A.cRank

theorem Matrix.cRank_reindex {m : Type um} {n₀ : Type un₀} {R : Type uR} {m₀ : Type um} {n : Type un} [Semiring R] (A : Matrix m n R) (em : m ≃ m₀) (en : n ≃ n₀) : ((reindex em en) A).cRank = A.cRank

A special case of lift_cRank_reindex for when the row types are in the same universe.

@[simp]

theorem Matrix.eRank_submatrix {m : Type um} {m₀ : Type um₀} {n₀ : Type un₀} {R : Type uR} {n : Type un} [Semiring R] (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) : (A.submatrix ⇑em ⇑en).eRank = A.eRank

theorem Matrix.eRank_reindex {m : Type um} {n₀ : Type un₀} {R : Type uR} {m₀ : Type um} {n : Type un} [Semiring R] (A : Matrix m n R) (em : m ≃ m₀) (en : n ≃ n₀) : ((reindex em en) A).eRank = A.eRank

theorem Matrix.rank_eq_finrank_range_toLin {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Finite m] [DecidableEq n] {M₁ : Type u_1} {M₂ : Type u_2} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (A : Matrix m n R) (v₁ : Module.Basis m R M₁) (v₂ : Module.Basis n R M₂) : A.rank = Module.finrank R ↥((toLin v₂ v₁) A).range

The rank of a matrix equals the dimension of the range of the corresponding linear map, and is therefore independent of the choice of bases.

theorem Matrix.rank_le_card_height {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Fintype m] [CommSemiring R] [StrongRankCondition R] (A : Matrix m n R) : A.rank ≤ Fintype.card m

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

theorem Matrix.rank_eq_finrank_span_cols {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommSemiring R] (A : Matrix m n R) : A.rank = Module.finrank R ↥(Submodule.span R (Set.range A.col))

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

@[simp]

theorem Matrix.cRank_toNat_eq_rank {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommSemiring R] (A : Matrix m n R) : Cardinal.toNat A.cRank = A.rank

@[simp]

theorem Matrix.eRank_toNat_eq_rank {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [CommSemiring R] (A : Matrix m n R) : A.eRank.toNat = A.rank

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

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

theorem Matrix.exists_rank_normal_form {m : Type um} {R : Type uR} [Field R] [Fintype m] [DecidableEq m] (M : Matrix m m R) : ∃ (V : Matrix m m R) (U : Matrix m m R) (e : m ≃ Fin M.rank ⊕ Fin (Fintype.card m - M.rank)), IsUnit V ∧ IsUnit U ∧ V * M * U = (fromBlocks 1 0 0 0).submatrix ⇑e ⇑e

Every square matrix over a field can be brought, by left and right multiplication by invertible matrices, into the block form fromBlocks 1 0 0 0, where the identity block has size equal to the rank of the matrix.

theorem Matrix.cRank_diagonal {m : Type um} {R : Type uR} [Field R] [DecidableEq m] (w : m → R) : (diagonal w).cRank = Cardinal.lift.{uR, um} (Cardinal.mk { i : m // w i ≠ 0 })

theorem Matrix.eRank_diagonal {m : Type um} {R : Type uR} [Field R] [DecidableEq m] (w : m → R) : (diagonal w).eRank = {i : m | w i ≠ 0}.encard

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 um} {n : Type un} {R : Type uR} [Fintype n] [Fintype m] [Field R] [PartialOrder R] [StarRing R] [StarOrderedRing R] (A : Matrix m n R) : (A.conjTranspose * A).mulVecLin.ker = A.mulVecLin.ker

theorem Matrix.rank_conjTranspose_mul_self {m : Type um} {n : Type un} {R : Type uR} [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 um} {n : Type un} {R : Type uR} [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 um} {n : Type un} {R : Type uR} [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 um} {n : Type un} {R : Type uR} [Fintype n] [Fintype m] [Field R] [LinearOrder R] [IsStrictOrderedRing R] (A : Matrix m n R) : (A.transpose * A).mulVecLin.ker = A.mulVecLin.ker

theorem Matrix.rank_transpose_mul_self {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Fintype m] [Field R] [LinearOrder R] [IsStrictOrderedRing R] (A : Matrix m n R) : (A.transpose * A).rank = A.rank

@[simp]

theorem Matrix.rank_transpose {m : Type um} {n : Type un} {R : Type uR} [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 um} {n : Type un} {R : Type uR} [Fintype n] [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Fintype m] (A : Matrix m n R) : (A * A.transpose).rank = A.rank

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

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

theorem LinearIndependent.rank_matrix {m : Type um} {n : Type un} {R : Type uR} [Fintype n] [Field R] [Fintype m] {M : Matrix m n R} (h : LinearIndependent R M.row) : M.rank = Fintype.card m

theorem Matrix.rank_add_rank_le_card_of_mul_eq_zero {l : Type ul} {m : Type um} {n : Type un} {R : Type uR} [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

theorem Matrix.rank_vecMulVec {K m n : Type u} [CommRing K] [Fintype n] [DecidableEq n] (w : m → K) (v : n → K) : (toLin' (vecMulVec w v)).rank ≤ 1