Burnside's lemma on a product of two G-sets

A point of a product G-set X × Y is fixed by g exactly when both of its components are, so Mathlib's Burnside lemma MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group, applied to X × Y, reads

∑ g : G, |X^g| * |Y^g| = |(X × Y) / G| * |G|.

This is the shape in which Burnside's lemma computes the pairing of two permutation characters. For disjoint unions, the analogous counting rules add the fixed-point counts, including for an indexed family of sets on which the action leaves the index fixed.

Main statements

• TauCeti.fixedBy_prod: the fixed points of g on X × Y are the product of its fixed points on X and on Y.
• TauCeti.card_fixedBy_prod: the corresponding count.
• TauCeti.card_fixedBy_sum and TauCeti.card_fixedBy_sigma: fixed-point counts on disjoint unions.
• TauCeti.sum_card_fixedBy_mul_card_fixedBy_eq_card_orbits_mul_card_group: Burnside's lemma on X × Y.

Implementation notes

Counts are phrased with Nat.card, with Set.ncard simp forms for disjoint unions. Mathlib's Burnside lemma is stated with Fintype.card and carries Fintype instances for each fixed-point set, which are supplied here from Finite X and Finite Y rather than assumed.

@[simp]

theorem TauCeti.fixedBy_prod {G : Type u_1} (X : Type u_2) (Y : Type u_3) [Monoid G] [MulAction G X] [MulAction G Y] (g : G) : MulAction.fixedBy (X × Y) g = MulAction.fixedBy X g ×ˢ MulAction.fixedBy Y g

A point of a product G-set is fixed exactly when both of its components are.

theorem TauCeti.card_fixedBy_prod {G : Type u_1} (X : Type u_2) (Y : Type u_3) [Monoid G] [MulAction G X] [MulAction G Y] (g : G) : Nat.card ↑(MulAction.fixedBy (X × Y) g) = Nat.card ↑(MulAction.fixedBy X g) * Nat.card ↑(MulAction.fixedBy Y g)

The fixed points of g on a product G-set are counted by the product of the two fixed-point counts.

theorem TauCeti.card_fixedBy_sum {G : Type u_4} {X : Type u_5} {Y : Type u_6} [Monoid G] [MulAction G X] [MulAction G Y] [Finite X] [Finite Y] (g : G) : Nat.card ↑(MulAction.fixedBy (X ⊕ Y) g) = Nat.card ↑(MulAction.fixedBy X g) + Nat.card ↑(MulAction.fixedBy Y g)

The fixed points on a disjoint union are counted by the sum of the fixed-point counts.

@[simp]

theorem TauCeti.ncard_fixedBy_sum {G : Type u_4} {X : Type u_5} {Y : Type u_6} [Monoid G] [MulAction G X] [MulAction G Y] [Finite X] [Finite Y] (g : G) : (MulAction.fixedBy (X ⊕ Y) g).ncard = (MulAction.fixedBy X g).ncard + (MulAction.fixedBy Y g).ncard

The fixed-point count on a disjoint union, in simp normal form.

theorem TauCeti.card_fixedBy_sigma {G : Type u_4} {ι : Type u_5} [Monoid G] [Finite ι] (X : ι → Type u_6) [(i : ι) → MulAction G (X i)] [∀ (i : ι), Finite (X i)] (g : G) : Nat.card ↑(MulAction.fixedBy ((i : ι) × X i) g) = ∑ᶠ (i : ι), Nat.card ↑(MulAction.fixedBy (X i) g)

For the fiberwise action on an indexed disjoint union, fixed-point counts add over the indices. The monoid fixes the index of each point.

@[simp]

theorem TauCeti.ncard_fixedBy_sigma {G : Type u_4} {ι : Type u_5} [Monoid G] [Finite ι] (X : ι → Type u_6) [(i : ι) → MulAction G (X i)] [∀ (i : ι), Finite (X i)] (g : G) : (MulAction.fixedBy ((i : ι) × X i) g).ncard = ∑ᶠ (i : ι), (MulAction.fixedBy (X i) g).ncard

The fixed-point count on a fiberwise indexed disjoint union, in simp normal form.

theorem TauCeti.sum_card_fixedBy_mul_card_fixedBy_eq_card_orbits_mul_card_group {G : Type u_1} (X : Type u_2) (Y : Type u_3) [Group G] [MulAction G X] [MulAction G Y] [Fintype G] [Finite X] [Finite Y] : ∑ g : G, Nat.card ↑(MulAction.fixedBy X g) * Nat.card ↑(MulAction.fixedBy Y g) = Nat.card (MulAction.orbitRel.Quotient G (X × Y)) * Nat.card G

Burnside's lemma on a product. For a finite group G acting on two finite sets X and Y, the sum over g : G of the product of the two fixed-point counts is the number of orbits of G on X × Y, times the order of G.