Determinants of a fixed family followed by a varying one

Let x be a family of vectors in R^ι indexed by m, and let y be a family indexed by n whose orthogonal vectors, those v with y k ⬝ᵥ v = 0 for every k, all lie in the span of x. Suppose w is a family indexed by n pairing with y to the standard basis, so y k ⬝ᵥ w j is 1 if j = k and 0 otherwise. Then, for a family z indexed by n, the determinant of the square matrix whose rows are x followed by z factors as the determinant of the pairings y k ⬝ᵥ z j times the same determinant at z = w.

The proof writes each z j as a combination of the x i plus ∑ k, (y k ⬝ᵥ z j) • w k, which expresses the matrix of x followed by z as a block lower triangular matrix times the matrix of x followed by w.

This is the linear algebra behind complementary minors: taking z to be standard basis vectors compares the Plücker coordinates of a subspace with those of its orthogonal complement.

Main results

• TauCeti.Matrix.det_sumElim_eq_det_mul: the determinant of x followed by z is det (y * zᵀ) times the determinant of x followed by w.

theorem TauCeti.Matrix.det_sumElim_eq_det_mul {R : Type u_1} {m : Type u_2} {n : Type u_3} {ι : Type u_4} [CommRing R] [Fintype m] [Fintype n] [Fintype ι] [DecidableEq m] [DecidableEq n] (e : m ⊕ n ≃ ι) {x : m → ι → R} {y w : n → ι → R} (hx : (Matrix.of y).mulVecLin.ker ≤ Submodule.span R (Set.range x)) (hw : ∀ (j : n), (Matrix.of y).mulVec (w j) = Pi.single j 1) (z : n → ι → R) : (Matrix.of fun (a b : m ⊕ n) => Sum.elim x z a (e b)).det = (Matrix.of y * (Matrix.of z).transpose).det * (Matrix.of fun (a b : m ⊕ n) => Sum.elim x w a (e b)).det

Let x span every vector orthogonal to all y k, and let w j pair with y to the standard basis vector at j. Then, as a function of z, the determinant of x followed by z (against an identification e of the index types) is the determinant of the pairings of y with z, times its value at w.