Linear independence and nonsingularity of matrices

In this file we formalize several theorems proved by Yi-Jia Tan in his paper [Tan16] Free sets and free subsemimodules in a semimodule. As consequences, we show that commutative semirings satisfy the strong rank condition, and that the columns of a square matrix are linearly independent if and only if the matrix is nonsingular (over a commutative ring, a matrix is nonsingular if and only if its determinant is not a zero divisor).

Main theorems

• Matrix.Nonsingular.of_linearIndependent_col: if the columns of a square matrix are linearly independent, then the matrix is nonsingular. Corollary 3.2(1) of [Tan16].

• Matrix.Nonsingular.linearIndependent_col: if a matrix over a commutative semiring with cancellative addition is nonsingular, then its columns are linearly independent. Corollary 3.2(2) of [Tan16].

• CommSemiring.strongRankCondition_of_nontrivial: a commutative semiring satisfies the strong rank condition.

theorem Matrix.isDetpBalanced_iff_sub_mul_det_eq_zero {n : Type u_3} [Fintype n] [DecidableEq n] {R : Type u_4} [CommRing R] {A : Matrix n n R} {a b : R} : A.IsDetpBalanced a b ↔ (a - b) * A.det = 0

theorem Matrix.nonsingular_iff_det_mem_nonZeroDivisors {n : Type u_3} [Fintype n] [DecidableEq n] {R : Type u_4} [CommRing R] {A : Matrix n n R} : A.Nonsingular ↔ A.det ∈ nonZeroDivisors R

theorem Matrix.nonsingular_iff_det_ne_zero {n : Type u_3} [Fintype n] [DecidableEq n] {R : Type u_4} [CommRing R] [IsDomain R] {A : Matrix n n R} : A.Nonsingular ↔ A.det ≠ 0

theorem Matrix.Nonsingular.of_linearIndependent_col {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} (ind : LinearIndependent R A.col) : A.Nonsingular

If the columns of a square matrix are linearly independent, then the matrix is nonsingular.

theorem Matrix.Nonsingular.of_linearIndependent_row {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} (ind : LinearIndependent R A.row) : A.Nonsingular

theorem Matrix.Nonsingular.of_leftRegular {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} (h : IsLeftRegular A) : A.Nonsingular

theorem Matrix.Nonsingular.of_rightRegular {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} (h : IsRightRegular A) : A.Nonsingular

theorem Matrix.Nonsingular.linearIndependent_col {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} [IsCancelAdd R] (hA : A.Nonsingular) : LinearIndependent R A.col

If a matrix over a commutative semiring with cancellative addition is nonsingular, then its columns are linearly independent. Generalizes Matrix.linearIndependent_cols_of_det_ne_zero.

theorem Matrix.Nonsingular.linearIndependent_row {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} [IsCancelAdd R] (hA : A.Nonsingular) : LinearIndependent R A.row

theorem Matrix.linearIndependent_col_iff {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} [IsCancelAdd R] : LinearIndependent R A.col ↔ A.Nonsingular

theorem Matrix.linearIndependent_row_iff {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} [IsCancelAdd R] : LinearIndependent R A.row ↔ A.Nonsingular

theorem Matrix.isLeftRegular_iff_nonsingular {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} [IsCancelAdd R] : IsLeftRegular A ↔ A.Nonsingular

theorem Matrix.isRightRegular_iff_nonsingular {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} [IsCancelAdd R] : IsRightRegular A ↔ A.Nonsingular

theorem Matrix.Nonsingular.mul {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} [IsCancelAdd R] {B : Matrix n n R} (hA : A.Nonsingular) (hB : B.Nonsingular) : (A * B).Nonsingular

theorem Matrix.nonsingular_mul_iff {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] [IsCancelAdd R] {A B : Matrix n n R} : (A * B).Nonsingular ↔ A.Nonsingular ∧ B.Nonsingular

theorem Matrix.Nonsingular.pow {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] {A : Matrix n n R} [IsCancelAdd R] (hA : A.Nonsingular) (k : ℕ) : (A ^ k).Nonsingular

theorem Matrix.isLeftRegular_iff_isRightRegular {R : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype n] {A : Matrix n n R} [IsCancelAdd R] : IsLeftRegular A ↔ IsRightRegular A

theorem Matrix.linearIndependent_col_iff_row {R : Type u_1} {n : Type u_3} [CommSemiring R] {A : Matrix n n R} [IsCancelAdd R] [Finite n] : LinearIndependent R A.col ↔ LinearIndependent R A.row

https://mathoverflow.net/questions/511862/transpose-symmetry-of-injectivity-of-linear-maps-over-semirings asks whether this is still true without IsCancelAdd R.

@[instance 100]

instance CommSemiring.strongRankCondition_of_nontrivial {R : Type u_1} [CommSemiring R] [Nontrivial R] : StrongRankCondition R

A nontrivial commutative semiring satisfies the strong rank condition.