Formalization Blueprint for “An Introduction to Algebraic Combinatorics” by Darij Grinberg

1.1 Notations and elementary facts

We will use the following notations and conventions:

  • The symbol \(\mathbb {N}\) will denote the set \(\left\{ 0,1,2,3,\ldots \right\} \) of nonnegative integers.

  • The size (i.e., cardinality) of a set \(A\) will be denoted by \(\left\vert A\right\vert \).

We will need some basics from enumerative combinatorics:

  • Addition principle (sum rule): If \(A\) and \(B\) are two disjoint sets, then \(\left\vert A\cup B\right\vert =\left\vert A\right\vert +\left\vert B\right\vert \).

  • Multiplication principle (product rule): If \(A\) and \(B\) are any two sets, then \(\left\vert A\times B\right\vert =\left\vert A\right\vert \cdot \left\vert B\right\vert \).

  • Bijection principle: There is a bijection between two sets \(X\) and \(Y\) if and only if \(\left\vert X\right\vert =\left\vert Y\right\vert \).

  • A set with \(n\) elements has \(2^{n}\) subsets, and has \(\binom {n}{k}\) size-\(k\) subsets for any \(k\in \mathbb {R}\).

  • A set with \(n\) elements has \(n!\) permutations.

1.1.1 Binomial coefficients

Definition 1.1
#

For any numbers \(n\) and \(k\), we set

\begin{equation} \binom {n}{k}=\begin{cases} \frac{n\left( n-1\right) \left( n-2\right) \cdots \left( n-k+1\right) }{k!}, & \text{if }k\in \mathbb {N};\\ 0, & \text{else.}\end{cases} \label{eq.def.binom.binom.eq}\end{equation}
1

Note that “numbers” is to be understood fairly liberally here. In particular, \(n\) can be any integer, rational, real or complex number (or, more generally, any element in a \(\mathbb {Q}\)-algebra), whereas \(k\) can be anything (although the only nonzero values of \(\binom {n}{k}\) will be achieved for \(k\in \mathbb {N}\), by the above definition).

Lemma 1.2

For any \(k\in \mathbb {N}\), we have \(\binom {-1}{k} = (-1)^k\).

Proof

We have

\begin{align*} \binom {-1}{k} & =\frac{\left( -1\right) \left( -1-1\right) \left( -1-2\right) \cdots \left( -1-k+1\right) }{k!}\\ & =\frac{\left( -1\right) \left( -2\right) \left( -3\right) \cdots \left( -k\right) }{k!}=\frac{\left( -1\right) ^{k}k!}{k!}=\left( -1\right) ^{k}. \end{align*}

If \(n,k\in \mathbb {N}\) and \(n\geq k\), then

\begin{equation} \binom {n}{k}=\frac{n!}{k!\left( n-k\right) !}. \label{eq.binom.fac-form}\end{equation}
4

But this formula only applies to the case when \(n,k\in \mathbb {N}\) and \(n\geq k\). The above definition is more general than it.

Lemma 1.3

For \(n,k\in \mathbb {N}\) with \(k \leq n\), we have \(\binom {n}{k}=\frac{n!}{k!\left( n-k\right) !}\).

Proof

This follows directly from the definition by cancellation.

Lemma 1.4

Let \(n\in \mathbb {N}\). Then, \(\binom {2n}{n}=\frac{1\cdot 3\cdot 5\cdot \cdots \cdot \left( 2n-1\right) }{n!}\cdot 2^{n}\).

Proof

We have

\begin{align*} \left( 2n\right) ! & =1\cdot 2\cdot \cdots \cdot \left( 2n\right) \\ & =\left( 1\cdot 3\cdot 5\cdot \cdots \cdot \left( 2n-1\right) \right) \cdot \underbrace{\left( 2\cdot 4\cdot 6\cdot \cdots \cdot \left( 2n\right) \right) }_{=2^{n}\left( 1\cdot 2\cdot \cdots \cdot n\right) }\\ & =\left( 1\cdot 3\cdot 5\cdot \cdots \cdot \left( 2n-1\right) \right) \cdot 2^{n}\underbrace{\left( 1\cdot 2\cdot \cdots \cdot n\right) }_{=n!}\\ & =\left( 1\cdot 3\cdot 5\cdot \cdots \cdot \left( 2n-1\right) \right) \cdot 2^{n}n!. \end{align*}

Now, (4) yields

