The even and odd parts of the Leibniz expansion

The Leibniz formula writes the determinant of a square matrix as a signed sum over permutations. Grouping its terms by the sign of the permutation gives two sums, P over the even and N over the odd permutations, with det M = P - N and permanent M = P + N. A permutation of the rows or of the columns of M either fixes both sums or exchanges them, according to its sign, so the symmetric functions P + N and P * N are invariant under such permutations while det M is only invariant up to sign. Together with (P - N) ^ 2 = (P + N) ^ 2 - 4 * (P * N) this is the engine of Stickelberger's congruence for discriminants of number fields.

Main definitions

• Matrix.leibnizPart: the sum of the Leibniz terms of the permutations of a given sign.

Main results

• Matrix.leibnizPart_one_sub_leibnizPart_neg_one, Matrix.leibnizPart_one_add_leibnizPart_neg_one: the two parts recover the determinant and the permanent.
• Matrix.leibnizPart_submatrix_left, Matrix.leibnizPart_submatrix_right: permuting the rows or the columns by ρ shifts the sign by Equiv.Perm.sign ρ.
• Matrix.leibnizPart_transpose, Matrix.leibnizPart_map: invariance under transposition and naturality under ring homomorphisms.
• Matrix.leibnizPart_one_mul_leibnizPart_neg_one_submatrix_left, Matrix.leibnizPart_one_mul_leibnizPart_neg_one_submatrix_right: the product of the two parts is invariant under permutations of the rows and of the columns.
• Matrix.det_sq_eq_permanent_sq_sub_four_mul: det M ^ 2 = permanent M ^ 2 - 4 * (P * N).

References

• L. Stickelberger, Über eine neue Eigenschaft der Diskriminanten algebraischer Zahlkörper (1897).
• W. Narkiewicz, Elementary and Analytic Theory of Algebraic Numbers, Chapter 4.

def Matrix.leibnizPart {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (s : ℤˣ) : R

The part of the Leibniz expansion of M indexed by the permutations of sign s: the sum of ∏ i, M (σ i) i over the permutations σ with Equiv.Perm.sign σ = s.

theorem Matrix.leibnizPart_def {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (s : ℤˣ) : M.leibnizPart s = ∑ σ : Equiv.Perm n with Equiv.Perm.sign σ = s, ∏ i : n, M (σ i) i

The defining sum of a Leibniz part.

theorem Matrix.leibnizPart_eq_sum_ite {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (s : ℤˣ) : M.leibnizPart s = ∑ σ : Equiv.Perm n, if Equiv.Perm.sign σ = s then ∏ i : n, M (σ i) i else 0

The Leibniz part as a sum over all permutations, the terms of the wrong sign being zero.

theorem Matrix.leibnizPart_one_add_leibnizPart_neg_one {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) : M.leibnizPart 1 + M.leibnizPart (-1) = M.permanent

The even part plus the odd part of the Leibniz expansion is the permanent.

@[simp]

theorem Matrix.leibnizPart_submatrix_left {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (ρ : Equiv.Perm n) (s : ℤˣ) : (M.submatrix (⇑ρ) id).leibnizPart s = M.leibnizPart (Equiv.Perm.sign ρ * s)

Permuting the rows by ρ multiplies the sign index of a Leibniz part by sign ρ.

@[simp]

theorem Matrix.leibnizPart_transpose {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (s : ℤˣ) : M.transpose.leibnizPart s = M.leibnizPart s

A Leibniz part is unchanged by transposition.

@[simp]

theorem Matrix.leibnizPart_submatrix_right {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (ρ : Equiv.Perm n) (s : ℤˣ) : (M.submatrix id ⇑ρ).leibnizPart s = M.leibnizPart (Equiv.Perm.sign ρ * s)

Permuting the columns by ρ multiplies the sign index of a Leibniz part by sign ρ.

theorem Matrix.leibnizPart_one_mul_leibnizPart_neg_one_submatrix_left {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (ρ : Equiv.Perm n) : (M.submatrix (⇑ρ) id).leibnizPart 1 * (M.submatrix (⇑ρ) id).leibnizPart (-1) = M.leibnizPart 1 * M.leibnizPart (-1)

The product of the even and the odd Leibniz parts is invariant under permutations of the rows.

theorem Matrix.leibnizPart_one_mul_leibnizPart_neg_one_submatrix_right {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommSemiring R] (M : Matrix n n R) (ρ : Equiv.Perm n) : (M.submatrix id ⇑ρ).leibnizPart 1 * (M.submatrix id ⇑ρ).leibnizPart (-1) = M.leibnizPart 1 * M.leibnizPart (-1)

The product of the even and the odd Leibniz parts is invariant under permutations of the columns.

@[simp]

theorem Matrix.leibnizPart_map {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} {S : Type u_3} [CommSemiring R] [CommSemiring S] {F : Type u_4} [FunLike F R S] [RingHomClass F R S] (f : F) (M : Matrix n n R) (s : ℤˣ) : (M.map ⇑f).leibnizPart s = f (M.leibnizPart s)

A ring homomorphism carries a Leibniz part of M to the Leibniz part of the mapped matrix.

theorem Matrix.leibnizPart_one_sub_leibnizPart_neg_one {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_4} [CommRing R] (M : Matrix n n R) : M.leibnizPart 1 - M.leibnizPart (-1) = M.det

The even part minus the odd part of the Leibniz expansion is the determinant.

theorem Matrix.det_sq_eq_permanent_sq_sub_four_mul {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_4} [CommRing R] (M : Matrix n n R) : M.det ^ 2 = M.permanent ^ 2 - 4 * (M.leibnizPart 1 * M.leibnizPart (-1))

The discriminant identity (P - N) ^ 2 = (P + N) ^ 2 - 4 * (P * N) for the two parts of the Leibniz expansion.