Deleting a column of a matrix whose rows sum to zero

Let M be a matrix with rows indexed by ι and columns indexed by κ, where κ has one element more than ι, and suppose every row of M sums to zero. Deleting any column j of M and ordering the remaining columns by an equivalence ι ≃ {j' // j' ≠ j} gives a square matrix. Its determinant is the same for every choice of j and of the equivalence, up to sign.

This is the linear algebra behind the independence of a regulator from the place left out of the logarithmic embedding: the product formula says exactly that the rows of the full matrix of weighted logarithms sum to zero. Mathlib's Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det' is the case κ = Fin (n + 1), ι = Fin n, with the columns ordered by Fin.succAbove; here the index types are arbitrary.

Main results

• Matrix.exists_det_submatrix_eq_units_smul_of_injective: choosing the columns along any injective map avoiding a column j, instead of along an equivalence ι ≃ {j' // j' ≠ j}, changes the determinant only by a sign. This holds for any matrix.
• Matrix.exists_det_submatrix_eq_units_smul_of_sum_eq_zero: the two determinants agree up to a sign s : ℤˣ.
• Matrix.abs_det_submatrix_eq_of_sum_eq_zero: over a commutative ring with a linear order, such as ℝ, they have the same absolute value.

theorem Matrix.exists_det_submatrix_eq_units_smul_of_injective {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing R] (M : Matrix ι κ R) {j : κ} (e : ι ≃ { j' : κ // j' ≠ j }) {g : ι → κ} (hg : Function.Injective g) (hgj : ∀ (k : ι), g k ≠ j) : ∃ (s : ℤˣ), (M.submatrix id g).det = s • (M.submatrix id fun (k : ι) => ↑(e k)).det

Choosing the columns of M along an injective map g : ι → κ that avoids j gives the same determinant, up to sign, as choosing them along an equivalence ι ≃ {j' // j' ≠ j}.

theorem Matrix.exists_det_submatrix_eq_units_smul_of_sum_eq_zero {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [CommRing R] (M : Matrix ι κ R) (hM : ∀ (i : ι), ∑ j : κ, M i j = 0) {j₁ j₂ : κ} (e₁ : ι ≃ { j : κ // j ≠ j₁ }) (e₂ : ι ≃ { j : κ // j ≠ j₂ }) : ∃ (s : ℤˣ), (M.submatrix id fun (k : ι) => ↑(e₁ k)).det = s • (M.submatrix id fun (k : ι) => ↑(e₂ k)).det

Deleting a column of a matrix whose rows sum to zero. If every row of M sums to zero, then deleting the column j₁ or the column j₂, and ordering the remaining columns by any equivalences e₁ and e₂, gives square matrices whose determinants agree up to a sign.

theorem Matrix.abs_det_submatrix_eq_of_sum_eq_zero {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {R : Type u_4} [CommRing R] [LinearOrder R] (M : Matrix ι κ R) (hM : ∀ (i : ι), ∑ j : κ, M i j = 0) {j₁ j₂ : κ} (e₁ : ι ≃ { j : κ // j ≠ j₁ }) (e₂ : ι ≃ { j : κ // j ≠ j₂ }) : |(M.submatrix id fun (k : ι) => ↑(e₁ k)).det| = |(M.submatrix id fun (k : ι) => ↑(e₂ k)).det|

Deleting a column of a matrix whose rows sum to zero, over a commutative ring with a linear order such as ℝ: the square matrices obtained by deleting any column and ordering the remaining columns arbitrarily all have determinants of the same absolute value.