\begin{align*} \binom {2n}{n} & =\frac{\left( 2n\right) !}{n!n!}=\frac{\left( 1\cdot 3\cdot 5\cdot \cdots \cdot \left( 2n-1\right) \right) \cdot 2^{n}n!}{n!\cdot n!}\\ & =\frac{1\cdot 3\cdot 5\cdot \cdots \cdot \left( 2n-1\right) }{n!}\cdot 2^{n}. \end{align*}
Proposition 1.5 Pascal’s identity, aka recurrence of the binomial coefficients

We have

\begin{equation} \binom {m}{n}=\binom {m-1}{n-1}+\binom {m-1}{n} \label{eq.binom.rec.m}\end{equation}
5

for any numbers \(m\) and \(n\).

Proof

This follows from the identity \(\binom {r+1}{k+1} = \binom {r}{k} + \binom {r}{k+1}\) (the successor form of Pascal’s identity) by substituting \(r = m - 1\) and \(k = n - 1\).

Lemma 1.6

For natural numbers \(m, n\) with \(m {\gt} 0\) and \(n {\gt} 0\), we have \(\binom {m}{n}=\binom {m-1}{n-1}+\binom {m-1}{n}\).

Proof

This is the natural number specialization of Proposition 1.5.

Lemma 1.7

For any element \(r\) in a binomial ring and \(k \in \mathbb {N}\), \(\binom {r+1}{k+1} = \binom {r}{k} + \binom {r}{k+1}\).

Proof

This is the successor form of Pascal’s identity, which is a standard result in Mathlib.

Proposition 1.8

Let \(m,n\in \mathbb {N}\) satisfy \(m{\lt}n\). Then, \(\binom {m}{n}=0\).

Proof

If \(m {\lt} n\), then in the product \(m(m-1)(m-2)\cdots (m-n+1)\) in the numerator of \(\binom {m}{n}\), one of the factors is \(m - m = 0\) (since \(m - n + 1 \leq 0 \leq m\) when \(m {\lt} n\) and \(m \in \mathbb {N}\)). Hence the entire product is \(0\), and so \(\binom {m}{n} = 0\).

Note that this really requires \(m\in \mathbb {N}\). For example, \(1.5{\lt}2\) but \(\binom {1.5}{2}=0.375\neq 0\).

Theorem 1.9 Symmetry of the binomial coefficients

Let \(n\in \mathbb {N}\) and \(k\in \mathbb {R}\). Then,

\[ \binom {n}{k}=\binom {n}{n-k}. \]
Proof

For \(k \notin \{ 0, 1, \ldots , n\} \), both sides are \(0\) (if \(k {\lt} 0\) or \(k {\gt} n\), then both \(\binom {n}{k} = 0\) and \(\binom {n}{n-k} = 0\) by Proposition 1.8 or by the definition). For \(k \in \{ 0, 1, \ldots , n\} \), we use the factorial formula (4):

\[ \binom {n}{k} = \frac{n!}{k!(n-k)!} = \frac{n!}{(n-k)!k!} = \binom {n}{n-k}. \]

Note the \(n\in \mathbb {N}\) requirement. Theorem 1.9 would fail for \(n=-1\) and \(k=0\), since \(\binom {-1}{0} = 1\) but \(\binom {-1}{-1} = 0\).

Lemma 1.10

For any \(a, b \in \mathbb {N}\), we have \(\binom {a+b}{a} = \binom {a+b}{b}\).

Proof

This follows from Theorem 1.9 since \((a+b) - a = b\).

Lemma 1.11

For any binomial ring \(R\), natural numbers \(n, k\) with \(k \leq n\), \(\binom {n}{k} = \binom {n}{n-k}\) where \(n\) is viewed as an element of \(R\).

Proof

This follows from the natural-number symmetry (Theorem 1.9) and the fact that the generalized binomial coefficient agrees with the natural-number binomial coefficient on natural numbers (Lemma 1.16).

Lemma 1.12

For any \(r\), we have \(\binom {r}{0} = 1\).

Proof

The empty product in the numerator of \(\binom {r}{0}\) equals \(1\), and \(0! = 1\).

Lemma 1.13

For any \(r\), we have \(\binom {r}{1} = r\).

Proof

We have \(\binom {r}{1} = \frac{r}{1!} = r\).

Lemma 1.14

For \(k {\gt} 0\), we have \(\binom {0}{k} = 0\).

Proof

The numerator of \(\binom {0}{k}\) contains the factor \(0\).

Lemma 1.15

