Determinants of skew-symmetric matrices and of even symmetric matrices

The determinant of a skew-symmetric matrix M (Mᵀ = -M) with zero diagonal over a field is a square: the form x, y ↦ xᵀ M y is alternating, so when it is nondegenerate it has a symplectic basis, in which its matrix is J of determinant 1, and det M is the square of the determinant of the change of basis. For an integer matrix the diagonal vanishes automatically and the square root, a rational number, is an integer. Over an arbitrary commutative ring the statement is Cayley's identity det M = Pf(M)², which needs the Pfaffian and is not proved here.

A symmetric integer matrix A with even diagonal, of size 2k, splits as A = S + Sᵀ. The polynomial q(X) = det (X • Sᵀ + S) has degree at most 2k and is its own reflection at 2k, because reflecting the entries transposes the matrix; its coefficients are therefore palindromic. Comparing q(1) = det (S + Sᵀ) with q(-1) = det (S - Sᵀ) through the palindromic coefficients shows that (-1)^k det (S + Sᵀ) ≡ det (S - Sᵀ) modulo 4, over any commutative ring. Since S - Sᵀ is skew-symmetric its determinant is a square, so (-1)^k det A ≡ 0 or 1 modulo 4: the signed determinant of an even symmetric integer matrix of even size is a discriminant. For the Gram matrix !![2a, b; b, 2c] of a binary form this is b² - 4ac ≡ b² (mod 4).

Main results

• Matrix.isSquare_det_of_transpose_eq_neg_of_diag_eq_zero: a skew-symmetric matrix with zero diagonal over a field has square determinant.
• Matrix.isSquare_det_of_transpose_eq_neg: a skew-symmetric integer matrix has square determinant.
• Matrix.four_dvd_neg_one_pow_mul_det_add_transpose_sub_det_sub_transpose: in dimension 2k, (-1)^k det (S + Sᵀ) ≡ det (S - Sᵀ) modulo 4.
• Matrix.IsSymm.neg_one_pow_mul_det_modEq_zero_or_one: for a symmetric integer matrix A of size 2k with even diagonal, (-1)^k det A ≡ 0 or 1 modulo 4.

Skew-symmetric matrices

theorem Matrix.isSquare_det_of_transpose_eq_neg_of_diag_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {K : Type u_2} [Field K] {M : Matrix ι ι K} (hM : M.transpose = -M) (hd : ∀ (i : ι), M i i = 0) : IsSquare M.det

The determinant of a skew-symmetric matrix with zero diagonal over a field is a square.

theorem Matrix.isSquare_det_of_transpose_eq_neg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Matrix ι ι ℤ} (hM : M.transpose = -M) : IsSquare M.det

The determinant of a skew-symmetric integer matrix is a square.

The determinant of S + Sᵀ modulo 4

theorem Matrix.four_dvd_neg_one_pow_mul_det_add_transpose_sub_det_sub_transpose {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [CommRing R] {k : ℕ} (hk : Fintype.card ι = 2 * k) (S : Matrix ι ι R) : 4 ∣ (-1) ^ k * (S + S.transpose).det - (S - S.transpose).det

det (S + Sᵀ) modulo 4. For a square matrix S of size 2k over a commutative ring, (-1)^k det (S + Sᵀ) ≡ det (S - Sᵀ) modulo 4.

Even symmetric integer matrices

theorem Matrix.IsSymm.neg_one_pow_mul_det_modEq_zero_or_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι ℤ} (hA : A.IsSymm) (hd : ∀ (i : ι), Even (A i i)) {k : ℕ} (hk : Fintype.card ι = 2 * k) : (-1) ^ k * A.det ≡ 0 [ZMOD 4] ∨ (-1) ^ k * A.det ≡ 1 [ZMOD 4]

The signed determinant of an even symmetric integer matrix is a discriminant. If A is a symmetric integer matrix of size 2k with even diagonal entries, then (-1)^k det A is congruent to 0 or 1 modulo 4.