Minors and determinants of matrices

Nonzero minors of matrices with arbitrarily many rows: the row index type may be infinite, as for coefficient matrices indexed by all monomials; only the column index type is finite.

Main results

• Matrix.exists_fin_linearIndependent_row_span_eq: finitely many linearly independent rows span the row space.
• Matrix.exists_rank_linearIndependent_rows: there are A.rank linearly independent rows.
• Matrix.exists_det_submatrix_ne_zero_of_le_rank: every r ≤ A.rank is witnessed by a nonzero r × r minor with distinct rows and columns.
• Matrix.le_rank_of_det_submatrix_ne_zero: conversely, a nonzero k × k minor shows k ≤ A.rank.
• Matrix.HasNonzeroMinor: the predicate that some r × r minor is nonzero; its rows and columns are automatically distinct (Matrix.injective_rows_of_det_submatrix_ne_zero, Matrix.injective_cols_of_det_submatrix_ne_zero).
• Matrix.det_blockDiagonal': the determinant of blockDiagonal' M is the product of the determinants of the blocks. Mathlib computes Matrix.det_blockDiagonal for blocks of a common size; here the blocks may have different sizes.
• Matrix.dvd_det_sub_det_of_dvd_sub: entrywise congruence of integer matrices implies congruence of their determinants.

theorem Matrix.exists_fin_linearIndependent_row_span_eq {F : Type u_1} {ι : Type u_2} {ν : Type u_3} [Field F] [Finite ν] (A : Matrix ι ν F) : ∃ (s : ℕ) (a : Fin s → ι), Function.Injective a ∧ LinearIndependent F (A.submatrix a id).row ∧ Submodule.span F (Set.range (A.submatrix a id).row) = Submodule.span F (Set.range A.row)

A finite independent family spans the rows even when their original index set is infinite.

theorem Matrix.ker_mulVecLin_submatrix_eq_of_span_row_eq {F : Type u_1} {ι : Type u_2} {κ : Type u_3} {ν : Type u_4} [Field F] [Fintype ν] (A : Matrix ι ν F) (a : κ → ι) (hs : Submodule.span F (Set.range (A.submatrix a id).row) = Submodule.span F (Set.range A.row)) : (A.submatrix a id).mulVecLin.ker = A.mulVecLin.ker

Restriction to spanning rows preserves the exact kernel.

theorem Matrix.exists_rank_linearIndependent_rows {F : Type u_1} {ι : Type u_2} {ν : Type u_3} [Field F] [Fintype ν] (A : Matrix ι ν F) : ∃ (a : Fin A.rank → ι), Function.Injective a ∧ LinearIndependent F (A.submatrix a id).row

There are exactly rank-many independent rows.

theorem Matrix.exists_det_submatrix_ne_zero_of_linearIndependent_row {F : Type u_1} {ν : Type u_2} [Field F] [Finite ν] {s : ℕ} (A : Matrix (Fin s) ν F) (hi : LinearIndependent F A.row) : ∃ (c : Fin s → ν), Function.Injective c ∧ (A.submatrix id c).det ≠ 0

Full row rank supplies a nonzero square minor: some set of columns of the transpose is linearly independent.

theorem Matrix.exists_det_submatrix_ne_zero_of_le_rank {F : Type u_1} {ι : Type u_2} {ν : Type u_3} [Field F] [Fintype ν] (A : Matrix ι ν F) (r : ℕ) (hr : r ≤ A.rank) : ∃ (a : Fin r → ι) (c : Fin r → ν), Function.Injective a ∧ Function.Injective c ∧ (A.submatrix a c).det ≠ 0

Every rank lower bound is witnessed by a nonzero minor with distinct rows and distinct columns, without any finiteness requirement on the rows.

theorem Matrix.le_rank_of_det_submatrix_ne_zero {R : Type u_1} {ι : Type u_2} {ν : Type u_3} [CommRing R] [IsDomain R] [Fintype ν] {k : ℕ} (A : Matrix ι ν R) (r : Fin k → ι) (c : Fin k → ν) (h : (A.submatrix r c).det ≠ 0) : k ≤ A.rank

A nonzero k × k minor shows that a matrix over a domain has rank at least k.

theorem Matrix.injective_rows_of_det_submatrix_ne_zero {R : Type u_1} {ι : Type u_2} {ν : Type u_3} [CommRing R] {k : ℕ} {A : Matrix ι ν R} {r : Fin k → ι} {c : Fin k → ν} (h : (A.submatrix r c).det ≠ 0) : Function.Injective r

The rows selected by a nonzero minor are distinct: a repeated row forces the determinant to vanish.

theorem Matrix.injective_cols_of_det_submatrix_ne_zero {R : Type u_1} {ι : Type u_2} {ν : Type u_3} [CommRing R] {k : ℕ} {A : Matrix ι ν R} {r : Fin k → ι} {c : Fin k → ν} (h : (A.submatrix r c).det ≠ 0) : Function.Injective c

The columns selected by a nonzero minor are distinct: a repeated column forces the determinant to vanish.

def Matrix.HasNonzeroMinor {R : Type u_1} {ι : Type u_2} {ν : Type u_3} [CommRing R] (A : Matrix ι ν R) (r : ℕ) : Prop

A has a nonzero r × r minor: some choice of r rows and r columns of A whose square submatrix has nonzero determinant. The chosen rows and columns are automatically distinct (Matrix.injective_rows_of_det_submatrix_ne_zero, Matrix.injective_cols_of_det_submatrix_ne_zero).

Equations

• A.HasNonzeroMinor r = ∃ (a : Fin r → ι) (c : Fin r → ν), (A.submatrix a c).det ≠ 0

theorem Matrix.hasNonzeroMinor_of_le_rank {F : Type u_1} {ι : Type u_2} {ν : Type u_3} [Field F] [Fintype ν] (A : Matrix ι ν F) {r : ℕ} (hr : r ≤ A.rank) : A.HasNonzeroMinor r

Every rank lower bound over a field is witnessed by a nonzero minor.

theorem Matrix.HasNonzeroMinor.le_rank {R : Type u_1} {ι : Type u_2} {ν : Type u_3} [CommRing R] [IsDomain R] [Fintype ν] {A : Matrix ι ν R} {r : ℕ} (h : A.HasNonzeroMinor r) : r ≤ A.rank

A nonzero r × r minor of a matrix over a domain shows r ≤ A.rank.

theorem Matrix.det_blockDiagonal' {o : Type u_1} {R : Type u_2} {m' : o → Type u_3} [Fintype o] [DecidableEq o] [(i : o) → Fintype (m' i)] [(i : o) → DecidableEq (m' i)] [CommRing R] (M : (i : o) → Matrix (m' i) (m' i) R) : (blockDiagonal' M).det = ∏ i : o, (M i).det

The determinant of a block-diagonal matrix with blocks of varying sizes is the product of the determinants of its blocks.

theorem Matrix.dvd_det_sub_det_of_dvd_sub {s : ℕ} (A B : Matrix (Fin s) (Fin s) ℤ) (m : ℤ) (h : ∀ (i j : Fin s), m ∣ A i j - B i j) : m ∣ A.det - B.det

Entrywise congruence implies determinant congruence, for every modulus.