Formalization Blueprint for “An Introduction to Algebraic Combinatorics” by Darij Grinberg
1
Formal Power Series
▶
1.1
Notations and elementary facts
▶
1.1.1
Binomial coefficients
1.1.2
Helpers for Lemma
1.4
1.1.3
The Fibonacci sequence (Example 1)
1.1.4
Dyck words and Catalan numbers (Example 2)
1.1.5
The Vandermonde convolution (Example 3)
1.1.6
Solving a recurrence (Example 4)
1.1.7
Auxiliary generating function results
1.2
Commutative rings and modules
▶
1.2.1
Reminder: Commutative rings
1.2.2
Standard rules in commutative rings
1.2.3
Finite sums and products
1.2.4
\(K\)-modules
1.2.5
Additive inverses in modules
1.2.6
Inverses in commutative rings
1.2.7
Fractions and integer powers
1.3
Formal power series: definition and basic properties
▶
1.3.1
Convention
1.3.2
The definition of formal power series
1.3.3
Essentially finite sums and summable families
1.3.4
The indeterminate \(x\) and powers
1.3.5
Helper lemmas from the formalization
1.3.6
Generating functions
1.3.7
The Chu–Vandermonde identity
1.4
Dividing FPSs
▶
1.4.1
Inverses in commutative rings
1.4.2
Inverses in \(K[[x]]\)
1.4.3
Coefficient formulas for inverses
1.4.4
Newton’s binomial formula
1.4.5
Dividing by \(x\)
1.4.6
A few lemmas
1.5
Polynomials
▶
1.5.1
Definition
1.5.2
Polynomials form a subring of power series
1.5.3
Reminders on rings and \(K\)-algebras
1.5.4
Evaluation aka substitution into polynomials
1.5.5
Special evaluation results
1.6
Substitution and evaluation of power series
▶
1.6.1
Defining substitution
1.6.2
Well-definedness of substitution
1.6.3
Lemma for first \(k\) coefficients
1.6.4
Kronecker delta notation
1.6.5
Laws of substitution
1.6.6
Example: Fibonacci generating function
1.7
Derivatives of FPSs
▶
1.7.1
Derivative rules
1.8
Exponentials and logarithms
▶
1.8.1
Definitions
1.8.2
Helpers for derivative computations
1.8.3
The exponential and the logarithm are inverse
1.8.4
Helpers for Theorem
1.221
1.8.5
The exponential and the logarithm of an FPS
1.8.6
Helpers for the group structure
1.8.7
Addition to multiplication
1.8.8
Helpers for the logarithmic derivative
1.8.9
The logarithmic derivative
1.8.10
Summable and multipliable families
1.8.11
Exp and Log for infinite products and sums
1.9
Non-integer powers
▶
1.9.1
Definition
1.9.2
Rules of exponents
1.9.3
The Newton binomial formula for arbitrary exponents
1.9.4
Further rules of exponents
1.9.5
Another application
1.9.6
Helper lemmas from the formalization
1.9.7
Helpers for Theorem
1.264
1.9.8
Helpers for Proposition
1.271
1.10
Integer compositions
▶
1.10.1
Compositions
1.10.2
Helpers for Theorem
1.304
1.10.3
Weak compositions
1.10.4
Weak compositions with entries from \(\left\{ 0,1,\ldots ,p-1\right\} \)
1.11
\(x^{n}\)-equivalence
▶
1.11.1
Helpers for the equivalence relation
1.11.2
Helpers for inversion and division
1.11.3
Divisibility characterization
1.11.4
Composition
1.11.5
Equality via \(x^n\)-equivalence
1.12
Infinite products of FPSs
▶
1.12.1
Determining coefficients in products
1.12.2
Multipliable families and infinite products
1.12.3
Irrelevance lemmas
1.12.4
Multipliability criterion
1.12.5
Further multipliability results
1.12.6
Binary product example
1.12.7
\(x^n\)-approximators
1.12.8
Properties of infinite products
1.12.9
Subfamilies of multipliable families
1.12.10
Reindexing
1.12.11
Breaking products into subproducts
1.12.12
Fubini rule for infinite products
1.13
Product rules (generalized distributive laws)
▶
Helpers for the finite product rule
1.13.1
Helper lemmas for the infinite product rule
1.13.2
Helper lemmas from the Lean formalization
1.13.3
Binary product rule
1.13.4
Another example
1.13.5
Infinite products and substitution
1.13.6
Exponentials, logarithms and infinite products
1.14
The generating function of a weighted set
▶
1.14.1
The theory
1.14.2
Domino tilings
1.15
Limits of FPSs
▶
1.15.1
Stabilization of scalars
1.15.2
Coefficientwise stabilization of FPSs
1.15.3
Some properties of limits
1.15.4
Infinite sums and products
1.16
Laurent power series
▶
1.16.1
Motivation
1.16.2
The space \(K\left[\left[x^{\pm }\right]\right]\)
1.16.3
Laurent polynomials
1.16.4
Laurent series
1.16.5
Embeddings
1.16.6
The partial product formula
1.16.7
Laurent polynomial action and torsion
1.16.8
Equivalence of balanced ternary formulations
1.17
Multivariate formal power series
▶
1.17.1
Embedding univariate power series into bivariate power series
1.17.2
Comparing coefficients of \(y^k\)
1.17.3
Application: binomial generating function identity
1.17.4
Helper lemmas from the formalization
1.17.5
Partial derivatives
2
Integer Partitions
▶
2.1
Partition basics
▶
2.1.1
Definitions
2.1.2
Simple properties of partition numbers
2.1.3
The generating function
2.1.4
Odd parts and distinct parts
2.1.5
Partitions with a given largest part
2.1.6
Counting partitions by parts and largest part
2.1.7
Partition number vs. sums of divisors
2.2
Euler’s pentagonal number theorem and Jacobi’s triple product identity
▶
2.2.1
Euler’s pentagonal number theorem
2.2.2
Jacobi’s triple product identity
2.3
\(q\)-Binomial Coefficients
▶
2.3.1
Motivation
2.3.2
Definition
2.3.3
Basic properties
2.3.4
Recurrence relations
2.3.5
Product and quotient formulas
2.3.6
\(q\)-integers and \(q\)-factorials
2.3.7
Symmetry
2.4
\(q\)-Binomial formulas
▶
2.4.1
Combinatorial definition of \(q\)-binomial coefficients
2.4.2
Alternative characterizations from the recurrence
2.4.3
Product expansion rule
2.4.4
First \(q\)-binomial theorem
2.4.5
Second \(q\)-binomial theorem
2.4.6
Counting subspaces of vector spaces
2.4.7
Limits of \(q\)-binomial coefficients
3
Permutations
▶
3.1
Permutations: basic definitions
▶
3.1.1
Basic definitions
3.1.2
Transpositions, cycles and involutions
3.1.3
Further properties of involutions
3.2
Inversions, length and Lehmer codes
▶
3.2.1
Inversions and lengths
3.2.2
Helpers for Proposition
3.37
3.2.3
Lehmer codes
3.2.4
Lexicographic order
3.2.5
Generating function for lengths
3.3
More about lengths and simples
▶
3.3.1
Helpers for Proposition
3.59
3.3.2
Rothe diagram and Lehmer entry properties
3.3.3
The Lehmer code representation
3.3.4
Helpers for Proposition
3.107
3.4
Signs of permutations
▶
3.4.1
Definition and basic properties
3.4.2
The sign homomorphism
3.4.3
Even and odd permutations
3.4.4
The alternating group
3.4.5
Counting even and odd permutations
3.4.6
Sign for permutations of arbitrary finite sets
3.5
The cycle decomposition
▶
3.5.1
Properties of the cycle decomposition
3.5.2
Auxiliary lemmas on cycles
3.5.3
Sign from cycle decomposition
3.5.4
Canonical DCD construction helpers
4
Signed Counting
▶
4.1
Cancellations in alternating sums
▶
4.1.1
Acceptable sets, partners, and signs
4.1.2
Cancellation principles
4.1.3
Switching operations and the \(q\)-binomial at \(q = -1\)
4.1.4
Roots of unity
4.1.5
The \(q\)-Lucas theorem
4.1.6
The \(q\)-binomial at \(q = -1\)
4.2
The principles of inclusion and exclusion
▶
4.2.1
The size version
4.2.2
Alternative formulations of the size version
4.2.3
Counting surjections
4.2.4
Consequences of the surjection formula
4.2.5
Helpers for the divisibility proof
4.2.6
Derangements
4.2.7
Euler’s totient formula
4.2.8
The weighted version
4.3
Boolean Möbius inversion
▶
4.3.1
Alternating sums over supersets
4.3.2
The Boolean Möbius inversion formula
4.4
More subtractive methods
▶
4.4.1
Sums with varying signs
4.4.2
Lemmas for the proof
4.4.3
Involution argument for part (a)
4.4.4
Computing the left-hand side
4.4.5
Helper lemmas for toSign
4.4.6
Corollaries of the counting formula
5
Determinants
▼
5.1
Determinants: Basic Properties
▶
5.1.1
Conventions
5.1.2
Definition
5.1.3
Small determinants and basic API
5.1.4
Helpers for Proposition
5.17
5.1.5
Basic properties
5.1.6
Permutation images and submatrix determinants
5.2
Cauchy–Binet and related formulas
▶
5.2.1
Submatrices and minors
5.2.2
The Cauchy–Binet formula
5.2.3
The formula for \(\det (A+B)\)
5.2.4
Minors of diagonal matrices
5.2.5
Determinant of \(A+D\)
5.2.6
Determinant of \(x + D\)
5.2.7
Characteristic polynomial coefficients
5.2.8
The Pascal matrix
5.3
Determinants: Factor Hunting, Laplace Expansion, and Desnanot–Jacobi
▶
5.3.1
Factor hunting and the Vandermonde determinant
5.3.2
Laplace expansion
5.3.3
Laplace expansion along multiple rows
5.3.4
Desnanot–Jacobi and Dodgson condensation
5.3.5
Generalized Desnanot–Jacobi
5.3.6
Jacobi’s complementary minor theorem
5.3.7
Helpers for the Vandermonde determinant proof
5.3.8
Helpers for the Desnanot–Jacobi proof
5.3.9
Helpers for the generalized Desnanot–Jacobi proof
5.3.10
Helpers for the adjugate and inverse relationship
5.3.11
Helpers for block matrix decomposition
5.3.12
Helpers for the complementary minor theorem proof
5.3.13
Helpers for the Cauchy determinant proof (factor hunting)
5.4
The Lindström–Gessel–Viennot lemma
▶
5.4.1
Definitions
5.4.2
Helpers for lattice path infrastructure
5.4.3
Counting paths from \((a,b)\) to \((c,d)\)
5.4.4
Path tuples, nipats and ipats
5.4.5
Helpers for path tuple finiteness
5.4.6
Crowded vertices and the minimum crowded path index
5.4.7
The LGV lemma for two paths
5.4.8
The baby Jordan curve theorem
5.4.9
Log-concavity of binomial coefficients
5.4.10
The LGV lemma for \(k\) paths
5.5
The LGV lemma: weighted and generalized versions
▶
5.5.1
The weighted version
5.5.2
Generalization to acyclic digraphs
5.5.3
Helper lemmas for the sign-reversing involution
5.5.4
Infrastructure for the LGV proof
5.5.5
The nonpermutable case
5.5.6
Applications
5.5.7
Bridge between path representations
6
Symmetric Functions
▶
6.1
Definitions and examples of symmetric polynomials
▶
6.1.1
Setup
6.1.2
The polynomial ring and the symmetric group action
6.1.3
The action is well-defined
6.1.4
The action is by algebra automorphisms
6.1.5
Symmetric polynomials form a subalgebra
6.1.6
Monomials
6.1.7
Elementary, complete homogeneous, and power sum symmetric polynomials
6.1.8
Elementary symmetric polynomials vanish for large degree
6.1.9
Generating function identities
6.1.10
Newton–Girard formulas
6.1.11
Fundamental Theorem of Symmetric Polynomials
6.1.12
Simple transpositions suffice
6.1.13
Helper lemmas from the Lean formalization
6.1.14
Monomial API
6.1.15
Basic values of \(e_n\), \(h_n\), \(p_n\)
6.1.16
Alternative characterizations of \(e_n\), \(h_n\), \(p_n\)
6.1.17
Integer-indexed versions
6.1.18
Adding a variable recurrence
6.1.19
Antisymmetric polynomials
6.1.20
The sum of variables is symmetric
6.2
\(N\)-partitions and monomial symmetric polynomials
▶
6.2.1
\(N\)-partitions
6.2.2
Monomials and sorting
6.2.3
Monomial symmetric polynomials
6.2.4
Elementary, homogeneous, and power sum via monomial symmetric polynomials
6.2.5
Permutation action on polynomial coefficients
6.2.6
Basis theorem
6.3
Schur polynomials
▶
6.3.1
Alternants
6.3.2
Young diagrams and Schur polynomials
6.3.3
Examples of Schur polynomials
6.3.4
Symmetry of Schur polynomials
6.3.5
Skew Young diagrams and skew Schur polynomials
6.3.6
Filling infrastructure for Schur polynomials
6.3.7
Bender–Knuth involutions (helper lemmas)
6.3.8
Equivalences between Schur polynomial definitions
6.4
The Littlewood–Richardson rule
▶
6.4.1
Tuple arithmetic
6.4.2
Content of a tableau
6.4.3
Column restriction of tableaux
6.4.4
Yamanouchi tableaux
6.4.5
Content and column restriction helpers
6.4.6
Properties of alternants
6.4.7
Regular elements and cancellation
6.4.8
Bender–Knuth involution
6.4.9
Symmetry of skew Schur polynomials
6.4.10
Stembridge’s involution infrastructure
6.4.11
Stembridge’s involution and sign-reversing property
6.4.12
Stembridge’s Lemma
6.4.13
Consequences of Stembridge’s Lemma
6.4.14
The Littlewood–Richardson rule
6.5
The Pieri Rules and Jacobi–Trudi Identities
▶
6.5.1
Strips and skew partitions
6.5.2
Schur and skew Schur polynomials
6.5.3
Symmetric polynomials as Schur polynomials
6.5.4
The Pieri rules
6.5.5
The Jacobi–Trudi identities
6.5.6
Special cases
6.5.7
Symmetry of Schur polynomials via Jacobi–Trudi
6.5.8
The \(\omega \)-involution
A
Details
▶
A.1
Details: Infinite products (part 1)
▶
A.1.1
Essentially finite families
A.1.2
Existence of approximators
A.1.3
Multipliability criteria
A.1.4
Multipliable product and division rules (Lean formalization)
A.1.5
Subfamily and reindexing lemmas
A.1.6
Fiber product decomposition
A.1.7
Fubini rules for infinite products
A.1.8
Coefficient form of the generalized distributive law
A.1.9
Congruence lemma for division
A.1.10
Detailed proof of Proposition
1.367
A.1.11
Approximator intersection lemma
A.1.12
Detailed proof of Proposition
1.369
A.1.13
Finite products and \(x^n\)-equivalence
A.1.14
Detailed proof of Proposition
1.372
A.1.15
Detailed proof of Proposition
1.366
A.1.16
Product rule claims
A.1.17
Composition rules for infinite products
A.1.18
Additional supporting lemmas
A.2
Details: Infinite products (part 2) – Finite product composition rule
▶
A.2.1
Detailed proof of Proposition
1.399
A.3
Domino tilings of height-3 rectangles
▶
A.3.1
The tilings \(A_n\), \(B_n\), and \(C\)
A.3.2
Properties of \(A_n\), \(B_n\), and \(C\)
A.3.3
Faultfreeness of \(A_n\), \(B_n\), and \(C\)
A.3.4
Reflection lemmas
A.3.5
Auxiliary lemmas for the classification
A.3.6
The classification
A.3.7
Structural helpers for the classification
A.3.8
Height-\(2\) Fibonacci recurrence
A.3.9
Bridge between \(\mathbb {N}\)-based and \(\mathbb {Z}\)-based domino tilings
A.4
Details: Limits of FPSs
▶
A.4.1
Detailed proof of Lemma
1.462
A.4.2
Detailed proof of Proposition
1.463
A.4.3
Helpers for Proposition
1.468
A.4.4
Detailed proof of Proposition
1.468
A.4.5
Detailed proof of Theorem
1.475
A.4.6
Helpers for Theorem
1.476
A.4.7
Detailed proof of Theorem
1.476
A.4.8
Detailed proofs of Corollary
1.477
A.4.9
Detailed proof of Theorem
1.478
A.4.10
Helpers for Theorem
1.479
A.4.11
Detailed proof of Theorem
1.479
A.4.12
Helper lemmas from the Lean formalization
A.5
Details on Laurent power series
▶
A.5.1
Proof of Theorem
1.498
(sketched)
A.5.2
Helpers for Theorem
1.498
A.5.3
Multiplication by \(x\) shifts coefficients
A.5.4
Powers of \(x\)
A.5.5
Proof of Proposition
1.505
(sketched)
A.5.6
Proof of Theorem
1.509
(sketched)
A.5.7
Helpers for the embeddings
A.5.8
Helpers for Theorem
1.483
Dependency graph
5 Determinants
5.1
Determinants: Basic Properties
5.1.1
Conventions
5.1.2
Definition
5.1.3
Small determinants and basic API
5.1.4
Helpers for Proposition
5.17
5.1.5
Basic properties
5.1.6
Permutation images and submatrix determinants
5.2
Cauchy–Binet and related formulas
5.2.1
Submatrices and minors
5.2.2
The Cauchy–Binet formula
Helpers for the Cauchy–Binet formula
5.2.3
The formula for \(\det (A+B)\)
Basic definitions
Expansion steps
Permutation decomposition infrastructure
Sign decomposition infrastructure
5.2.4
Minors of diagonal matrices
5.2.5
Determinant of \(A+D\)
5.2.6
Determinant of \(x + D\)
5.2.7
Characteristic polynomial coefficients
5.2.8
The Pascal matrix
5.3
Determinants: Factor Hunting, Laplace Expansion, and Desnanot–Jacobi
5.3.1
Factor hunting and the Vandermonde determinant
5.3.2
Laplace expansion
5.3.3
Laplace expansion along multiple rows
5.3.4
Desnanot–Jacobi and Dodgson condensation
5.3.5
Generalized Desnanot–Jacobi
5.3.6
Jacobi’s complementary minor theorem
5.3.7
Helpers for the Vandermonde determinant proof
5.3.8
Helpers for the Desnanot–Jacobi proof
5.3.9
Helpers for the generalized Desnanot–Jacobi proof
5.3.10
Helpers for the adjugate and inverse relationship
5.3.11
Helpers for block matrix decomposition
5.3.12
Helpers for the complementary minor theorem proof
5.3.13
Helpers for the Cauchy determinant proof (factor hunting)
5.4
The Lindström–Gessel–Viennot lemma
5.4.1
Definitions
5.4.2
Helpers for lattice path infrastructure
5.4.3
Counting paths from \((a,b)\) to \((c,d)\)
5.4.4
Path tuples, nipats and ipats
5.4.5
Helpers for path tuple finiteness
5.4.6
Crowded vertices and the minimum crowded path index
5.4.7
The LGV lemma for two paths
Signed path tuple infrastructure
First intersection point
5.4.8
The baby Jordan curve theorem
5.4.9
Log-concavity of binomial coefficients
5.4.10
The LGV lemma for \(k\) paths
Definitions for general \(k\)
Bridge between LGV1 and LGV2
Product rule and partition lemmas
5.5
The LGV lemma: weighted and generalized versions
5.5.1
The weighted version
5.5.2
Generalization to acyclic digraphs
5.5.3
Helper lemmas for the sign-reversing involution
5.5.4
Infrastructure for the LGV proof
5.5.5
The nonpermutable case
5.5.6
Applications
Nonnegativity of binomial coefficient determinants
Helpers for Corollary
5.181
Catalan Hankel determinant
Helpers for the Dyck path–DyckWord bijection
Helpers for the unique nipat (Catalan case)
5.5.7
Bridge between path representations