Chiò's condensation

Let A be a square matrix of size n + 1 over a commutative ring, with corner entry a = A 0 0. Its condensation at that corner is the n × n matrix of 2 × 2 minors

A' i j = a · A (i + 1) (j + 1) - A (i + 1) 0 · A 0 (j + 1),

and Chiò's identity says a · det A' = aⁿ · det A. Over a field with a ≠ 0 it is the Schur complement formula det A = a · det (D - C a⁻¹ B) with the denominators cleared, and it holds over every commutative ring, with no invertibility hypothesis. This is what makes it usable for integral matrices: the condensation of an integral Gram matrix is again integral, and it is a times the Gram matrix of the projection orthogonal to the first basis vector. That is the inductive step of Hermite's inequality for the minimum of a positive definite quadratic form over ℤ.

Main results

• Matrix.mul_det_condensation_eq_pow_mul_det: A 0 0 · det A' = (A 0 0)ⁿ · det A.

References

• F. Chiò, Mémoire sur les fonctions connues sous le nom de résultantes ou de déterminants, Turin, 1853.

theorem Matrix.mul_det_condensation_eq_pow_mul_det {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin (n + 1)) (Fin (n + 1)) R) : A 0 0 * (of fun (i j : Fin n) => A 0 0 * A i.succ j.succ - A i.succ 0 * A 0 j.succ).det = A 0 0 ^ n * A.det

Chiò's condensation. For a square matrix A of size n + 1, the matrix A' of 2 × 2 minors A 0 0 * A (i + 1) (j + 1) - A (i + 1) 0 * A 0 (j + 1) satisfies A 0 0 · det A' = (A 0 0)ⁿ · det A. No invertibility of A 0 0 is needed.