For any element \(r\) in a binomial ring and \(n \in \mathbb {N}\), \(n! \cdot \binom {r}{n} = r(r-1)(r-2)\cdots (r-n+1)\).

Proof

This is the defining property of generalized binomial coefficients in a binomial ring, expressed using the descending Pochhammer symbol.

Lemma 1.16

For natural numbers \(n, k\), the generalized binomial coefficient \(\binom {n}{k}\) (computed in any binomial ring) agrees with the natural-number binomial coefficient \(\binom {n}{k}\) as computed from Definition 1.1.

Proof

This follows from the fact that the generalized binomial coefficient agrees with the natural-number binomial coefficient when \(n\) and \(k\) are natural numbers.

1.1.2 Helpers for Lemma 1.4

Lemma 1.17

For any \(n\in \mathbb {N}\), \(\prod _{i=0}^{n-1}(2i+1) = (2n-1)!!\). That is, the product of odd numbers \(1\cdot 3\cdot 5\cdots (2n-1)\) equals the double factorial \((2n-1)!!\).

Proof

By induction on \(n\), using the double factorial recurrence \((2m+3)!! = (2m+3)\cdot (2m+1)!!\).

Lemma 1.18

For any \(n\in \mathbb {N}\), \(n!\) divides \(\left(\prod _{i=0}^{n-1}(2i+1)\right)\cdot 2^n\).

Proof

Uses the factorization \((2n)! = 2^n \cdot n! \cdot (2n-1)!!\) together with the divisibility \(n!\cdot n! \mid (2n)!\).

1.1.3 The Fibonacci sequence (Example 1)

Definition 1.19
#

The Fibonacci sequence \((f_0, f_1, f_2, \ldots )\) is defined by \(f_0 = 0\), \(f_1 = 1\), and \(f_n = f_{n-1} + f_{n-2}\) for \(n \geq 2\).

Definition 1.20
#

The golden ratio \(\phi _+ = \frac{1+\sqrt{5}}{2}\).

Definition 1.21
#

The conjugate golden ratio \(\phi _- = \frac{1-\sqrt{5}}{2}\).

Theorem 1.22

The generating function of the Fibonacci sequence is

\[ F(x) = \sum _{n\geq 0} f_n x^n = \frac{x}{1-x-x^2}. \]
Proof

Let \(D = 1 - x - x^2\). We verify \(F \cdot D = x\) by checking that for each \(n\), \([x^n](F\cdot D) = f_n - f_{n-1} - f_{n-2} = 0\) for \(n \geq 2\), \([x^1](F\cdot D) = 1\), and \([x^0](F\cdot D) = 0\). Then \(F = x \cdot D^{-1}\) since the constant term of \(D\) is nonzero.

Theorem 1.23 Binet’s formula

For any \(n\in \mathbb {N}\),

\[ f_n = \frac{\phi _+^n - \phi _-^n}{\sqrt{5}}. \]
Proof

This follows from Binet’s formula as established in Mathlib.

1.1.4 Dyck words and Catalan numbers (Example 2)

Definition 1.24
#

A Dyck word of length \(2n\) is a list of \(0\)s and \(1\)s with equal numbers of each, such that every prefix has at least as many \(1\)s as \(0\)s.

Definition 1.25
#

The \(n\)-th Catalan number is \(c_n = \frac{1}{n+1}\binom {2n}{n}\).

Theorem 1.26

For \(n \geq 1\), the Catalan numbers satisfy the recurrence

\[ c_n = \sum _{k=0}^{n-1} c_k \, c_{n-1-k}. \]
Proof

Follows from Mathlib’s Catalan number recurrence, converting between Mathlib’s recursive definition and the explicit formula.

Lemma 1.27

The explicit formula for Catalan numbers: \(c_n = \frac{1}{n+1}\binom {2n}{n}\).

Proof

This is immediate from the definition of \(c_n\).

Lemma 1.28

For \(n \geq 1\), \(c_n = \binom {2n}{n} - \binom {2n}{n-1}\).

Proof

Uses the identity \(\binom {2n}{n-1}\cdot (n+1) = \binom {2n}{n}\cdot n\) (from the recurrence for binomial coefficients) and the divisibility \((n+1) \mid \binom {2n}{n}\).

Theorem 1.29

The generating function \(C(x) = \sum _{n\geq 0} c_n x^n\) satisfies the functional equation \(C(x) = 1 + x\, C(x)^2\).

Proof

Follows from Mathlib’s identity \(C(x)^2 \cdot x + 1 = C(x)\) for the Catalan generating function, after showing that \(C(x)\) equals the image of Mathlib’s Catalan series under the natural map.

