Determinants and matrix identities

Determinant expansions and identities, determinants of special products and exponentials, derivatives of determinants, and algebraic identities between matrices.

• Decomposition of the bit-swap permutation matrix
• First-order expansion of the determinant
• Generalized factorial matrices
• Matrix determinant lemma
• Matrix exponential

TheoremCarroll (Desnanot–Jacobi) identity#✓fully proved

Let \(R\) be a commutative ring, let \(n\) be a natural number, and let \(C\) be an \((n + 2) \times (n + 2)\) matrix over \(R\). For indices \(a\) and \(b\), write \(C^{a}_{b}\) for the \((n + 1) \times (n + 1)\) matrix obtained from \(C\) by deleting row \(a\) and column \(b\). Let \(i \ne j\) be distinct indices and let \(C^{ij}_{ij}\) be the \(n \times n\) matrix obtained from \(C\) by deleting rows \(i\) and \(j\) and columns \(i\) and \(j\). Then

\[\det C \cdot \det C^{ij}_{ij} = \det C^{i}_{i} \det C^{j}_{j} - \det C^{i}_{j} \det C^{j}_{i}.\]

For \(n = 0\) the matrix \(C^{ij}_{ij}\) is empty and its determinant is \(1\).

theorem carroll_identity
    (n : ℕ) (R : Type _) [CommRing R]
    (C : Matrix (Fin (n + 2)) (Fin (n + 2)) R) (i j : Fin (n + 2)) (hij : i ≠ j) :
    Matrix.det C * Matrix.det (Matrix.submatrix C
      (Subtype.val : {k : Fin (n + 2) // k ≠ i ∧ k ≠ j} → Fin (n + 2))
      (Subtype.val : {k : Fin (n + 2) // k ≠ i ∧ k ≠ j} → Fin (n + 2))) =
    Matrix.det (Matrix.submatrix C (Fin.succAbove i) (Fin.succAbove i)) *
      Matrix.det (Matrix.submatrix C (Fin.succAbove j) (Fin.succAbove j)) -
    Matrix.det (Matrix.submatrix C (Fin.succAbove i) (Fin.succAbove j)) *
      Matrix.det (Matrix.submatrix C (Fin.succAbove j) (Fin.succAbove i))

Sources

• Charles Delorme and Guillermo Pineda-Villavicencio, "Quadratic Form Representations via Generalized Continuants", Journal of Integer Sequences 18 (2015), Article 15.6.4, displayed lemma lines 133–142. https://cs.uwaterloo.ca/journals/JIS/VOL18/Pineda/pin2.tex. The source cites C. L. Dodgson, "Condensation of determinants, being a new and brief method for computing their arithmetical values", Proc. Roy. Soc. Lond. 15 (1866), 150–155.

TheoremJacobi's formula#●ready to prove

Let \(n\) be a finite type, and let \(A\) be a curve \(\mathbb{R} \to \mathbb{R}^{n \times n}\) of square real matrices with rows and columns indexed by \(n\). Suppose \(A\) is differentiable at \(t \in \mathbb{R}\). Then the derivative of \(s \mapsto \det A(s)\) at \(t\) is \(\operatorname{tr}\bigl(\operatorname{adj}(A(t))\, A'(t)\bigr)\), where \(\operatorname{adj}\) denotes the adjugate matrix and \(A'(t)\) the derivative of \(A\) at \(t\).

public theorem_wanted jacobi_det_derivative
    (A : ℝ → Matrix n n ℝ) (t : ℝ) (hA : DifferentiableAt ℝ A t) :
    deriv (fun t => Matrix.det (A t)) t
      = Matrix.trace (Matrix.adjugate (A t) * deriv A t)

Sources

• R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge Univ. Press, 2013, §0.8.10; https://en.wikipedia.org/wiki/Jacobi%27s_formula

TheoremSymmetry criterion for matrices indexed by a product#✓fully proved

A matrix on a product is symmetric exactly when its restrictions to each row and column are symmetric and both diagonals of every ordered rectangle agree in opposite directions.

theorem isSymm_prod_iff {A : Matrix (ρ × γ) (ρ × γ) α} :
    A.IsSymm ↔
      (∀ a, (A.submatrix (a, ·) (a, ·)).IsSymm) ∧
      (∀ i, (A.submatrix (·, i) (·, i)).IsSymm) ∧
      ∀ a b i j, a < b → i < j →
        A (a, i) (b, j) = A (b, j) (a, i) ∧
          A (a, j) (b, i) = A (b, i) (a, j)

Used by 1

Used byComplete-graph tensor value as a crossing grid evaluation

TheoremSymplectic matrices have determinant one#●ready to prove

Let \(R\) be a commutative ring, \(l\) a finite set, \(I\) the identity matrix indexed by \(l\), and \(J = \begin{pmatrix} 0 & -I \\ I & 0 \end{pmatrix}\) the matrix over \(R\) indexed by the disjoint union \(l \sqcup l\). Every square matrix \(A\) over \(R\) indexed by \(l \sqcup l\) with \(A J A^{\mathsf{T}} = J\) satisfies \(\det A = 1\).

public theorem_wanted symplectic_matrix_det
    {l R : Type*} [DecidableEq l] [Fintype l] [CommRing R]
    {A : Matrix (l ⊕ l) (l ⊕ l) R} (_hA : A ∈ Matrix.symplecticGroup l R) :
    A.det = 1

Sources

• Folklore (Pfaffian computation). Listed as §39 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem symplectic_matrix_det of the lean-eval benchmark.

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.