Section-regular partitions

For a finite group G acting transitively on a finite set Ω, counting triples (a, b, g) with g • a = b gives (∑_g #((g • A) ∩ B)) · #Ω = #A · #B · #G. Consequences: constant intersection sizes l force #A · #B = l · #Ω, and a partition all of whose translates of a section are again sections has parts of equal size.

Main definitions

• IsSection S P: S meets every part of the partition P in exactly one point.
• IsSectionRegular G P S: every translate g • S is a section of P.

Main results

• card_smul_fiber_mul_card_eq_card_group: #{g | g • a = b} · #Ω = #G for transitive actions.
• sum_card_smul_inter_mul_card: the triple count.
• card_mul_card_of_forall_card_smul_inter_eq: constant intersections give #A · #B = l · #Ω.
• IsSectionRegular.card_part_mul_card_section, IsSectionRegular.card_part_eq_card_part: the parts of a section-regular partition have size #Ω / #S.
• card_smul_inter_eq_of_forall_le, card_smul_inter_eq_of_forall_ge: if #A · #B = l · #Ω and all intersections are ≥ l (or all ≤ l), they all equal l.

References

• P. J. Cameron, Synchronization, LTCC lecture notes, 2010, Lecture 3, Theorems 8–10.

Sections and section-regular partitions

def IsSection {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] (S : Finset Ω) (P : Finpartition Finset.univ) : Prop

Cameron: S is a section (transversal) of the partition P of Ω if it contains exactly one point of every part of P.

Equations

• IsSection S P = ∀ T ∈ P.parts, (S ∩ T).card = 1

def IsSectionRegular {Ω : Type u_1} [DecidableEq Ω] [Fintype Ω] (G : Type u_3) [Group G] [MulAction G Ω] (P : Finpartition Finset.univ) (S : Finset Ω) : Prop

Cameron: P is section-regular for G with section S if g • S is a section of P for every g : G.

Equations

• IsSectionRegular G P S = ∀ (g : G), IsSection (g • S) P

theorem IsSectionRegular.isSection {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype Ω] {P : Finpartition Finset.univ} {S : Finset Ω} (hreg : IsSectionRegular G P S) : IsSection S P

The section of a section-regular partition is itself a section (take g = 1).

The transitive fibre count

theorem card_smul_fiber_mul_card_eq_card_group {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] [Fintype Ω] [MulAction.IsPretransitive G Ω] (a b : Ω) : {g : G | g • a = b}.card * Fintype.card Ω = Fintype.card G

For a transitive action of a finite group G on a finite set Ω, the number of group elements sending a to b is #G / #Ω, stated multiplied out: #{g | g • a = b} * #Ω = #G. The fibre over b of g ↦ g • a is a left coset of the stabilizer of a; conclude by orbit–stabilizer.

The averaging lemma (Cameron Theorem 10)

theorem card_smul_inter_eq_card_filter {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] (g : G) (A B : Finset Ω) : (g • A ∩ B).card = {a ∈ A | g • a ∈ B}.card

The translate-intersection count, pulled back to A: #((g • A) ∩ B) = #{a ∈ A | g • a ∈ B}.

theorem sum_card_smul_inter_mul_card {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] [Fintype Ω] [MulAction.IsPretransitive G Ω] (A B : Finset Ω) : (∑ g : G, (g • A ∩ B).card) * Fintype.card Ω = A.card * B.card * Fintype.card G

Cameron, Synchronization Lecture 3, Theorem 10 (set version, multiplied out to stay in ℕ). For a transitive action of a finite group G on a finite set Ω and any A B : Finset Ω: (∑ g : G, #((g • A) ∩ B)) * #Ω = #A * #B * #G. Both sides count the triples (a, b, g) with a ∈ A, b ∈ B, g • a = b, times #Ω.

Uniformity (Cameron Theorems 8 and 9)

theorem card_mul_card_of_forall_card_smul_inter_eq {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] [Fintype Ω] [MulAction.IsPretransitive G Ω] {A B : Finset Ω} {l : ℕ} (h : ∀ (g : G), (g • A ∩ B).card = l) : A.card * B.card = l * Fintype.card Ω

Cameron Theorem 9 (set version): if all translate intersections have the same size l, then #A * #B = l * #Ω. Immediate from the averaging lemma, cancelling #G > 0.

theorem IsSectionRegular.card_part_mul_card_section {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] [Fintype Ω] [MulAction.IsPretransitive G Ω] {P : Finpartition Finset.univ} {S : Finset Ω} (hreg : IsSectionRegular G P S) {T : Finset Ω} (hT : T ∈ P.parts) : T.card * S.card = Fintype.card Ω

Cameron Theorem 9: section-regular partitions are uniform. If P is section-regular for G with section S, every part T of P satisfies #T * #S = #Ω. This is the l = 1 case of the previous theorem: a section meets every part, in every translate, in exactly one point.

theorem IsSectionRegular.card_part_eq_card_part {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] [Fintype Ω] [MulAction.IsPretransitive G Ω] {P : Finpartition Finset.univ} {S : Finset Ω} (hreg : IsSectionRegular G P S) {T₁ T₂ : Finset Ω} (h1 : T₁ ∈ P.parts) (h2 : T₂ ∈ P.parts) : T₁.card = T₂.card

All parts of a section-regular partition have the same size ("section-regular partitions are uniform").

theorem card_smul_inter_eq_of_forall_le {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] [Fintype Ω] [Nonempty Ω] [MulAction.IsPretransitive G Ω] {A B : Finset Ω} {l : ℕ} (hAB : A.card * B.card = l * Fintype.card Ω) (hle : ∀ (g : G), l ≤ (g • A ∩ B).card) (g : G) : (g • A ∩ B).card = l

Cameron Theorem 8, "≥ forces =": if #A * #B = l * #Ω and every translate intersection has size at least l, then every translate intersection has size exactly l (the average equals l, so no term can exceed it).

theorem card_smul_inter_eq_of_forall_ge {Ω : Type u_1} [DecidableEq Ω] {G : Type u_2} [Group G] [MulAction G Ω] [Fintype G] [Fintype Ω] [Nonempty Ω] [MulAction.IsPretransitive G Ω] {A B : Finset Ω} {l : ℕ} (hAB : A.card * B.card = l * Fintype.card Ω) (hge : ∀ (g : G), (g • A ∩ B).card ≤ l) (g : G) : (g • A ∩ B).card = l

Cameron Theorem 8, "≤ forces =": if #A * #B = l * #Ω and every translate intersection has size at most l, then every translate intersection has size exactly l.