Matrices skew-adjoint for a bilinear form

For a square matrix J, Mathlib's Matrix.IsSkewAdjoint J A is the condition Aᵀ * J = J * -A: the matrix A is skew-adjoint for the bilinear form B(u, v) = u ⬝ᵥ J v. This file records basic facts about such matrices, independent of any Lie theory.

When J is invertible, skew-adjointness makes Aᵀ conjugate to -A, so A has trace zero as soon as 2 is invertible. When J is symmetric, every pair of vectors u, v gives a skew-adjoint matrix, the matrix vecMulVec v (u ᵥ* J) - vecMulVec u (v ᵥ* J) sending x to B(u, x) v - B(v, x) u.

The file also records the matrices preserving J by congruence, M * J * Mᵀ = J: a square-zero matrix Y with Y * J + J * Yᵀ = 0, that is, with Yᵀ skew-adjoint for J, gives the form-preserving unipotents 1 + t • Y; a diagonal matrix preserves J as soon as it does so entrywise; when J * J = -1, the row and column conventions agree for matrices with a left inverse; and a scalar matrix c • 1 can only preserve an invertible J when c ^ 2 = 1.

Main results

• Matrix.isUnit_of_mul_self_eq_neg_one: a form matrix whose square is minus the identity is a unit over any ring.
• Matrix.IsSkewAdjoint.trace_eq_zero: a matrix skew-adjoint for an invertible matrix has trace zero when 2 is invertible.
• Matrix.isSkewAdjoint_vecMulVec_sub_vecMulVec: for symmetric J, the matrix vecMulVec v (u ᵥ* J) - vecMulVec u (v ᵥ* J) is skew-adjoint for J.
• Matrix.vecMulVec_sub_vecMulVec_mulVec: that matrix sends x to (u ⬝ᵥ J *ᵥ x) • v - (v ⬝ᵥ J *ᵥ x) • u.
• Matrix.one_add_smul_mul_mul_transpose: a square-zero matrix Y with Y * J + J * Yᵀ = 0 gives form-preserving unipotents.
• Matrix.diagonal_mul_mul_transpose_diagonal: a diagonal matrix preserving J entrywise preserves it over any semiring.
• Matrix.transpose_mul_mul_eq_of_mul_mul_transpose_eq: for J * J = -1, a matrix with a left inverse preserving J in the row convention preserves it in the column convention over any ring.
• Matrix.sq_eq_one_of_smul_one_mul_mul_transpose_eq: for invertible J over a nonempty index type and a commutative semiring, a scalar matrix preserving J has scalar of square one.

theorem Matrix.isUnit_of_mul_self_eq_neg_one {n : Type u_1} {R : Type u_2} [Fintype n] [Ring R] [DecidableEq n] {J : Matrix n n R} (hJ : J * J = -1) : IsUnit J

A matrix whose square is minus the identity is a unit, with inverse its negative.

theorem Matrix.IsSkewAdjoint.trace_eq_zero {n : Type u_1} {R : Type u_2} [Fintype n] [CommRing R] [DecidableEq n] [Invertible 2] {J A : Matrix n n R} (hJ : IsUnit J) (hA : J.IsSkewAdjoint A) : A.trace = 0

A matrix skew-adjoint for an invertible matrix has trace zero when 2 is invertible: skew-adjointness makes Aᵀ conjugate to -A.

theorem Matrix.isSkewAdjoint_vecMulVec_sub_vecMulVec {n : Type u_1} {R : Type u_2} [Fintype n] [CommRing R] {J : Matrix n n R} (hJ : J.IsSymm) (u v : n → R) : J.IsSkewAdjoint (vecMulVec v (vecMul u J) - vecMulVec u (vecMul v J))

For a symmetric matrix J, the matrix sending x to (u ⬝ᵥ J x) • v - (v ⬝ᵥ J x) • u is skew-adjoint for J.

theorem Matrix.vecMulVec_sub_vecMulVec_mulVec {n : Type u_1} {R : Type u_2} [Fintype n] [CommRing R] (J : Matrix n n R) (u v x : n → R) : (vecMulVec v (vecMul u J) - vecMulVec u (vecMul v J)).mulVec x = (u ⬝ᵥ J.mulVec x) • v - (v ⬝ᵥ J.mulVec x) • u

The matrix vecMulVec v (u ᵥ* J) - vecMulVec u (v ᵥ* J) sends x to (u ⬝ᵥ J *ᵥ x) • v - (v ⬝ᵥ J *ᵥ x) • u.

Matrices preserving a form

theorem Matrix.one_add_smul_mul_mul_transpose {n : Type u_1} {R : Type u_2} [Fintype n] [CommRing R] [DecidableEq n] (J Y : Matrix n n R) (t : R) (hskew : Y * J + J * Y.transpose = 0) (hsq : Y * Y = 0) : (1 + t • Y) * J * (1 + t • Y).transpose = J

A square-zero matrix Y with Y * J + J * Yᵀ = 0 gives form-preserving unipotents: (1 + t • Y) * J * (1 + t • Y)ᵀ = J for every scalar t.

theorem Matrix.diagonal_mul_mul_transpose_diagonal {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] (d : n → R) (J : Matrix n n R) (hd : ∀ (i j : n), d i * J i j * d j = J i j) : diagonal d * J * (diagonal d).transpose = J

Over any semiring, a diagonal matrix preserves a form J as soon as it does so entrywise: d i * J i j * d j = J i j for all i and j.

theorem Matrix.transpose_mul_mul_eq_of_mul_mul_transpose_eq {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [Ring R] {J M N : Matrix n n R} (hJ : J * J = -1) (hNM : N * M = 1) (h : M * J * M.transpose = J) : M.transpose * J * M = J

For a form J with J * J = -1, the row and column conventions agree: a matrix M with a left inverse and M * J * Mᵀ = J satisfies Mᵀ * J * M = J, over any ring.

theorem Matrix.sq_eq_one_of_smul_one_mul_mul_transpose_eq {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommSemiring R] [Nonempty n] {J : Matrix n n R} (hJ : IsUnit J) {c : R} (h : c • 1 * J * (c • 1).transpose = J) : c ^ 2 = 1

A scalar matrix preserving an invertible form J has scalar of square one, over a nonempty index type and a commutative semiring.