The Principles of Inclusion and Exclusion

This file formalizes the inclusion-exclusion principles and their applications from Section sec.sign.pie of the Algebraic Combinatorics notes.

Main results

Size version (Theorem thm.pie.1)

The size version of PIE states that for a finite set U and subsets A₁, ..., Aₙ: |{u ∈ U : u ∉ Aᵢ for all i}| = ∑_{I ⊆ [n]} (-1)^|I| |{u ∈ U : u ∈ Aᵢ for all i ∈ I}|

This is already available in Mathlib as Finset.inclusion_exclusion_card_inf_compl.

Applications

• numSurj - The number of surjective maps from [m] to [n] (Theorem thm.pie.count-sur)
• numSurj_formula - The formula: ∑_{k=0}^{n} (-1)^k * C(n,k) * (n-k)^m
• Corollaries about the surjection count (cor.pie.count-sur.cors)
• Derangement - Permutations with no fixed points (Definition def.pie.dera)
• numDerangements_formula - The derangement count formula (Theorem thm.pie.count-der)
• totient_eq_prod_one_sub_inv - Euler's totient formula (Theorem thm.pie.euler-tot)

Weighted version (Theorem thm.pie.2)

The weighted version generalizes the size version by replacing cardinalities with weighted sums. This is already available in Mathlib as Finset.inclusion_exclusion_sum_inf_compl.

References

• Section sec.sign.pie of the Algebraic Combinatorics notes
• Mathlib's Mathlib.Combinatorics.Enumerative.InclusionExclusion

Size version of PIE (Theorem thm.pie.1)

The size version is already in Mathlib. We restate it here for reference. See Finset.inclusion_exclusion_card_inf_compl.

For a finite set U and subsets A₁, ..., Aₙ: |U \ (A₁ ∪ ... ∪ Aₙ)| = ∑{I ⊆ [n]} (-1)^|I| |⋂{i ∈ I} Aᵢ|

where the empty intersection is taken to be U.

theorem AlgebraicCombinatorics.InclusionExclusion.pie_size_version {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype α] (s : Finset ι) (A : ι → Finset α) : ↑(s.inf fun (i : ι) => (A i)ᶜ).card = ∑ I ∈ s.powerset, (-1) ^ I.card * ↑(I.inf A).card

Theorem thm.pie.1 (Size version of PIE): For a finite set U and subsets A₁, ..., Aₙ, the number of elements in U that belong to none of the Aᵢ equals the alternating sum over all subsets I ⊆ [n] of the cardinalities of the intersections ⋂_{i ∈ I} Aᵢ.

More precisely: |U ∩ A₁ᶜ ∩ A₂ᶜ ∩ ... ∩ Aₙᶜ| = ∑{I ⊆ [n]} (-1)^|I| |⋂{i ∈ I} Aᵢ|

where the empty intersection is taken to be U.

This is Finset.inclusion_exclusion_card_inf_compl from Mathlib.

theorem AlgebraicCombinatorics.InclusionExclusion.pie_size_version' {α : Type u_1} {ι : Type u_2} [DecidableEq α] [Fintype α] (s : Finset ι) (A : ι → Finset α) : ↑(s.biUnion A)ᶜ.card = ∑ I ∈ s.powerset, (-1) ^ I.card * ↑(I.inf A).card

Alternative form of thm.pie.1 using the complement of a union.

This states: |U \ (A₁ ∪ A₂ ∪ ... ∪ Aₙ)| = ∑{I ⊆ [n]} (-1)^|I| |⋂{i ∈ I} Aᵢ|

This is the more common textbook formulation.

theorem AlgebraicCombinatorics.InclusionExclusion.pie_size_version_fin {α : Type u_1} [DecidableEq α] [Fintype α] (n : ℕ) (A : Fin n → Finset α) : ↑(Finset.univ.inf fun (i : Fin n) => (A i)ᶜ).card = ∑ I ∈ Finset.univ.powerset, (-1) ^ I.card * ↑(I.inf A).card

Theorem thm.pie.1 specialized to n subsets indexed by Fin n.

