Conjugacy class sizes in the symmetric group

The conjugacy classes of Equiv.Perm α are indexed by partitions of Fintype.card α through Equiv.Perm.partition. This file computes the size of each class. The weight attached to a partition μ is

zPart μ = ∏ i, i ^ mᵢ * mᵢ !,

where mᵢ = partMultiplicity μ i is the multiplicity of the part i in μ, that is, Mathlib's μ.parts.count i. It is the order of the centralizer of any permutation with partition μ, so the class of such a permutation has n ! / zPart μ elements.

The main results are nat_card_centralizer_eq_zPart, the multiplicative class-size formula card_partition_mul_zPart with its transported form card_partition_parts_mul_zPart_fin, and the normalisation sum_factorial_div_zPart, which says the class sizes add up to n !. These are the weights in the orthogonality relations for the characters of the symmetric group, where the class with partition μ is weighted by 1 / zPart μ. The last section reads the formula on a conjugacy class itself rather than on a fibre of the partition map, as ConjClasses.card_carrier_mul_zPart, and specializes it to the class attached to a partition, card_carrier_partitionEquivConjClasses being the form those orthogonality relations consume.

Mathlib counts permutations of a given cycle type, a multiset recording only the cycles of length at least two (Equiv.Perm.nat_card_centralizer, Equiv.Perm.card_isConj_mul_eq). The translation to partitions, which record the fixed points as parts equal to one, is zPart_partition.

Partitions of Fintype.card α and of n are different types even when Fintype.card α = n, so the statements about Equiv.Perm (Fin n) describe the permutations with partition μ by the equality σ.partition.parts = μ.parts of the underlying multisets, which determines the partition.

References

• Schur--Weyl roadmap, Layer 6, the class-sizes build item.
• Mathlib's Mathlib.GroupTheory.Perm.Centralizer, for the cycle-type count.

def TauCeti.partMultiplicity {n : ℕ} (μ : n.Partition) (i : ℕ) : ℕ

The multiplicity mᵢ of the part i in the partition μ: the number of parts of μ equal to i. This is the mᵢ of the weight zPart μ = ∏ᵢ i ^ mᵢ · mᵢ !.

It is Mathlib's Multiset.count on the parts; partMultiplicity_eq_count is a simp lemma, so proofs about multiplicities are carried out with the Multiset.count API.

Equations

• TauCeti.partMultiplicity μ i = Multiset.count i μ.parts

@[simp]

theorem TauCeti.partMultiplicity_eq_count {n : ℕ} (μ : n.Partition) (i : ℕ) : partMultiplicity μ i = Multiset.count i μ.parts

The multiplicity of a part is its count in the multiset of parts.

def TauCeti.zPart {n : ℕ} (μ : n.Partition) : ℕ

The weight z_μ = ∏ᵢ i ^ mᵢ · mᵢ ! of a partition μ, where mᵢ = partMultiplicity μ i is the multiplicity of the part i.

It is the order of the centralizer of a permutation whose cycle lengths are the parts of μ, so the conjugacy class of that permutation has n ! / zPart μ elements.

Equations

• TauCeti.zPart μ = ∏ i ∈ μ.parts.toFinset, i ^ TauCeti.partMultiplicity μ i * (TauCeti.partMultiplicity μ i).factorial

theorem TauCeti.zPart_congr {m n : ℕ} {μ : m.Partition} {ν : n.Partition} (h : μ.parts = ν.parts) : zPart μ = zPart ν

The weight depends only on the multiset of parts, so it is unchanged by transporting a partition along an equality of the number being partitioned.

theorem TauCeti.zPart_eq_prod_of_subset {n : ℕ} (μ : n.Partition) {s : Finset ℕ} (hs : μ.parts.toFinset ⊆ s) : zPart μ = ∏ i ∈ s, i ^ Multiset.count i μ.parts * (Multiset.count i μ.parts).factorial

The defining product may be taken over any finite set of naturals containing the parts: the extra factors are i ^ 0 * 0 ! = 1.

theorem TauCeti.zPart_def {n : ℕ} (μ : n.Partition) : zPart μ = ∏ i ∈ μ.parts.toFinset, i ^ partMultiplicity μ i * (partMultiplicity μ i).factorial

The defining equation of zPart: the product of i ^ mᵢ * mᵢ ! over the parts i of μ, with mᵢ = partMultiplicity μ i, the case s = μ.parts.toFinset of zPart_eq_prod_of_subset.

theorem TauCeti.zPart_pos {n : ℕ} (μ : n.Partition) : 0 < zPart μ

The weight of a partition is positive; the parts of a partition are positive.

@[simp]

