5.1 Determinants: Basic Properties

5.1.1 Conventions

Convention 5.1

For the rest of this section, we fix a commutative ring \(K\). In most examples, \(K\) will be \(\mathbb {Z}\) or \(\mathbb {Q}\) or a polynomial ring.

Convention 5.2

Let \(n, m \in \mathbb {N}\).

(a) If \(A\) is an \(n \times m\)-matrix, then \(A_{i,j}\) shall mean the \((i,j)\)-th entry of \(A\), that is, the entry of \(A\) in row \(i\) and column \(j\).

(b) If \(a_{i,j}\) is an element of \(K\) for each \(i \in [n]\) and each \(j \in [m]\), then

\[ \left( a_{i,j} \right)_{1 \leq i \leq n,\; 1 \leq j \leq m} \]

shall denote the \(n \times m\)-matrix whose \((i,j)\)-th entry is \(a_{i,j}\) for all \(i \in [n]\) and \(j \in [m]\).

(c) We let \(K^{n \times m}\) denote the set of all \(n \times m\)-matrices with entries in \(K\). This is a \(K\)-module. If \(n = m\), this is also a \(K\)-algebra.

(d) Let \(A \in K^{n \times m}\) be an \(n \times m\)-matrix. The transpose \(A^T\) of \(A\) is defined to be the \(m \times n\)-matrix whose entries are given by

\[ \left( A^T \right)_{i,j} = A_{j,i} \quad \text{for all } i \in [m] \text{ and } j \in [n]. \]

5.1.2 Definition

Definition 5.3

✓

Let \(n \in \mathbb {N}\). Let \(A \in K^{n \times n}\) be an \(n \times n\)-matrix. The determinant \(\det A\) of \(A\) is defined to be the element

\[ \sum _{\sigma \in S_n} (-1)^{\sigma } \underbrace{A_{1,\sigma (1)} A_{2,\sigma (2)} \cdots A_{n,\sigma (n)}}_{ = \prod _{i=1}^{n} A_{i,\sigma (i)}} \]

of \(K\). Here:

we let \(S_n\) denote the \(n\)-th symmetric group (i.e., the group of permutations of \([n] = \{ 1, 2, \ldots , n\} \));
we let \((-1)^{\sigma }\) denote the sign of the permutation \(\sigma \) (as defined in Definition 3.109).

docs source

theorem AlgebraicCombinatorics.Det.det_eq_sum_sign_prod_textbook {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) :

A.det = ∑ σ : Equiv.Perm (Fin n), Equiv.Perm.sign σ • ∏ i : Fin n, A i (σ i)

5.1.3 Small determinants and basic API

Lemma 5.4

✓

The determinant of a \(0 \times 0\) matrix is \(1\) (empty product convention).

docs source

theorem AlgebraicCombinatorics.Det.det_fin_zero' {K : Type u_1} [CommRing K] (A : Matrix (Fin 0) (Fin 0) K) :

A.det = 1

Proof ▶

The sum over \(S_0 = \{ \mathrm{id}\} \) gives \((-1)^{\mathrm{id}} \cdot 1 = 1\) (empty product is \(1\)).

Lemma 5.5

✓

The determinant of a \(1 \times 1\) matrix is its single entry: \(\det (a) = a\).

docs source

theorem AlgebraicCombinatorics.Det.det_fin_one' {K : Type u_1} [CommRing K] (A : Matrix (Fin 1) (Fin 1) K) :

A.det = A 0 0

Proof ▶

The sum over \(S_1 = \{ \mathrm{id}\} \) gives \((-1)^{\mathrm{id}} \cdot a = a\).

Lemma 5.6

✓

The determinant of a \(2 \times 2\) matrix satisfies \(\det \begin{pmatrix} a & b \\ c & d \end{pmatrix} = ad - bc\).

docs source

theorem AlgebraicCombinatorics.Det.det_fin_two' {K : Type u_1} [CommRing K] (A : Matrix (Fin 2) (Fin 2) K) :

A.det = A 0 0 * A 1 1 - A 0 1 * A 1 0

Proof ▶

\(S_2\) has two elements: the identity (sign \(+1\)) and the transposition (sign \(-1\)). The sum gives \(a \cdot d - b \cdot c\).

Lemma 5.7

✓

The determinant of the identity matrix is \(1\): \(\det I_n = 1\).

