Matrices equal to the negative of their transpose

A matrix satisfying Mᵀ = -M is determined by its entries above the diagonal, once its diagonal is known to vanish: the entries below are the negatives of their mirror images. The diagonal does vanish as soon as the value ring has no element that is its own negative apart from zero, which covers every ring of odd characteristic.

Main results

• Matrix.transpose_single_sub_single: transposing the difference of two opposite singleton matrices with the same coefficient negates it.
• Matrix.transpose_map_of_transpose_eq_neg: the condition passes to the image of the matrix under an additive morphism of the entry types.
• Matrix.diag_eq_zero_of_transpose_eq_neg: the diagonal vanishes when doubling is injective at zero, with Matrix.diag_eq_zero_of_transpose_eq_neg_of_charP reading that off an odd characteristic.
• Matrix.ext_of_lt_of_transpose_eq_neg: two such matrices with vanishing diagonals agree as soon as they agree above the diagonal.

theorem Matrix.transpose_single_sub_single {K : Type u_4} {ι : Type u_5} [AddGroup K] [DecidableEq ι] (i j : ι) (a : K) : (single i j a - single j i a).transpose = -(single i j a - single j i a)

Transposing the difference of two opposite singleton matrices with the same coefficient negates it.

theorem Matrix.transpose_map_of_transpose_eq_neg {n : Type u_1} {S : Type u_2} {T : Type u_3} [AddGroup S] [SubtractionMonoid T] {F : Type u_4} [FunLike F S T] [AddMonoidHomClass F S T] (f : F) {M : Matrix n n S} (hM : M.transpose = -M) : (M.map ⇑f).transpose = -M.map ⇑f

The condition Mᵀ = -M passes to the image of the matrix under an additive morphism of the entry types.

theorem Matrix.diag_eq_zero_of_transpose_eq_neg {n : Type u_1} {S : Type u_2} [AddGroup S] {M : Matrix n n S} (hM : M.transpose = -M) (h2 : ∀ (x : S), x + x = 0 → x = 0) (a : n) : M a a = 0

The diagonal of a matrix equal to the negative of its transpose vanishes, as soon as zero is the only entry that doubles to zero.

theorem Matrix.diag_eq_zero_of_transpose_eq_neg_of_charP {n : Type u_1} {S : Type u_2} [Ring S] (p : ℕ) [CharP S p] (hp : Odd p) {M : Matrix n n S} (hM : M.transpose = -M) (a : n) : M a a = 0

In a ring of odd characteristic the diagonal of a matrix equal to the negative of its transpose vanishes: odd characteristic implies that doubling is injective at zero, which is what the diagonal entries need.

theorem Matrix.ext_of_lt_of_transpose_eq_neg {n : Type u_1} {S : Type u_2} [LinearOrder n] [Zero S] [Neg S] {M N : Matrix n n S} (hM : M.transpose = -M) (hN : N.transpose = -N) (hMd : ∀ (a : n), M a a = 0) (hNd : ∀ (a : n), N a a = 0) (h : ∀ (a b : n), a < b → M a b = N a b) : M = N

Two matrices equal to the negatives of their transposes agree as soon as they agree above the diagonal, provided both diagonals vanish: the entries below the diagonal are the negatives of their mirror images.