theorem TauCeti.zPart_indiscrete {n : ℕ} (hn : n ≠ 0) : zPart (Nat.Partition.indiscrete n) = n

The weight of the one-part partition of n is n: for 2 ≤ n an n-cycle commutes exactly with its own powers, and for n = 1 the centralizer is the trivial group.

theorem TauCeti.zPart_partition {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) : zPart σ.partition = (Fintype.card α - σ.cycleType.sum).factorial * σ.cycleType.prod * ∏ i ∈ σ.cycleType.toFinset, (Multiset.count i σ.cycleType).factorial

The weight of the partition of a permutation, in terms of its cycle type.

Mathlib's cycle type omits the fixed points; they contribute the single extra factor 1 ^ k * k !, where k is the number of fixed points.

theorem TauCeti.zPart_partition_one (α : Type u_2) [Fintype α] [DecidableEq α] : zPart (Equiv.Perm.partition 1) = (Fintype.card α).factorial

The weight of the partition of the identity is the order of the group: the cycle type of the identity is empty, so all Fintype.card α of its parts equal 1.

theorem TauCeti.nat_card_centralizer_eq_zPart {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) : Nat.card ↥(Subgroup.centralizer {σ}) = zPart σ.partition

The centralizer of a permutation has order the weight of its partition.

theorem TauCeti.card_isConj_mul_zPart {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) : Nat.card ↑{τ : Equiv.Perm α | IsConj σ τ} * zPart σ.partition = (Fintype.card α).factorial

The class-size formula in its conjugacy formulation: the conjugacy class of σ has (Fintype.card α)! / zPart σ.partition elements.