docs source

theorem AlgebraicCombinatorics.Det.det_one_eq_one {K : Type u_1} [CommRing K] {n : ℕ} :

Matrix.det 1 = 1

Proof ▶

By the fact that the identity matrix has determinant \(1\).

Lemma 5.8

✓

For \(n \geq 1\), the determinant of the zero matrix is \(0\). (For \(n = 0\), the zero matrix is the empty matrix, and \(\det (\emptyset ) = 1\).)

docs source

theorem AlgebraicCombinatorics.Det.det_zero_eq_zero {K : Type u_1} [CommRing K] {n : ℕ} (hn : 0 < n) :

Matrix.det 0 = 0

Proof ▶

The zero matrix has a zero row, so \(\det = 0\) by Theorem 5.20 (b).

Lemma 5.9

✓

The determinant of a diagonal matrix equals the product of its diagonal entries: \(\det (\mathrm{diag}(d_1, \ldots , d_n)) = d_1 d_2 \cdots d_n\).

docs source

theorem AlgebraicCombinatorics.Det.det_diagonal' {K : Type u_1} [CommRing K] {n : ℕ} (d : Fin n → K) :

(Matrix.diagonal d).det = ∏ i : Fin n, d i

Proof ▶

A diagonal matrix is both upper- and lower-triangular, so this follows from Theorem 5.19.

Lemma 5.10

✓

For \(n \geq 2\), a matrix with all entries equal to \(c\) has determinant \(0\). This is a corollary of Proposition 5.12 with \(x_i = 1\) and \(y_j = c\).

docs source

theorem AlgebraicCombinatorics.Det.det_const_matrix_eq_zero {K : Type u_1} [CommRing K] {n : ℕ} (c : K) (hn : 2 ≤ n) :

(Matrix.of fun (x x_1 : Fin n) => c).det = 0

Proof ▶

The constant matrix \((c)_{i,j}\) is the outer product of \(\mathbf{1}\) and \((c, c, \ldots , c)\). By Proposition 5.12, its determinant is \(0\).

Lemma 5.11

✓

Let \(n \geq 2\). Then,

\[ \sum _{\sigma \in S_n} (-1)^{\sigma } = 0. \]

docs source

theorem AlgebraicCombinatorics.Det.sum_sign_eq_zero {K : Type u_1} [CommRing K] {n : ℕ} (hn : 2 ≤ n) :

∑ σ : Equiv.Perm (Fin n), ↑↑(Equiv.Perm.sign σ) = 0

Proof ▶

The proof uses a sign-reversing involution: for \(n \geq 2\), pick two distinct elements \(i, j\) and their transposition \(t_{i,j}\). The map \(\sigma \mapsto \sigma \cdot t_{i,j}\) pairs up permutations with opposite signs, so all summands cancel.

Proposition 5.12

✓

Let \(n \in \mathbb {N}\) be such that \(n \geq 2\). Let \(x_1, x_2, \ldots , x_n \in K\) and \(y_1, y_2, \ldots , y_n \in K\). Then,

