The corner minor of a doubly singular matrix

The corner minor of a square matrix A indexed by Fin (n + 1) is the determinant of the submatrix obtained by deleting its last row and its last column, that is, the determinant of A.submatrix Fin.castSucc Fin.castSucc. Unlike the determinant it is not a conjugation invariant in general. It becomes one on a matrix that is annihilated on the right by a column vector u and on the left by a row vector w, as soon as the conjugating matrix fixes u and w as well and the last coordinates of u and w are units: this is Matrix.det_submatrix_castSucc_conj.

The mechanism is that u and w give A a factorisation through the corner minor's own index type Fin n: the identity with its last row replaced by w carries A into the image of the inclusion Fin n ↪ Fin (n + 1), and the identity with its last column replaced by u does the same on the other side. A conjugation A ↦ N * A * N⁻¹ by a matrix fixing u and w therefore multiplies the corner minor by N.det on one side and by N.det⁻¹ on the other.

The rectangular deletion and inclusion matrices and the row and column framing matrices are recorded first under [Zero R] [One R], followed by their interaction with matrix multiplication under [NonAssocSemiring R]. The sparse Laplace expansions along the last row and column, the description of the corner minor as an ordinary determinant after replacing the last column by the last standard basis vector, and the conjugation invariance formula are proved under [CommRing R].

The intended source of such a matrix is burau b - 1 for a braid b, where u is the all-ones vector and w is the geometric vector (1, t, …, t ^ n).

Main results

• Matrix.det_eq_mul_det_submatrix_castSucc_of_row and Matrix.det_eq_mul_det_submatrix_castSucc_of_col: the determinant of a matrix whose last row, or whose last column, vanishes off the diagonal is the corner entry times the corner minor.
• Matrix.det_eq_det_submatrix_castSucc_of_apply_last: the determinant of a matrix whose last row is that of the identity is its corner minor.
• Matrix.det_updateCol_last_single: replacing the last column by the last standard basis vector turns the determinant into the corner minor.
• Matrix.submatrix_mul_of_mulVec_single: deleting the last row and column commutes with a product when the left factor fixes the last standard basis vector.
• Matrix.det_updateCol_last_smul_col_sub_single_of_det_sub_one_eq_zero: a determinant formula for replacing the last column of M - 1 by a linear combination of the last columns of M and 1.
• Matrix.det_submatrix_castSucc_conj: the corner minor of N * A * N⁻¹ equals that of A, when A is annihilated by u on the right and by w on the left and N fixes both.

The two rectangular matrices that delete and restore the last coordinate

The two square matrices built from the annihilating vectors

theorem Matrix.submatrix_mul_of_mulVec_single {n : ℕ} {R : Type u_1} [NonAssocSemiring R] (X Y : Matrix (Fin (n + 1)) (Fin (n + 1)) R) (hX : X.mulVec (Pi.single (Fin.last n) 1) = Pi.single (Fin.last n) 1) : (X * Y).submatrix Fin.castSucc Fin.castSucc = X.submatrix Fin.castSucc Fin.castSucc * Y.submatrix Fin.castSucc Fin.castSucc

Deleting the last row and column of a product is the product of the deletions, provided the left factor has the last standard basis vector as its last column.

theorem Matrix.det_eq_mul_det_submatrix_castSucc_of_row {n : ℕ} {R : Type u_1} [CommRing R] (A : Matrix (Fin (n + 1)) (Fin (n + 1)) R) (h : ∀ (j : Fin (n + 1)), j ≠ Fin.last n → A (Fin.last n) j = 0) : A.det = A (Fin.last n) (Fin.last n) * (A.submatrix Fin.castSucc Fin.castSucc).det

Laplace expansion along the last row of a matrix whose last row vanishes off the diagonal.

theorem Matrix.det_eq_mul_det_submatrix_castSucc_of_col {n : ℕ} {R : Type u_1} [CommRing R] (A : Matrix (Fin (n + 1)) (Fin (n + 1)) R) (h : ∀ (i : Fin (n + 1)), i ≠ Fin.last n → A i (Fin.last n) = 0) : A.det = A (Fin.last n) (Fin.last n) * (A.submatrix Fin.castSucc Fin.castSucc).det

Laplace expansion along the last column of a matrix whose last column vanishes off the diagonal.

theorem Matrix.det_eq_det_submatrix_castSucc_of_apply_last {n : ℕ} {R : Type u_1} [CommRing R] {A : Matrix (Fin (n + 1)) (Fin (n + 1)) R} (h : A (Fin.last n) = 1 (Fin.last n)) : A.det = (A.submatrix Fin.castSucc Fin.castSucc).det

The determinant of a matrix whose last row is that of the identity is its corner minor.

theorem Matrix.det_updateCol_last_single {n : ℕ} {R : Type u_1} [CommRing R] (A : Matrix (Fin (n + 1)) (Fin (n + 1)) R) : (A.updateCol (Fin.last n) (Pi.single (Fin.last n) 1)).det = (A.submatrix Fin.castSucc Fin.castSucc).det

Replacing the last column of a matrix by the last standard basis vector turns its determinant into its corner minor.

theorem Matrix.det_updateCol_last_smul_col_sub_single_of_det_sub_one_eq_zero {n : ℕ} {R : Type u_1} [CommRing R] (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R) (hdet : (M - 1).det = 0) (c : R) : ((M - 1).updateCol (Fin.last n) fun (u : Fin (n + 1)) => c * M u (Fin.last n) - Pi.single (Fin.last n) 1 u).det = (c - 1) * ((M - 1).submatrix Fin.castSucc Fin.castSucc).det

The determinant of a matrix M - 1 whose last column has been replaced by c • M.col (last) - e (last), in terms of the corner minor of M - 1.

Conjugation invariance of the corner minor

theorem Matrix.det_submatrix_castSucc_conj {n : ℕ} {R : Type u_1} [CommRing R] (A N : Matrix (Fin (n + 1)) (Fin (n + 1)) R) {u w : Fin (n + 1) → R} (hAu : A.mulVec u = 0) (hwA : vecMul w A = 0) (hNu : N.mulVec u = u) (hwN : vecMul w N = w) (hN : IsUnit N.det) (hu : IsUnit (u (Fin.last n))) (hw : IsUnit (w (Fin.last n))) : ((N * A * N⁻¹).submatrix Fin.castSucc Fin.castSucc).det = (A.submatrix Fin.castSucc Fin.castSucc).det

The corner minor is a conjugation invariant on doubly singular matrices. If a square matrix A is annihilated on the right by a column vector u and on the left by a row vector w, both of which have a unit in their last coordinate, then conjugating A by any invertible matrix that fixes u and w leaves the determinant of A.submatrix Fin.castSucc Fin.castSucc unchanged.