Helpers for the Catalan generating function

Lemma 1.30

For \(n\in \mathbb {N}\), \((n+1)\binom {1/2}{n+1} = \left(\frac{1}{2}-n\right)\binom {1/2}{n}\).

Proof

Follows from the descending Pochhammer recurrence applied to \(\binom {1/2}{n}\).

Lemma 1.31

For \(n\in \mathbb {N}\), \(\binom {1/2}{n+1}\cdot (-4)^{n+1}\cdot (n+1) = -2\cdot \binom {2n}{n}\).

Proof

By induction on \(n\), using Lemma 1.30 and the central binomial coefficient recurrence \((n+1)\binom {2(n+1)}{n+1} = 2(2n+1)\binom {2n}{n}\).

Lemma 1.32

For \(n\in \mathbb {N}\), \(\binom {1/2}{n+1}\cdot (-4)^{n+1} = -2\, c_n\).

Proof

Follows from Lemma 1.31 by dividing both sides by \((n+1)\), using \((n+1)\mid \binom {2n}{n}\) and \(c_n = \binom {2n}{n}/(n+1)\).

Theorem 1.33

The generating function of the Catalan numbers satisfies

\[ 2x\, C(x) = 1 - \sqrt{1-4x}, \]

where \(\sqrt{1-4x} = \sum _{n\geq 0}\binom {1/2}{n}(-4)^n x^n\) is the binomial series.

Proof

We check coefficient by coefficient. For \(n=0\), both sides give \(0\). For \(n \geq 1\), the \(n\)-th coefficient of the left side is \(2c_{n-1}\), and the \(n\)-th coefficient of \(1 - \sqrt{1-4x}\) is \(-\binom {1/2}{n}(-4)^n\), which equals \(2c_{n-1}\) by Lemma 1.32.

1.1.5 The Vandermonde convolution (Example 3)

Theorem 1.34 Vandermonde convolution

For \(a, b, n \in \mathbb {N}\),

\[ \binom {a+b}{n} = \sum _{k=0}^{n}\binom {a}{k}\binom {b}{n-k}. \]
Proof

Follows from the Vandermonde convolution identity for natural-number binomial coefficients from Mathlib, with the antidiagonal sum rewritten as a range sum.

1.1.6 Solving a recurrence (Example 4)

Definition 1.35
#

The sequence \((a_n)\) defined by \(a_0 = 1\) and \(a_{n+1} = 2a_n + n\) for all \(n\geq 0\).

Theorem 1.36

For all \(n\in \mathbb {N}\), \(a_n = 2^{n+1} - (n+1)\).

Proof

By induction on \(n\). The base case \(a_0 = 1 = 2^1 - 1\) is immediate. For the induction step, \(a_{n+1} = 2a_n + n = 2(2^{n+1}-(n+1)) + n = 2^{n+2} - (n+2)\).

1.1.7 Auxiliary generating function results

Lemma 1.37

The geometric series identity: \(\frac{1}{1-x} = 1 + x + x^2 + x^3 + \cdots = \sum _{n\geq 0} x^n\).

Proof

We verify \((1-x)\cdot \sum _{n\geq 0}x^n = 1\) and invert, using that the constant term of \((1-x)\) is nonzero.

Lemma 1.38

For any \(\alpha \in \mathbb {Q}\), \(\frac{1}{1-\alpha x} = \sum _{n\geq 0}\alpha ^n x^n\).

Proof

We verify \((1-\alpha x)\cdot \sum _{n\geq 0}\alpha ^n x^n = 1\) by checking coefficients, then invert.

Lemma 1.39

The formal derivative of \(\frac{1}{1-x}\) is \(\frac{1}{(1-x)^2}\).

Proof

Follows from the derivative of an inverse formula in Mathlib.

Lemma 1.40

The power series identity \(\sum _{n\geq 0}(n+1)x^n = \frac{1}{(1-x)^2}\).

Proof

Uses the identity \(\sum _{n\geq 0}(n+1)x^n = \frac{1}{(1-x)^2}\) from Mathlib.

Lemma 1.41

The power series identity \(\sum _{n\geq 0}n\, x^n = \frac{x}{(1-x)^2}\).

Proof

For \(n=0\) both sides give \(0\); for \(n \geq 1\), \([x^n]\left(\frac{x}{(1-x)^2}\right) = [x^{n-1}]\frac{1}{(1-x)^2} = n\), using Lemma 1.40.