The signature of a square matrix over a linearly ordered field

The signature of a square matrix A over a linearly ordered field is the difference between the two indices of inertia of the quadratic form x ↦ x ⬝ᵥ A *ᵥ x, that is Mathlib's sigPos A.toQuadraticForm' - sigNeg A.toQuadraticForm'. Only the symmetric part of A is visible to that form, so the signature of A agrees with the signature of A + Aᵀ.

The three properties that make the signature computable are proved here: it is invariant under congruence A ↦ P * A * Pᵀ by a matrix with unit determinant, it is additive along a block diagonal, and on a diagonal matrix it counts the positive entries against the negative ones. Together these evaluate the signature of any matrix diagonalised by an explicit congruence.

For an integral symmetric bilinear form presented as a lattice, TauCeti.IntegralLattice.signature records the finer triple (n₊, n₀, n₋); the definition here is the basis-level matrix counterpart, which is what a congruence class of matrices — such as the S-equivalence class of a Seifert matrix — offers.

Main definitions

• Matrix.signature: the difference of the two indices of inertia.

Main results

• Matrix.signature_congr: invariance under congruence by a matrix with unit determinant.
• Matrix.signature_submatrix_equiv_self: invariance under an equivalence of the coordinate type.
• Matrix.signature_fromBlocks_zero: additivity along a block diagonal.
• Matrix.signature_diagonal: the signature of a diagonal matrix as a sum of signs.
• Matrix.signature_hyperbolicGram: the hyperbolic plane has signature zero.
• Matrix.signature_eq_of_congr_diagonal: the signature read off an explicit diagonalising congruence.
• Matrix.signature_add_transpose: the signature of A + Aᵀ is the signature of A.
• Matrix.signature_smul_of_pos: positive scaling does not change the signature.

References

• W. Ebeling, Lattices and Codes, Chapter 1.

noncomputable def Matrix.signature {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} [Fintype ι] (A : Matrix ι ι 𝕜) : ℤ

The signature of a square matrix over a linearly ordered field: the positive index of inertia of the quadratic form x ↦ x ⬝ᵥ A *ᵥ x minus its negative index.

Only the symmetric part of A contributes, by Matrix.signature_add_transpose.

The quadratic form of a matrix does not depend on the decidability of equality on the index type, so the local decider here is invisible: Matrix.signature_def identifies the definition with the one read off any DecidableEq ι instance. Keeping it local leaves DecidableEq out of the statements that do not mention Matrix.toQuadraticForm', Matrix.diagonal or Matrix.det themselves.

Equations

• A.signature = ↑(sigPos A.toQuadraticForm') - ↑(sigNeg A.toQuadraticForm')

theorem Matrix.signature_def {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι 𝕜) : A.signature = ↑(sigPos A.toQuadraticForm') - ↑(sigNeg A.toQuadraticForm')

theorem Matrix.signature_eq_of_equivalent {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] {A : Matrix ι ι 𝕜} {B : Matrix κ κ 𝕜} (h : QuadraticMap.Equivalent A.toQuadraticForm' B.toQuadraticForm') : A.signature = B.signature

Isometric quadratic forms have the same signature, so the signature only depends on the isometry class of the form of a matrix.

theorem Matrix.signature_congr {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {P : Matrix ι ι 𝕜} (hP : IsUnit P.det) (A : Matrix ι ι 𝕜) : (P * A * P.transpose).signature = A.signature

Congruence invariance of the signature. Replacing A by P * A * Pᵀ for a matrix P with unit determinant does not change the signature.

@[simp]

theorem Matrix.signature_submatrix_equiv_self {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (A : Matrix ι ι 𝕜) : (A.submatrix ⇑e.symm ⇑e.symm).signature = A.signature

Reindexing both coordinates of a matrix along an equivalence does not change its signature.

@[simp]

theorem Matrix.signature_transpose {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} [Fintype ι] (A : Matrix ι ι 𝕜) : A.transpose.signature = A.signature

Transposing a matrix does not change its signature.

@[simp]

theorem Matrix.signature_neg {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} [Fintype ι] (A : Matrix ι ι 𝕜) : (-A).signature = -A.signature

Negating a matrix negates its signature.

@[simp]

theorem Matrix.signature_zero {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} [Fintype ι] : signature 0 = 0

The zero matrix has signature zero.

@[simp]

theorem Matrix.signature_of_isEmpty {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} [Fintype ι] [IsEmpty ι] (A : Matrix ι ι 𝕜) : A.signature = 0

A matrix indexed by an empty type has signature zero.

@[simp]

theorem Matrix.signature_add_transpose {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} [Fintype ι] [IsStrictOrderedRing 𝕜] (A : Matrix ι ι 𝕜) : (A + A.transpose).signature = A.signature

The signature of a matrix is the signature of its symmetrisation A + Aᵀ.

@[simp]

theorem Matrix.signature_smul_of_pos {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} [Fintype ι] [IsStrictOrderedRing 𝕜] {c : 𝕜} (hc : 0 < c) (A : Matrix ι ι 𝕜) : (c • A).signature = A.signature

Scaling a matrix by a positive scalar does not change its signature.

@[simp]

theorem Matrix.signature_fromBlocks_zero {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [IsStrictOrderedRing 𝕜] (A : Matrix ι ι 𝕜) (B : Matrix κ κ 𝕜) : (fromBlocks A 0 0 B).signature = A.signature + B.signature

Additivity of the signature along a block diagonal.

@[simp]

theorem Matrix.signature_diagonal {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} [Fintype ι] [IsStrictOrderedRing 𝕜] [DecidableEq ι] (d : ι → 𝕜) : (diagonal d).signature = ∑ i : ι, if 0 < d i then 1 else if d i < 0 then -1 else 0

The signature of a diagonal matrix counts its positive entries against its negative ones.

theorem Matrix.signature_eq_of_congr_diagonal {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] {ι : Type u_2} [Fintype ι] [IsStrictOrderedRing 𝕜] [DecidableEq ι] {P A : Matrix ι ι 𝕜} (hP : IsUnit P.det) {d : ι → 𝕜} (h : P * A * P.transpose = diagonal d) : A.signature = ∑ i : ι, if 0 < d i then 1 else if d i < 0 then -1 else 0

The signature from an explicit diagonalising congruence.

@[simp]

theorem Matrix.signature_hyperbolicGram {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] : !![0, 1; 1, 0].signature = 0

The Gram matrix of a hyperbolic plane has signature zero: it is congruent to diagonal ![2, -2].