Documentation

AlgebraicCombinatorics.Extra.Pfaffian

Skew-Symmetric Matrices #

This file defines skew-symmetric matrices and proves basic properties.

A matrix A is skew-symmetric (also called antisymmetric) if A^T = -A.

Main definitions #

Main results #

Notes #

This file provides basic infrastructure for skew-symmetric matrices. The Pfaffian of a skew-symmetric matrix and Kasteleyn's formula for counting domino tilings would require substantial additional infrastructure.

Note: Mathlib has Matrix.IsSkewAdjoint J A which is the more general notion of A being skew-adjoint with respect to a bilinear form J (i.e., Aᵀ * J = -J * A). Our IsSkewSymmetric is the special case where J = I, i.e., simply Aᵀ = -A.

References #

Skew-Symmetric Matrices #

source
def Matrix.IsSkewSymmetric {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] (A : Matrix n n R) :
Prop

A matrix A is skew-symmetric if A^T = -A.

Equations
Instances For
    source
    theorem Matrix.IsSkewSymmetric.diag_eq_zero {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] [NoZeroDivisors R] [CharZero R] {A : Matrix n n R} (hA : A.IsSkewSymmetric) (i : n) :
    A i i = 0

    Diagonal entries of a skew-symmetric matrix are zero (in characteristic ≠ 2).

    source
    theorem Matrix.IsSkewSymmetric.apply_neg {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] {A : Matrix n n R} (hA : A.IsSkewSymmetric) (i j : n) :
    A i j = -A j i

    For a skew-symmetric matrix, A i j = -A j i.

    source
    theorem Matrix.IsSkewSymmetric.reindex {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] {R : Type u_3} [Ring R] {A : Matrix n n R} (hA : A.IsSkewSymmetric) (e : n ≃ m) :
    ((Matrix.reindex e e) A).IsSkewSymmetric

    Skew-symmetry is preserved under reindexing.

    source
    theorem Matrix.IsSkewSymmetric.map {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} {S : Type u_3} [Ring R] [Ring S] {A : Matrix n n R} (hA : A.IsSkewSymmetric) (f : R → S) (hf : ∀ (x : R), f (-x) = -f x) :
    (A.map f).IsSkewSymmetric

    Skew-symmetry is preserved under map when the map preserves negation.

    source
    theorem Matrix.IsSkewSymmetric.smul {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] {A : Matrix n n R} (hA : A.IsSkewSymmetric) (c : R) :
    (c • A).IsSkewSymmetric

    Skew-symmetry is preserved under scalar multiplication.

    source
    theorem Matrix.IsSkewSymmetric.zero {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] :
    IsSkewSymmetric 0

    The zero matrix is skew-symmetric.

    source
    theorem Matrix.IsSkewSymmetric.add {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] {A B : Matrix n n R} (hA : A.IsSkewSymmetric) (hB : B.IsSkewSymmetric) :
    (A + B).IsSkewSymmetric

    The sum of skew-symmetric matrices is skew-symmetric.

    source
    theorem Matrix.IsSkewSymmetric.neg {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] {A : Matrix n n R} (hA : A.IsSkewSymmetric) :
    (-A).IsSkewSymmetric

    The negation of a skew-symmetric matrix is skew-symmetric.

    source
    theorem Matrix.IsSkewSymmetric.sub {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] {A B : Matrix n n R} (hA : A.IsSkewSymmetric) (hB : B.IsSkewSymmetric) :
    (A - B).IsSkewSymmetric

    The difference of two skew-symmetric matrices is skew-symmetric.

    source
    theorem Matrix.IsSkewSymmetric.det_eq_zero_of_odd {n : ℕ} {R : Type u_1} [CommRing R] [NoZeroDivisors R] [CharZero R] (A : Matrix (Fin (2 * n + 1)) (Fin (2 * n + 1)) R) (hA : A.IsSkewSymmetric) :
    A.det = 0

    The determinant of an odd-dimensional skew-symmetric matrix is zero. This follows from det(A) = det(Aᵀ) = det(-A) = (-1)^n det(A) = -det(A), hence 2 det(A) = 0, so det(A) = 0 (in characteristic ≠ 2).