mathlib3 documentation

data.matrix.rank

Rank of matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_to_lin.

Main declarations #

TODO #

source
noncomputable def matrix.rank {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [comm_ring R] (A : matrix m n R) :
ℕ

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

Equations
source
@[simp]
theorem matrix.rank_one {n : Type u_3} {R : Type u_5} [fintype n] [comm_ring R] [strong_rank_condition R] [decidable_eq n] :
1.rank = fintype.card n
source
@[simp]
theorem matrix.rank_zero {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [comm_ring R] [nontrivial R] :
0.rank = 0
source
theorem matrix.rank_le_card_width {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [comm_ring R] [strong_rank_condition R] (A : matrix m n R) :
A.rank ≤ fintype.card n
source
theorem matrix.rank_le_width {R : Type u_5} [comm_ring R] [strong_rank_condition R] {m n : ℕ} (A : matrix (fin m) (fin n) R) :
A.rank ≤ n
source
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] [comm_ring R] [strong_rank_condition R] (A : matrix m n R) (B : matrix n o R) :
(A.mul B).rank ≤ A.rank
source
theorem matrix.rank_mul_le_right {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_5} [m_fin : fintype m] [fintype n] [comm_ring R] [strong_rank_condition R] (A : matrix l m R) (B : matrix m n R) :
(A.mul B).rank ≤ B.rank
source
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] [comm_ring R] [strong_rank_condition R] (A : matrix m n R) (B : matrix n o R) :
(A.mul B).rank ≤ linear_order.min A.rank B.rank
source
theorem matrix.rank_unit {n : Type u_3} {R : Type u_5} [fintype n] [comm_ring R] [strong_rank_condition R] [decidable_eq n] (A : (matrix n n R)ˣ) :
↑A.rank = fintype.card n
source
theorem matrix.rank_of_is_unit {n : Type u_3} {R : Type u_5} [fintype n] [comm_ring R] [strong_rank_condition R] [decidable_eq n] (A : matrix n n R) (h : is_unit A) :
A.rank = fintype.card n
source
theorem matrix.rank_submatrix_le {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [comm_ring R] [strong_rank_condition 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.

source
theorem matrix.rank_reindex {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [comm_ring R] [fintype m] (e₁ e₂ : m ≃ n) (A : matrix m m R) :
(⇑(matrix.reindex e₁ e₂) A).rank = A.rank
source
@[simp]
theorem matrix.rank_submatrix {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [comm_ring R] [fintype m] (A : matrix m m R) (e₁ e₂ : n ≃ m) :
(A.submatrix ⇑e₁ ⇑e₂).rank = A.rank
source
theorem matrix.rank_eq_finrank_range_to_lin {m : Type u_2} {n : Type u_3} {R : Type u_5} [m_fin : fintype m] [fintype n] [comm_ring R] [decidable_eq n] {M₁ : Type u_1} {M₂ : Type u_4} [add_comm_group M₁] [add_comm_group M₂] [module R M₁] [module R M₂] (A : matrix m n R) (v₁ : basis m R M₁) (v₂ : basis n R M₂) :
A.rank = finite_dimensional.finrank R ↥(linear_map.range (⇑(matrix.to_lin v₂ v₁) A))
source
theorem matrix.rank_le_card_height {m : Type u_2} {n : Type u_3} {R : Type u_5} [m_fin : fintype m] [fintype n] [comm_ring R] [strong_rank_condition R] (A : matrix m n R) :
A.rank ≤ fintype.card m
source
theorem matrix.rank_le_height {R : Type u_5} [comm_ring R] [strong_rank_condition R] {m n : ℕ} (A : matrix (fin m) (fin n) R) :
A.rank ≤ m
source
theorem matrix.rank_eq_finrank_span_cols {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [comm_ring R] (A : matrix m n R) :
A.rank = finite_dimensional.finrank R ↥(submodule.span R (set.range A.transpose))

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

Lemmas about transpose and conjugate transpose #

This section contains lemmas about the rank of matrix.transpose and matrix.conj_transpose.

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_locale complex_order) but not linearly ordered. For now we don't prove the transpose case for ℂ.

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

source
theorem matrix.ker_mul_vec_lin_conj_transpose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [fintype m] [field R] [partial_order R] [star_ordered_ring R] (A : matrix m n R) :
linear_map.ker (A.conj_transpose.mul A).mul_vec_lin = linear_map.ker A.mul_vec_lin
source
theorem matrix.rank_conj_transpose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [fintype m] [field R] [partial_order R] [star_ordered_ring R] (A : matrix m n R) :
(A.conj_transpose.mul A).rank = A.rank
source
@[simp]
theorem matrix.rank_conj_transpose {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [fintype m] [field R] [partial_order R] [star_ordered_ring R] (A : matrix m n R) :
A.conj_transpose.rank = A.rank

TODO: prove this in greater generality.

source
@[simp]
theorem matrix.rank_self_mul_conj_transpose {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [fintype m] [field R] [partial_order R] [star_ordered_ring R] (A : matrix m n R) :
(A.mul A.conj_transpose).rank = A.rank
source
theorem matrix.ker_mul_vec_lin_transpose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [fintype m] [linear_ordered_field R] (A : matrix m n R) :
linear_map.ker (A.transpose.mul A).mul_vec_lin = linear_map.ker A.mul_vec_lin
source
theorem matrix.rank_transpose_mul_self {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [fintype m] [linear_ordered_field R] (A : matrix m n R) :
(A.transpose.mul A).rank = A.rank
source
@[simp]
theorem matrix.rank_transpose {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [fintype m] [linear_ordered_field R] (A : matrix m n R) :
A.transpose.rank = A.rank

TODO: prove this in greater generality.

source
@[simp]
theorem matrix.rank_self_mul_transpose {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [fintype m] [linear_ordered_field R] (A : matrix m n R) :
(A.mul A.transpose).rank = A.rank
source
theorem matrix.rank_eq_finrank_span_row {m : Type u_2} {n : Type u_3} {R : Type u_5} [fintype n] [linear_ordered_field R] [finite m] (A : matrix m n R) :
A.rank = finite_dimensional.finrank R ↥(submodule.span R (set.range A))

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

TODO: prove this in a generality that works for ℂ too, not just ℚ and ℝ.