\[ \det \left( \left( x_i y_j \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right) = 0. \]

docs source

theorem AlgebraicCombinatorics.Det.det_outerProduct_eq_zero {K : Type u_1} [CommRing K] {n : ℕ} (x y : Fin n → K) (hn : 2 ≤ n) :

(outerProductMatrix x y).det = 0

Proof ▶

The definition of the determinant yields (using Lemma 5.11 for the last step)

\begin{align*} \det \left( \left( x_i y_j \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right) & = \sum _{\sigma \in S_n} (-1)^{\sigma } \underbrace{(x_1 y_{\sigma (1)})(x_2 y_{\sigma (2)}) \cdots (x_n y_{\sigma (n)})}_{ = (x_1 x_2 \cdots x_n)(y_{\sigma (1)} y_{\sigma (2)} \cdots y_{\sigma (n)})} \\ & = \sum _{\sigma \in S_n} (-1)^{\sigma } (x_1 x_2 \cdots x_n) \underbrace{(y_{\sigma (1)} y_{\sigma (2)} \cdots y_{\sigma (n)})}_{\substack{[ , =, , y, _, 1, , y, _, 2, , \cdots , y, _, n, , \\ , , \text , {, (, s, i, n, c, e, , }, , \sigma , \text , {, , i, s, , a, , b, i, j, e, c, t, i, o, n, ), }]}} \\ & = (x_1 x_2 \cdots x_n)(y_1 y_2 \cdots y_n) \underbrace{\sum _{\sigma \in S_n} (-1)^{\sigma }}_{= 0} = 0. \end{align*}

Lemma 5.13

✓

Let \(A\) be a \(5 \times 5\) matrix such that \(A_{i,j} = 0\) whenever \(i, j \in \{ 2, 3, 4\} \). Then \(\det A = 0\). This formalizes the \(5 \times 5\) hollow matrix example: a matrix with a \(3 \times 3\) block of zeros in the middle has determinant \(0\).

docs source

theorem AlgebraicCombinatorics.Det.det_hollow_core_eq_zero {K : Type u_1} [CommRing K] (A : Matrix (Fin 5) (Fin 5) K) (hA : ∀ (i j : Fin 5), ↑i ∈ {1, 2, 3} → ↑j ∈ {1, 2, 3} → A i j = 0) :

A.det = 0

Proof ▶

By the pigeonhole principle: any permutation \(\sigma \) of \([5]\) must map some element of \(\{ 2,3,4\} \) to an element of \(\{ 2,3,4\} \), because \(|\{ 2,3,4\} | = 3 {\gt} 2 = |\{ 1,5\} |\). Hence, for every \(\sigma \), the product \(\prod _i A_{i,\sigma (i)}\) contains a zero factor, making every term in the determinant sum equal to \(0\).

5.1.4 Helpers for Proposition 5.17

Lemma 5.14

✓

The factor matrix \(A\) in the factorization of the sum matrix \((x_i + y_j)\) has a zero column (column index \(2\)) when \(n \geq 3\). The matrix \(A\) has \(x_i\) in the first column, \(1\) in the second column, and \(0\) elsewhere.

docs source

theorem AlgebraicCombinatorics.Det.sumMatrix_factorA_has_zero_col {K : Type u_1} [CommRing K] {n : ℕ} (x : Fin n → K) (hn : 3 ≤ n) (i : Fin n) :

sumMatrix_factorA x i ⟨2, ⋯⟩ = 0

Proof ▶

By direct computation: for column index \(2\), neither \(j = 0\) nor \(j = 1\), so the entry is \(0\).

Lemma 5.15

✓

For \(n \geq 3\), the factor matrix \(A\) has determinant \(0\).

docs source

theorem AlgebraicCombinatorics.Det.det_sumMatrix_factorA_eq_zero {K : Type u_1} [CommRing K] {n : ℕ} (x : Fin n → K) (hn : 3 ≤ n) :

(sumMatrix_factorA x).det = 0

Proof ▶

By Lemma 5.14, column \(2\) is zero. By Theorem 5.21 (b), \(\det A = 0\).

Lemma 5.16

✓

For \(n \geq 2\), the matrix \((x_i + y_j)_{i,j}\) factors as \(A \cdot B\) where:

\[ A_{i,j} = \begin{cases} x_i & \text{if } j = 0, \\ 1 & \text{if } j = 1, \\ 0 & \text{otherwise,} \end{cases} \qquad B_{i,j} = \begin{cases} 1 & \text{if } i = 0, \\ y_j & \text{if } i = 1, \\ 0 & \text{otherwise.} \end{cases} \]

docs source

theorem AlgebraicCombinatorics.Det.sumMatrix_eq_factorA_mul_factorB {K : Type u_1} [CommRing K] {n : ℕ} (x y : Fin n → K) (hn : 2 ≤ n) :

sumMatrix x y = sumMatrix_factorA x * sumMatrix_factorB y

Proof ▶

Direct matrix multiplication: \((AB)_{i,j} = \sum _k A_{i,k} B_{k,j} = x_i \cdot 1 + 1 \cdot y_j = x_i + y_j\).

Proposition 5.17

✓

Let \(n \in \mathbb {N}\) be such that \(n \geq 3\). Let \(x_1, x_2, \ldots , x_n \in K\) and \(y_1, y_2, \ldots , y_n \in K\). Then,

\[ \det \left( \left( x_i + y_j \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right) = 0. \]

docs source

theorem AlgebraicCombinatorics.Det.det_sumMatrix_eq_zero {K : Type u_1} [CommRing K] {n : ℕ} (x y : Fin n → K) (hn : 3 ≤ n) :

(sumMatrix x y).det = 0

Proof ▶

Define two \(n \times n\)-matrices

\[ A := \begin{pmatrix} x_1 & 1 & 0 & \cdots & 0 \\ x_2 & 1 & 0 & \cdots & 0 \\ x_3 & 1 & 0 & \cdots & 0 \\ \vdots & \vdots & \vdots & \ddots & \vdots \\ x_n & 1 & 0 & \cdots & 0 \end{pmatrix} \quad \text{and} \quad B := \begin{pmatrix} 1 & 1 & 1 & \cdots & 1 \\ y_1 & y_2 & y_3 & \cdots & y_n \\ 0 & 0 & 0 & \cdots & 0 \\ \vdots & \vdots & \vdots & \ddots & \vdots \\ 0 & 0 & 0 & \cdots & 0 \end{pmatrix}. \]

Then \(\left( x_i + y_j \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} = AB\), so

\[ \det \left( \left( x_i + y_j \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right) = \det (AB) = \det A \cdot \det B \]

(by Theorem 5.23). However, the matrix \(A\) has a zero column (since \(n \geq 3\)), and thus \(\det A = 0\) (by Theorem 5.21 (b)). Hence the product is \(0\).

5.1.5 Basic properties

Theorem 5.18 Transposes preserve determinants

✓

Let \(n \in \mathbb {N}\). If \(A \in K^{n \times n}\) is any \(n \times n\)-matrix, then \(\det (A^T) = \det A\).

docs source

theorem AlgebraicCombinatorics.Det.det_transpose' {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) :

A.transpose.det = A.det

Proof ▶

See [ Strick13 , Corollary B.16 ] or [ Grinbe15 , Exercise 6.4 ] or [ Laue15 , § 5.3.2 ] .

Theorem 5.19 Determinants of triangular matrices

✓

Let \(n \in \mathbb {N}\). Let \(A \in K^{n \times n}\) be a triangular (i.e., lower-triangular or upper-triangular) \(n \times n\)-matrix. Then, the determinant of the matrix \(A\) is the product of its diagonal entries. That is,

\[ \det A = A_{1,1} A_{2,2} \cdots A_{n,n}. \]

docs source

theorem AlgebraicCombinatorics.Det.det_upperTriangular {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (hA : ∀ (i j : Fin n), j < i → A i j = 0) :

A.det = ∏ i : Fin n, A i i

docs source

theorem AlgebraicCombinatorics.Det.det_lowerTriangular {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (hA : ∀ (i j : Fin n), i < j → A i j = 0) :

A.det = ∏ i : Fin n, A i i

Proof ▶

See [ Strick13 , Proposition B.11 ] or [ Grinbe15 , Exercise 6.3 and the paragraph after Exercise 6.4 ] .

Theorem 5.20 Row operation properties

✓

Let \(n \in \mathbb {N}\). Let \(A \in K^{n \times n}\) be an \(n \times n\)-matrix. Then:

(a) If we swap two rows of \(A\), then \(\det A\) gets multiplied by \(-1\).

(b) If \(A\) has a zero row (i.e., a row that consists entirely of zeroes), then \(\det A = 0\).

(c) If \(A\) has two equal rows, then \(\det A = 0\).

(d) Let \(\lambda \in K\). If we multiply a row of \(A\) by \(\lambda \) (that is, we multiply all entries of this one row by \(\lambda \), while leaving all other entries of \(A\) unchanged), then \(\det A\) gets multiplied by \(\lambda \).

(e) If we add a row of \(A\) to another row of \(A\) (that is, we add each entry of the former row to the corresponding entry of the latter), then \(\det A\) stays unchanged.

(f) Let \(\lambda \in K\). If we add \(\lambda \) times a row of \(A\) to another row of \(A\) (that is, we add \(\lambda \) times each entry of the former row to the corresponding entry of the latter), then \(\det A\) stays unchanged.

(g) Let \(B, C \in K^{n \times n}\) be two further \(n \times n\)-matrices. Let \(k \in [n]\). Assume that

\[ (\text{the } k\text{-th row of } C) = (\text{the } k\text{-th row of } A) + (\text{the } k\text{-th row of } B), \]

whereas each \(i \neq k\) satisfies

\[ (\text{the } i\text{-th row of } C) = (\text{the } i\text{-th row of } A) = (\text{the } i\text{-th row of } B). \]

Then,

\[ \det C = \det A + \det B. \]

docs source

theorem AlgebraicCombinatorics.Det.det_swap_rows {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (i j : Fin n) (hij : i ≠ j) :

(Matrix.of (A ∘ ⇑(Equiv.swap i j))).det = -A.det

docs source

theorem AlgebraicCombinatorics.Det.det_zero_row {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (i : Fin n) (hi : ∀ (j : Fin n), A i j = 0) :

A.det = 0

docs source

theorem AlgebraicCombinatorics.Det.det_eq_rows {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (i j : Fin n) (hij : i ≠ j) (hrows : A i = A j) :

A.det = 0

docs source

theorem AlgebraicCombinatorics.Det.det_scale_row {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (i : Fin n) (c : K) :

(A.updateRow i (c • A i)).det = c * A.det

docs source

theorem AlgebraicCombinatorics.Det.det_add_row {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (i j : Fin n) (hij : i ≠ j) :

(A.updateRow i (A i + A j)).det = A.det

docs source

theorem AlgebraicCombinatorics.Det.det_add_smul_row {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (i j : Fin n) (hij : i ≠ j) (c : K) :

(A.updateRow i (A i + c • A j)).det = A.det

docs source

theorem AlgebraicCombinatorics.Det.det_row_add {K : Type u_1} [CommRing K] {n : ℕ} (A B C : Matrix (Fin n) (Fin n) K) (k : Fin n) (hk : C k = A k + B k) (hother : ∀ (i : Fin n), i ≠ k → C i = A i ∧ A i = B i) :

C.det = A.det + B.det

Proof ▶

(a) See [ Grinbe15 , Exercise 6.7 (a) ] . This is also a particular case of [ Strick13 , Corollary B.19 ] .

(b) See [ Grinbe15 , Exercise 6.7 (c) ] . This is also near-obvious from Definition 5.3.

(c) See [ Grinbe15 , Exercise 6.7 (e) ] or [ Laue15 , § 5.3.3, property (iii) ] .

(d) See [ Grinbe15 , Exercise 6.7 (g) ] or [ Laue15 , § 5.3.3, property (ii) ] .

(f) See [ Grinbe15 , Exercise 6.8 (a) ] .

(e) This is the particular case of part (f) for \(\lambda = 1\).

(g) See [ Grinbe15 , Exercise 6.7 (i) ] or [ Laue15 , § 5.3.3, property (i) ] .

Theorem 5.21 Column operation properties

✓

Theorem 5.20 also holds if we replace “row” by “column” throughout it.

docs source

theorem AlgebraicCombinatorics.Det.det_swap_cols {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (i j : Fin n) (hij : i ≠ j) :

(A.submatrix id ⇑(Equiv.swap i j)).det = -A.det

docs source

theorem AlgebraicCombinatorics.Det.det_zero_col {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (j : Fin n) (hj : ∀ (i : Fin n), A i j = 0) :

A.det = 0

docs source

theorem AlgebraicCombinatorics.Det.det_eq_cols {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (i j : Fin n) (hij : i ≠ j) (hcols : ∀ (k : Fin n), A k i = A k j) :

A.det = 0

docs source

theorem AlgebraicCombinatorics.Det.det_scale_col {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (j : Fin n) (c : K) :

(Matrix.of fun (i k : Fin n) => if k = j then c * A i k else A i k).det = c * A.det

docs source

theorem AlgebraicCombinatorics.Det.det_add_col {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (i j : Fin n) (hij : i ≠ j) :

(A.updateCol i fun (k : Fin n) => A k i + A k j).det = A.det

docs source

theorem AlgebraicCombinatorics.Det.det_add_smul_col {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (i j : Fin n) (hij : i ≠ j) (c : K) :

(A.updateCol i fun (k : Fin n) => A k i + c * A k j).det = A.det

docs source

theorem AlgebraicCombinatorics.Det.det_col_add {K : Type u_1} [CommRing K] {n : ℕ} (A B C : Matrix (Fin n) (Fin n) K) (k : Fin n) (hk : ∀ (i : Fin n), C i k = A i k + B i k) (hother : ∀ (i j : Fin n), j ≠ k → C i j = A i j ∧ A i j = B i j) :

C.det = A.det + B.det

Proof ▶

Theorem 5.18 shows that the determinant of a matrix does not change when we replace it by its transpose; however, the rows of this transpose \(A^T\) are the transposes of the columns of \(A\). Thus, Theorem 5.21 follows by applying Theorem 5.20 to the transposes of all the matrices involved.

Corollary 5.22

✓

Let \(n \in \mathbb {N}\). Let \(A \in K^{n \times n}\) and \(\tau \in S_n\). Then,

\begin{equation} \det \left( \left( A_{\tau (i), j} \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right) = (-1)^{\tau } \cdot \det A \label{eq.cor.det.sig-row-col.row} \end{equation}

and

\begin{equation} \det \left( \left( A_{i, \tau (j)} \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right) = (-1)^{\tau } \cdot \det A. \label{eq.cor.det.sig-row-col.col} \end{equation}

docs source

theorem AlgebraicCombinatorics.Det.det_permute_rows {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (τ : Equiv.Perm (Fin n)) :

(A.submatrix (⇑τ) id).det = ↑↑(Equiv.Perm.sign τ) * A.det

docs source

theorem AlgebraicCombinatorics.Det.det_permute_cols {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (τ : Equiv.Perm (Fin n)) :

(A.submatrix id ⇑τ).det = ↑↑(Equiv.Perm.sign τ) * A.det

Proof ▶

Let us first prove 8.

The definition of \(\det A\) yields

\begin{align*} \det A & = \sum _{\sigma \in S_n} (-1)^{\sigma } \prod _{i=1}^{n} A_{i, \sigma (i)}. \end{align*}

The definition of \(\det \left( \left( A_{i, \tau (j)} \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right)\) yields

\begin{align*} \det \left( \left( A_{i, \tau (j)} \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right) & = \sum _{\sigma \in S_n} (-1)^{\sigma } \prod _{i=1}^{n} A_{i, \tau (\sigma (i))}. \end{align*}

However, \(S_n\) is a group. Thus, the map \(\sigma \mapsto \tau ^{-1} \sigma \) is a bijection on \(S_n\). Substituting \(\tau ^{-1} \sigma \) for \(\sigma \), we obtain (using Proposition 3.110 (d) and (f))

\begin{align*} & \sum _{\sigma \in S_n} (-1)^{\sigma } \prod _{i=1}^{n} A_{i, \tau (\sigma (i))} \\ & = \sum _{\sigma \in S_n} \underbrace{(-1)^{\tau ^{-1} \sigma }}_{ = (-1)^{\tau ^{-1}} \cdot (-1)^{\sigma }} \prod _{i=1}^{n} \underbrace{A_{i, \tau ((\tau ^{-1} \sigma )(i))}}_{= A_{i, \sigma (i)}} \\ & = \underbrace{(-1)^{\tau ^{-1}}}_{= (-1)^{\tau }} \cdot \underbrace{\sum _{\sigma \in S_n} (-1)^{\sigma } \prod _{i=1}^{n} A_{i, \sigma (i)}}_{= \det A} \\ & = (-1)^{\tau } \cdot \det A. \end{align*}

This proves 8.

Now, 7 follows by applying 8 to \(A^T\) instead of \(A\) and using Theorem 5.18.

Theorem 5.23 Multiplicativity of the determinant

✓

Let \(n \in \mathbb {N}\). Let \(A, B \in K^{n \times n}\) be two \(n \times n\)-matrices. Then,

\[ \det (AB) = \det A \cdot \det B. \]

docs source

theorem AlgebraicCombinatorics.Det.det_mul' {K : Type u_1} [CommRing K] {n : ℕ} (A B : Matrix (Fin n) (Fin n) K) :

(A * B).det = A.det * B.det

Proof ▶

See [ Strick13 , Theorem B.17 ] or [ Grinbe15 , Theorem 6.23 ] or [ Zeilbe85 , § 5 ] or [ Ford21 , Lemma 4.7.5 (1) ] or [ Laue15 , Theorem 5.7 ] .

Corollary 5.24

✓

Let \(n \in \mathbb {N}\). Let \(A \in K^{n \times n}\) and \(d_1, d_2, \ldots , d_n \in K\). Then,

\begin{equation} \det \left( \left( d_i A_{i,j} \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right) = d_1 d_2 \cdots d_n \cdot \det A \label{eq.cor.det.scale-row-col.row} \end{equation}

and

\begin{equation} \det \left( \left( d_j A_{i,j} \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right) = d_1 d_2 \cdots d_n \cdot \det A. \label{eq.cor.det.scale-row-col.col} \end{equation}

docs source

theorem AlgebraicCombinatorics.Det.det_scale_rows {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (d : Fin n → K) :

(Matrix.of fun (i j : Fin n) => d i * A i j).det = (∏ i : Fin n, d i) * A.det

docs source

theorem AlgebraicCombinatorics.Det.det_scale_cols {K : Type u_1} [CommRing K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) (d : Fin n → K) :

(Matrix.of fun (i j : Fin n) => d j * A i j).det = (∏ j : Fin n, d j) * A.det

Proof ▶

The definition of a determinant yields

\[ \det A = \sum _{\sigma \in S_n} (-1)^{\sigma } A_{1,\sigma (1)} A_{2,\sigma (2)} \cdots A_{n,\sigma (n)} \]

and

\begin{align*} & \det \left( \left( d_i A_{i,j} \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right) \\ & = \sum _{\sigma \in S_n} (-1)^{\sigma } \underbrace{(d_1 A_{1,\sigma (1)})(d_2 A_{2,\sigma (2)}) \cdots (d_n A_{n,\sigma (n)})}_{ = (d_1 d_2 \cdots d_n)(A_{1,\sigma (1)} A_{2,\sigma (2)} \cdots A_{n,\sigma (n)})} \\ & = d_1 d_2 \cdots d_n \cdot \underbrace{\sum _{\sigma \in S_n} (-1)^{\sigma } A_{1,\sigma (1)} A_{2,\sigma (2)} \cdots A_{n,\sigma (n)}}_{= \det A} \\ & = d_1 d_2 \cdots d_n \cdot \det A \end{align*}

and

\begin{align*} & \det \left( \left( d_j A_{i,j} \right)_{1 \leq i \leq n,\; 1 \leq j \leq n} \right) \\ & = \sum _{\sigma \in S_n} (-1)^{\sigma } \underbrace{(d_{\sigma (1)} A_{1,\sigma (1)})(d_{\sigma (2)} A_{2,\sigma (2)}) \cdots (d_{\sigma (n)} A_{n,\sigma (n)})}_{ = (d_{\sigma (1)} d_{\sigma (2)} \cdots d_{\sigma (n)}) (A_{1,\sigma (1)} A_{2,\sigma (2)} \cdots A_{n,\sigma (n)})} \\ & = \sum _{\sigma \in S_n} (-1)^{\sigma } \underbrace{(d_{\sigma (1)} d_{\sigma (2)} \cdots d_{\sigma (n)})}_{\substack{[ , =, , d, _, 1, , d, _, 2, , \cdots , d, _, n, , \\ , , \text , {, (, s, i, n, c, e, , }, , \sigma , \text , {, , i, s, , a, , p, e, r, m, u, t, a, t, i, o, n, , o, f, , }, , [, n, ], , \text , {, ), }]}} (A_{1,\sigma (1)} A_{2,\sigma (2)} \cdots A_{n,\sigma (n)}) \\ & = d_1 d_2 \cdots d_n \cdot \det A. \end{align*}

5.1.6 Permutation images and submatrix determinants

Definition 5.25

✓

The image of a finite subset \(P \subseteq [n]\) under a permutation \(\sigma \in S_n\) is \(\sigma (P) = \{ \sigma (i) \mid i \in P\} \).

docs source

def PermFinset.imageFinset {n : ℕ} (σ : Equiv.Perm (Fin n)) (P : Finset (Fin n)) :

Finset (Fin n)

PermFinset.imageFinset σ P = Finset.map { toFun := ⇑σ, inj' := ⋯ } P

Lemma 5.26

✓

The image of a finset under a permutation has the same cardinality: \(|\sigma (P)| = |P|\).

docs source

theorem PermFinset.imageFinset_card {n : ℕ} (σ : Equiv.Perm (Fin n)) (P : Finset (Fin n)) :

(imageFinset σ P).card = P.card

Proof ▶

Since \(\sigma \) is injective, the image has the same cardinality as the original set.

Lemma 5.27

✓

The image of a complement equals the complement of the image: \(\sigma (P^c) = \sigma (P)^c\).

docs source

theorem PermFinset.imageFinset_compl {n : ℕ} (σ : Equiv.Perm (Fin n)) (P : Finset (Fin n)) :

imageFinset σ Pᶜ = (imageFinset σ P)ᶜ

Proof ▶

By the injectivity of \(\sigma \): \(x \in \sigma (P^c)\) iff \(\sigma ^{-1}(x) \notin P\) iff \(x \notin \sigma (P)\).

Lemma 5.28

✓

If \(\sigma (P) = Q\), then \(\sigma ^{-1}(Q) = P\).

docs source

theorem PermFinset.imageFinset_inv {n : ℕ} {σ : Equiv.Perm (Fin n)} {P Q : Finset (Fin n)} (h : imageFinset σ P = Q) :

imageFinset σ⁻¹ Q = P

Proof ▶

Apply \(\sigma ^{-1}\) to both sides of \(\sigma (P) = Q\) and use \(\sigma ^{-1} \circ \sigma = \mathrm{id}\).

Definition 5.29

✓

The set of permutations mapping \(P\) to \(Q\): \(\mathrm{permsMapping}(P, Q) = \{ \sigma \in S_n \mid \sigma (P) = Q\} \).

docs source

def PermFinset.permsMapping {n : ℕ} (P Q : Finset (Fin n)) :

Finset (Equiv.Perm (Fin n))

PermFinset.permsMapping P Q = {σ : Equiv.Perm (Fin n) | PermFinset.imageFinset σ P = Q}

Lemma 5.30

✓

If \(|P| \neq |Q|\), then no permutation maps \(P\) to \(Q\): \(\mathrm{permsMapping}(P, Q) = \emptyset \).

docs source

theorem PermFinset.permsMapping_empty_of_card_ne {n : ℕ} (P Q : Finset (Fin n)) (h : P.card ≠ Q.card) :

permsMapping P Q = ∅

Proof ▶

If \(\sigma (P) = Q\), then \(|Q| = |\sigma (P)| = |P|\) by Lemma 5.26, contradicting \(|P| \neq |Q|\).

Definition 5.31

✓

The submatrix determinant of an \(n \times n\) matrix \(A\) with row set \(P\) and column set \(Q\) (both subsets of \([n]\)) is

\[ \mathrm{submatrixDet}(A, P, Q) = \begin{cases} \det (A[P, Q]) & \text{if } |P| = |Q|, \\ 0 & \text{otherwise,} \end{cases} \]

where \(A[P, Q]\) is the submatrix of \(A\) with rows indexed by \(P\) and columns indexed by \(Q\), in the order determined by their natural ordering.

docs source

noncomputable def PermFinset.submatrixDet {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (P Q : Finset (Fin n)) :

PermFinset.submatrixDet A P Q = if h : P.card = Q.card then (A.submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(Q.orderEmbOfFin ⋯)).det else 0

Lemma 5.32

✓

When \(|P| = |Q|\), the submatrix determinant equals the actual determinant of the submatrix \(A[P, Q]\).

docs source

theorem PermFinset.submatrixDet_of_card_eq {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (P Q : Finset (Fin n)) (h : P.card = Q.card) :

submatrixDet A P Q = (A.submatrix ⇑(P.orderEmbOfFin ⋯) ⇑(Q.orderEmbOfFin ⋯)).det

Proof ▶

Immediate from the definitions, using the hypothesis \(|P| = |Q|\).

Lemma 5.33

✓

When \(|P| \neq |Q|\), the submatrix determinant is \(0\).

docs source

theorem PermFinset.submatrixDet_of_card_ne {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (P Q : Finset (Fin n)) (h : P.card ≠ Q.card) :

submatrixDet A P Q = 0

Proof ▶

Immediate from the definitions, using the hypothesis \(|P| \neq |Q|\).

Lemma 5.34

✓

The submatrix determinant of the empty row and column sets is \(1\): \(\mathrm{submatrixDet}(A, \emptyset , \emptyset ) = 1\).

docs source

theorem PermFinset.submatrixDet_empty {R : Type u_1} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) :

submatrixDet A ∅ ∅ = 1

Proof ▶

Both sets are empty (so \(|P| = |Q| = 0\)), and the determinant of the \(0 \times 0\) submatrix is \(1\).