theorem TauCeti.card_partition_mul_zPart {α : Type u_1} [Fintype α] [DecidableEq α] (μ : (Fintype.card α).Partition) : Nat.card { σ : Equiv.Perm α // σ.partition = μ } * zPart μ = (Fintype.card α).factorial

The class-size formula: the permutations with partition μ number (Fintype.card α)! / zPart μ.

Stated multiplicatively, so it carries no divisibility obligation; the quotient form is card_partition_div_zPart.

theorem TauCeti.card_partition_parts_mul_zPart {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (h : Fintype.card α = n) (μ : n.Partition) : Nat.card { σ : Equiv.Perm α // σ.partition.parts = μ.parts } * zPart μ = n.factorial

The class-size formula transported along an equality Fintype.card α = n.

theorem TauCeti.card_partition_parts_mul_zPart_fin (n : ℕ) (μ : n.Partition) : Nat.card { σ : Equiv.Perm (Fin n) // σ.partition.parts = μ.parts } * zPart μ = n.factorial

The class-size formula for Equiv.Perm (Fin n), the form the roadmap states: the permutations with partition μ number n ! / zPart μ.

theorem TauCeti.zPart_dvd_factorial {n : ℕ} (μ : n.Partition) : zPart μ ∣ n.factorial

The weight of a partition of n divides n !.

theorem TauCeti.card_partition_div_zPart {α : Type u_1} [Fintype α] [DecidableEq α] (μ : (Fintype.card α).Partition) : Nat.card { σ : Equiv.Perm α // σ.partition = μ } = (Fintype.card α).factorial / zPart μ

The quotient form of the class-size formula: the permutations with partition μ number (Fintype.card α)! / zPart μ.

theorem TauCeti.card_partition_parts_div_zPart {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (h : Fintype.card α = n) (μ : n.Partition) : Nat.card { σ : Equiv.Perm α // σ.partition.parts = μ.parts } = n.factorial / zPart μ

The quotient form of the class-size formula, transported along an equality Fintype.card α = n.

theorem TauCeti.card_partition_parts_div_zPart_fin (n : ℕ) (μ : n.Partition) : Nat.card { σ : Equiv.Perm (Fin n) // σ.partition.parts = μ.parts } = n.factorial / zPart μ

The quotient form of the class-size formula for Equiv.Perm (Fin n).

theorem TauCeti.card_partition_indiscrete {α : Type u_1} [Fintype α] [DecidableEq α] : Nat.card { σ : Equiv.Perm α // σ.partition = Nat.Partition.indiscrete (Fintype.card α) } = (Fintype.card α - 1).factorial

The permutations of α whose partition is the one-part partition of n = Fintype.card α number (n - 1)!.

For 2 ≤ n these are the n-cycles. For n ≤ 1 the fibre is the identity alone and both sides are 1, but the identity is not a cycle in Mathlib's sense: the one-part partition of 0 has no parts, and that of 1 has the single part 1, which is the partition of the identity of a one-element type.

theorem TauCeti.card_partition_parts_indiscrete {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (h : Fintype.card α = n) : Nat.card { σ : Equiv.Perm α // σ.partition.parts = (Nat.Partition.indiscrete n).parts } = (n - 1).factorial

The count of the permutations with the one-part partition, transported along an equality Fintype.card α = n.

theorem TauCeti.card_partition_parts_indiscrete_fin (n : ℕ) : Nat.card { σ : Equiv.Perm (Fin n) // σ.partition.parts = (Nat.Partition.indiscrete n).parts } = (n - 1).factorial

There are (n - 1)! n-cycles in Equiv.Perm (Fin n) when 2 ≤ n; for n ≤ 1 the fibre is the identity permutation of Fin n, which is not a cycle, and both sides are 1.

theorem TauCeti.sum_card_partition (α : Type u_2) [Fintype α] [DecidableEq α] : ∑ μ : (Fintype.card α).Partition, Nat.card { σ : Equiv.Perm α // σ.partition = μ } = (Fintype.card α).factorial

The permutations of a finite type are partitioned by their partitions.

theorem TauCeti.sum_card_partition_parts {n : ℕ} (α : Type u_2) [Fintype α] [DecidableEq α] (h : Fintype.card α = n) : ∑ μ : n.Partition, Nat.card { σ : Equiv.Perm α // σ.partition.parts = μ.parts } = n.factorial

The fibre decomposition transported along an equality Fintype.card α = n.

theorem TauCeti.sum_factorial_div_zPart (n : ℕ) : ∑ μ : n.Partition, n.factorial / zPart μ = n.factorial

The class sizes add up to the order of the group. Every division here is exact, by zPart_dvd_factorial.

This is the natural-number form of the normalisation of the orthogonality weights; the rational identity ∑_μ 1 / z_μ = 1, which divides this one by n !, is not formalised here.

The class attached to a partition

theorem TauCeti.zPart_partitionEquivConjClasses_symm_mk (n : ℕ) (σ : Equiv.Perm (Fin n)) : zPart ((partitionEquivConjClasses n).symm (ConjClasses.mk σ)) = zPart σ.partition

The weight of the partition indexing the class of σ is the weight of the partition of σ: the transport TauCeti.parts_partitionEquivConjClasses_symm_mk leaves the parts, hence the weight, alone.

For a general finite type the equivalence carries no transport, and TauCeti.partitionEquivPermConjClasses_symm_mk already identifies the indexing partition with σ.partition itself, so no separate statement is needed there.

theorem ConjClasses.card_carrier_mul_zPart {α : Type u_1} [Fintype α] [DecidableEq α] (C : ConjClasses (Equiv.Perm α)) : Nat.card ↑C.carrier * TauCeti.zPart (TauCeti.permConjClassPartition C) = (Fintype.card α).factorial

The multiplicative class-size formula on a conjugacy class: the cardinality of a conjugacy class C of permutations of α, multiplied by zPart (permConjClassPartition C), is (Fintype.card α)!. This is TauCeti.card_isConj_mul_zPart read on the class itself rather than on the permutations conjugate to a representative.

theorem TauCeti.card_carrier_partitionEquivPermConjClasses_mul_zPart {α : Type u_1} [Fintype α] [DecidableEq α] (p : (Fintype.card α).Partition) : Nat.card ↑((partitionEquivPermConjClasses α) p).carrier * zPart p = (Fintype.card α).factorial

The multiplicative class-size formula on the class attached to a partition: the cardinality of TauCeti.partitionEquivPermConjClasses α p, multiplied by zPart p, is (Fintype.card α)!.

theorem TauCeti.card_carrier_partitionEquivPermConjClasses {α : Type u_1} [Fintype α] [DecidableEq α] (p : (Fintype.card α).Partition) : Nat.card ↑((partitionEquivPermConjClasses α) p).carrier = (Fintype.card α).factorial / zPart p

The quotient form of TauCeti.card_carrier_partitionEquivPermConjClasses_mul_zPart.

theorem TauCeti.card_carrier_partitionEquivConjClasses_mul_zPart {n : ℕ} (ν : n.Partition) : Nat.card ↑((partitionEquivConjClasses n) ν).carrier * zPart ν = n.factorial

The multiplicative class-size formula on the class attached to a partition, for Equiv.Perm (Fin n): the cardinality of TauCeti.partitionEquivConjClasses n ν, multiplied by zPart ν, is n !. This is ConjClasses.card_carrier_mul_zPart with the transport along Fintype.card (Fin n) = n carried out; it is the form the orthogonality relations consume.

theorem TauCeti.card_carrier_partitionEquivConjClasses {n : ℕ} (ν : n.Partition) : Nat.card ↑((partitionEquivConjClasses n) ν).carrier = n.factorial / zPart ν

The quotient form of TauCeti.card_carrier_partitionEquivConjClasses_mul_zPart.