The pairing of two permutation characters counts double cosets #
The character of a permutation representation k[X] counts fixed points, so the normalized
pairing of two permutation characters is the Burnside average
|G|⁻¹ ∑ g, |X^g| · |Y^g|, which counts the orbits of G on X × Y. Taking X = G ⧸ H and
Y = G ⧸ K and identifying those orbits with double cosets gives
⟨Ind_H^G 1, Ind_K^G 1⟩_G = #(H \ G / K),
the pairing of two induced trivial representations.
Main statements #
TauCeti.sum_character_ofMulAction_mul_character_ofMulAction_eq_card_orbits_mul_card_group: Burnside's lemma as an unnormalized identity of character sums.TauCeti.characterPairing_ofMulAction_eq_card_orbits: the pairing of two permutation characters is the number of orbits ofGon the product.TauCeti.characterPairing_ofMulAction_quotient_eq_card_doubleCosetQuotient: the specialization to two coset spaces, whose value is the number of double cosets.TauCeti.characterPairing_ofMulAction_quotient_sub_punit_eq_card_doubleCosetQuotient_sub_one: the same pairing for the two coset permutation characters with the trivial character removed, one less than the number of double cosets.TauCeti.characterPairing_ind_trivial_eq_card_doubleCosetQuotient: the same value for the pairing of two induced trivial representations.
Implementation notes #
All the identities are equalities in the coefficient field k, with the counts cast into k, and
the normalized ones assume IsUnit (Nat.card G : k) so that the |G|⁻¹ in
TauCeti.ClassFunction.characterPairing is meaningful. No algebraic closure and no orthogonality
of irreducible characters is used: the proof is Burnside's lemma, not a decomposition of the
permutation representation into irreducibles. In particular the statements are valid in
characteristic p for p ∤ |G| and without assuming k algebraically closed; Maschke's theorem
does make the permutation representation semisimple under exactly this hypothesis, but nothing
below uses that, only the fact that its character counts fixed points.
The pairing ⟨χ, ψ⟩ = |G|⁻¹ ∑ g, χ g * ψ g⁻¹ is bilinear rather than Hermitian, and the inversion
in its second argument is exactly what MulAction.fixedBy_inv absorbs.
References #
This is the "⟨Ind_H^G 1, Ind_H^G 1⟩_G = #(H \ G / H)" clause of the permutation-character item of
Layer 2 in TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md, proved here for
two possibly different subgroups.
- J.-P. Serre, Linear Representations of Finite Groups, Chapter 7.3, Exercise 7.3.
Burnside's lemma for two permutation characters. The unnormalized sum
∑ g, χ_X(g) · χ_Y(g⁻¹) is the number of orbits of G on X × Y times the order of G.
This form carries no division, so it holds over any field.
The pairing of two permutation characters counts orbits on the product. For a finite group
G whose order is invertible in k, the normalized pairing of the characters of k[X] and k[Y]
is the number of orbits of G on X × Y.
The pairing of two coset permutation characters counts double cosets. For a finite group
G whose order is invertible in k, the normalized pairing of the characters of k[G ⧸ H] and
k[G ⧸ K] is the number of double cosets H \ G / K.
The pairing of two coset permutation characters with the trivial character removed. For a
finite group G whose order is invertible in k, subtracting the character of the one-point
G-set from each of the characters of k[G ⧸ H] and k[G ⧸ K] drops their pairing from the
number of double cosets H \ G / K to one less than it: the three extra Burnside terms are 1
each, because G is transitive on each coset space and on the point.
For K = H this is the norm of the augmentation, or Steinberg, character of k[G ⧸ H], whose
value is therefore #(H \ G / H) - 1.
The pairing of two induced trivial representations counts double cosets. For a finite
group G whose order is invertible in k, the pairing of the characters of Ind_H^G 1 and
Ind_K^G 1 is the number of double cosets H \ G / K.
For K = H this is the classical statement that ⟨Ind_H^G 1, Ind_H^G 1⟩_G counts H \ G / H.