For a finite type α (the "universe" U) and n subsets A₀, A₁, ..., Aₙ₋₁ of α: |{u ∈ α : u ∉ Aᵢ for all i ∈ Fin n}| = ∑{I ⊆ Fin n} (-1)^|I| |⋂{i ∈ I} Aᵢ|

This matches the textbook formulation where [n] = {1, 2, ..., n} is replaced by Fin n.

theorem AlgebraicCombinatorics.InclusionExclusion.pie_rule_breaking {α : Type u_1} [DecidableEq α] [Fintype α] (n : ℕ) (satisfiesRule : Fin n → Finset α) : ↑{u : α | ∀ (i : Fin n), u ∉ satisfiesRule i}.card = ∑ I ∈ Finset.univ.powerset, (-1) ^ I.card * ↑{u : α | ∀ i ∈ I, u ∈ satisfiesRule i}.card

The "rule-breaking" interpretation of PIE: Count elements that violate all rules.

Given n "rules" (encoded as subsets A₀, ..., Aₙ₋₁ where Aᵢ is the set of elements satisfying rule i), the number of elements violating all rules equals the alternating sum over all subsets I of the number of elements satisfying all rules in I.

Example 1: Counting surjective maps (Theorem thm.pie.count-sur)

The number of surjective maps from Fin m to Fin n is ∑_{k=0}^{n} (-1)^k * C(n,k) * (n-k)^m

def AlgebraicCombinatorics.InclusionExclusion.numSurj (m n : ℕ) : ℕ

The number of surjective maps from Fin m to Fin n.

Equations

• AlgebraicCombinatorics.InclusionExclusion.numSurj m n = Fintype.card { f : Fin m → Fin n // Function.Surjective f }

Helper lemmas for the surjection formula

theorem AlgebraicCombinatorics.InclusionExclusion.card_functions_avoiding_set (m n : ℕ) (I : Finset (Fin n)) : Fintype.card { f : Fin m → Fin n // ∀ i ∈ I, i ∉ Set.range f } = (n - I.card) ^ m

Count functions from Fin m to Fin n whose range avoids a given set I.

theorem AlgebraicCombinatorics.InclusionExclusion.card_inf_S_avoid (m n : ℕ) (t : Finset (Fin n)) : (t.inf (AlgebraicCombinatorics.InclusionExclusion.S_avoid✝ m n)).card = (n - t.card) ^ m

The cardinality of the intersection of S_avoid sets.

theorem AlgebraicCombinatorics.InclusionExclusion.numSurj_formula (m n : ℕ) : ↑(numSurj m n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * (↑n - ↑k) ^ m

Theorem thm.pie.count-sur: The number of surjective maps from Fin m to Fin n equals ∑_{k=0}^{n} (-1)^k * C(n,k) * (n-k)^m.

This is the main formula for counting surjections using inclusion-exclusion.

Corollary cor.pie.count-sur.cors: Consequences of the surjection formula

theorem AlgebraicCombinatorics.InclusionExclusion.surjOn_alternating_sum_eq_zero (n m : ℕ) (h : m < n) : ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * (↑n - ↑k) ^ m = 0

Corollary cor.pie.count-sur.cors (a): When m < n, there are no surjections, so the alternating sum equals 0.

theorem AlgebraicCombinatorics.InclusionExclusion.surjOn_alternating_sum_eq_factorial (n : ℕ) : ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * (↑n - ↑k) ^ n = ↑n.factorial

Corollary cor.pie.count-sur.cors (b): When m = n, the number of surjections equals n! (the surjections are precisely the permutations).

theorem AlgebraicCombinatorics.InclusionExclusion.surjOn_alternating_sum_nonneg (m n : ℕ) : 0 ≤ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * (↑n - ↑k) ^ m

Corollary cor.pie.count-sur.cors (c): The alternating sum is always nonnegative since it counts surjections.

Helper lemmas for the divisibility proof

The proof uses the orbit-stabilizer theorem. The symmetric group Perm (Fin n) acts on surjective maps Fin m → Fin n by post-composition. Since this action is free (the stabilizer of any surjective map is trivial), the number of surjections is divisible by n!.

instance AlgebraicCombinatorics.InclusionExclusion.permActionOnFun (m n : ℕ) : MulAction (Equiv.Perm (Fin n)) (Fin m → Fin n)

Action of Perm (Fin n) on functions Fin m → Fin n by post-composition.

Equations

• AlgebraicCombinatorics.InclusionExclusion.permActionOnFun m n = { smul := fun (σ : Equiv.Perm (Fin n)) (f : Fin m → Fin n) => ⇑σ ∘ f, mul_smul := ⋯, one_smul := ⋯ }

theorem AlgebraicCombinatorics.InclusionExclusion.surjective_smul {m n : ℕ} (σ : Equiv.Perm (Fin n)) {f : Fin m → Fin n} (hf : Function.Surjective f) : Function.Surjective (σ • f)

Post-composition with a permutation preserves surjectivity.

instance AlgebraicCombinatorics.InclusionExclusion.permActionOnSurj (m n : ℕ) : MulAction (Equiv.Perm (Fin n)) { f : Fin m → Fin n // Function.Surjective f }

Action of Perm (Fin n) on surjective functions Fin m → Fin n by post-composition.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.InclusionExclusion.stabilizer_surj_eq_bot {m n : ℕ} (f : { f : Fin m → Fin n // Function.Surjective f }) : MulAction.stabilizer (Equiv.Perm (Fin n)) f = ⊥

The action of Perm (Fin n) on surjective maps is free: the stabilizer of any surjective map is trivial. This is because if σ ∘ f = f and f is surjective, then σ = id.

theorem AlgebraicCombinatorics.InclusionExclusion.factorial_dvd_numSurj (m n : ℕ) : n.factorial ∣ numSurj m n

n! divides numSurj m n because the action of Perm (Fin n) on surjective maps is free, so each orbit has size n!.

theorem AlgebraicCombinatorics.InclusionExclusion.surjOn_alternating_sum_dvd_factorial (m n : ℕ) : ↑n.factorial ∣ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * (↑n - ↑k) ^ m

Corollary cor.pie.count-sur.cors (d): The alternating sum is divisible by n!. This follows from the orbit-stabilizer theorem applied to the action of Sₙ on surjections.

Example 2: Derangements (Definition def.pie.dera and Theorem thm.pie.count-der)

A derangement is a permutation with no fixed points.

Relationship to Mathlib:

• Mathlib defines derangements α : Set (Perm α) in Mathlib.Combinatorics.Derangements.Basic
• Mathlib defines numDerangements : ℕ → ℕ in Mathlib.Combinatorics.Derangements.Finite
• Our Derangement α is definitionally equal to ↥(derangements α) (the subtype)
• Fintype.card (Derangement (Fin n)) equals numDerangements n (see card_Derangement_eq)

We provide the explicit Derangement type to make the connection to the textbook explicit. The main theorems use Mathlib's numDerangements directly.

def AlgebraicCombinatorics.InclusionExclusion.Derangement (α : Type u_1) : Type u_1

Definition def.pie.dera: A derangement of a type α is a permutation with no fixed points.

This is definitionally equal to ↥(derangements α) from Mathlib.Combinatorics.Derangements.Basic.

Textbook definition: "A derangement of a set X means a permutation of X that has no fixed points."

Examples from the textbook:

• D₀ = 1: The identity on ∅ is a derangement (vacuously no fixed points)
• D₁ = 0: The identity on {0} fixes 0, so it's not a derangement
• D₂ = 1: Only the swap (0 1) is a derangement
• D₃ = 2: The two 3-cycles (0 1 2) and (0 2 1) are derangements

Equations

• AlgebraicCombinatorics.InclusionExclusion.Derangement α = { σ : Equiv.Perm α // ∀ (x : α), σ x ≠ x }

instance AlgebraicCombinatorics.InclusionExclusion.instFintypeDerangementOfDecidableEq {α : Type u_1} [DecidableEq α] [Fintype α] : Fintype (Derangement α)

Equations

• AlgebraicCombinatorics.InclusionExclusion.instFintypeDerangementOfDecidableEq = Subtype.fintype fun (σ : Equiv.Perm α) => ∀ (x : α), σ x ≠ x

theorem AlgebraicCombinatorics.InclusionExclusion.Derangement.mem_derangements {α : Type u_1} (σ : Derangement α) : ↑σ ∈ derangements α

A derangement is a permutation in derangements α. This shows our definition matches Mathlib's derangements set.

def AlgebraicCombinatorics.InclusionExclusion.Derangement.equivDerangements (α : Type u_1) : Derangement α ≃ ↑(derangements α)

The Derangement type is equivalent to the subtype of derangements α. This establishes that our explicit type is equivalent to Mathlib's set-based definition.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.InclusionExclusion.Derangement.id_of_isEmpty {α : Type u_1} [IsEmpty α] : ∃ (d : Derangement α), ↑d = 1

The identity is a derangement of the empty type. This matches the textbook example: D₀ = 1, since the identity has no fixed points when there are no elements.

theorem AlgebraicCombinatorics.InclusionExclusion.Derangement.id_not_derangement {α : Type u_1} [Nonempty α] (d : Derangement α) : ↑d ≠ 1

The identity is NOT a derangement when the type is nonempty. This matches the textbook example: D₁ = 0, since id(1) = 1 is a fixed point.

theorem AlgebraicCombinatorics.InclusionExclusion.card_Derangement_eq (n : ℕ) : Fintype.card (Derangement (Fin n)) = numDerangements n

The cardinality of Derangement (Fin n) equals Mathlib's numDerangements n.

theorem AlgebraicCombinatorics.InclusionExclusion.numDerangements_two' : numDerangements 2 = 1

D₂ = 1: The only derangement of {0, 1} is the swap. (Mathlib already provides numDerangements_zero and numDerangements_one as @[simp] lemmas.)

theorem AlgebraicCombinatorics.InclusionExclusion.numDerangements_three : numDerangements 3 = 2

D₃ = 2: There are exactly 2 derangements of {0, 1, 2} (the two 3-cycles). This matches the textbook: "the derangements are the 3-cycles cyc_{1,2,3} and cyc_{1,3,2}".

theorem AlgebraicCombinatorics.InclusionExclusion.numDerangements_four : numDerangements 4 = 9

D₄ = 9: There are exactly 9 derangements of {0, 1, 2, 3}. From the textbook table of early values.

theorem AlgebraicCombinatorics.InclusionExclusion.numDerangements_five : numDerangements 5 = 44

D₅ = 44: There are exactly 44 derangements of {0, 1, 2, 3, 4}. From the textbook table of early values.

theorem AlgebraicCombinatorics.InclusionExclusion.numDerangements_formula (n : ℕ) : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑(n.choose k) * ↑(n - k).factorial

Theorem thm.pie.count-der: The number of derangements of Fin n is Dₙ = ∑_{k=0}^{n} (-1)^k * C(n,k) * (n-k)! = n! * ∑_{k=0}^{n} (-1)^k / k!

This is derived from PIE by considering permutations that violate all "fixed point" rules.

Note: Mathlib's numDerangements_sum gives a related formula using ascending factorials.

theorem AlgebraicCombinatorics.InclusionExclusion.numDerangements_formula_rat (n : ℕ) : ↑(numDerangements n) = ↑n.factorial * ∑ k ∈ Finset.range (n + 1), (-1) ^ k / ↑k.factorial

Alternative form of the derangement formula: Dₙ = n! * ∑_{k=0}^{n} (-1)^k / k!

Example 3: Euler's totient function (Theorem thm.pie.euler-tot)

Euler's totient φ(c) counts integers in [1, c] coprime to c. The formula expresses this in terms of the prime factorization.

Note: Nat.totient is already defined in Mathlib.

theorem AlgebraicCombinatorics.InclusionExclusion.totient_eq_prod_one_sub_inv (c : ℕ) (_hc : 0 < c) : ↑c.totient = ↑c * ∏ p ∈ c.primeFactors, (1 - 1 / ↑p)

Theorem thm.pie.euler-tot: Euler's totient formula. For a positive integer c with prime factorization p₁^{a₁} * ... * pₙ^{aₙ}: φ(c) = c * ∏{i=1}^{n} (1 - 1/pᵢ) = ∏{i=1}^{n} (pᵢ^{aᵢ} - pᵢ^{aᵢ-1})

This is proved using PIE where rule i is "be divisible by pᵢ".

Note: This is essentially Nat.totient_eq_prod_factorization in Mathlib.

Example 4: Partitions into distinct vs odd parts

This example shows that p_dist(n) = p_odd(n) using PIE. This is already covered in other chapters on partitions.

Weighted version of PIE (Theorem thm.pie.2)

The weighted version of the Principle of Inclusion and Exclusion generalizes the size version by replacing cardinalities with weighted sums.

For a finite set U, subsets A₁, ..., Aₙ, an additive abelian group A, and a weight function w : U → A:

∑{u ∈ U : u ∉ Aᵢ for all i ∈ [n]} w(u) = ∑{I ⊆ [n]} (-1)^|I| ∑_{u ∈ U : u ∈ Aᵢ for all i ∈ I} w(u)

This is proved in Mathlib as Finset.inclusion_exclusion_sum_inf_compl. Theorem thm.pie.1 is obtained by setting w(u) = 1 for all u.

theorem AlgebraicCombinatorics.InclusionExclusion.weighted_pie {ι : Type u_1} {U : Type u_2} {G : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype U] [DecidableEq U] [AddCommGroup G] (A : ι → Finset U) (w : U → G) : ∑ u ∈ Finset.univ.inf fun (i : ι) => (A i)ᶜ, w u = ∑ I ∈ Finset.univ.powerset, (-1) ^ I.card • ∑ u ∈ I.inf A, w u

Theorem thm.pie.2: The weighted version of the Principle of Inclusion and Exclusion.

For a finite type U, finitely many subsets A₁, ..., Aₙ (indexed by a finite type ι), an additive abelian group G, and a weight function w : U → G:

∑{u ∈ U : u ∉ Aᵢ for all i} w(u) = ∑{I ⊆ ι} (-1)^|I| ∑_{u ∈ U : u ∈ Aᵢ for all i ∈ I} w(u)

This generalizes the size version (Theorem thm.pie.1) which is obtained by taking w(u) = 1.

The left-hand side sums w(u) over all elements u that belong to none of the subsets Aᵢ. The right-hand side is an alternating sum over all subsets I of the index set, where we sum w(u) over elements belonging to all Aᵢ with i ∈ I.

theorem AlgebraicCombinatorics.InclusionExclusion.weighted_pie' {ι : Type u_1} {U : Type u_2} {G : Type u_3} [DecidableEq ι] [Fintype U] [DecidableEq U] [AddCommGroup G] (s : Finset ι) (A : ι → Finset U) (w : U → G) : ∑ u ∈ s.inf fun (i : ι) => (A i)ᶜ, w u = ∑ I ∈ s.powerset, (-1) ^ I.card • ∑ u ∈ I.inf A, w u

Theorem thm.pie.2 (alternative formulation with explicit index set): The weighted PIE with an explicit finite index set s of "rules".

This version allows indexing by a subset s of a larger type ι, rather than requiring a finite type for the index.

theorem AlgebraicCombinatorics.InclusionExclusion.size_pie_from_weighted {ι : Type u_1} {U : Type u_2} [DecidableEq ι] [Fintype U] [DecidableEq U] (s : Finset ι) (A : ι → Finset U) : ↑(s.inf fun (i : ι) => (A i)ᶜ).card = ∑ I ∈ s.powerset, (-1) ^ I.card * ↑(I.inf A).card

The size version of PIE (Theorem thm.pie.1) follows from the weighted version by taking w(u) = 1 for all u.

This demonstrates that thm.pie.1 is a special case of thm.pie.2.