P. M. Neumann's separation lemma

If a group G acts on Ω and A, B are finite subsets, some g : G moves A off B (g • a ∉ B for all a ∈ A) in two situations: when the action is pretransitive and #A · #B < #Ω, and when every point of A has an infinite orbit. Both follow from B. H. Neumann's covering lemma (Subgroup.exists_index_le_card_of_leftCoset_cover): otherwise G is covered by the #A · #B cosets t(a, b) • stabilizer G a.

Main results

• TotD.separation_lemma_of_pretransitive, TotD.separation_lemma_of_pretransitive': the finite version (with Nat.card and with Fintype.card).
• TotD.neumann_separation_lemma, TotD.neumann_separation_lemma': the infinite version.

References

• P. J. Cameron, Synchronization, LTCC lecture notes, 2010, Lecture 3.
• J. Araújo, P. J. Cameron, B. Steinberg, Between primitive and 2-transitive: synchronization and its friends, EMS Surv. Math. Sci. 4 (2017) 101–184.

theorem TotD.separation_lemma_of_pretransitive (G : Type u_1) {Ω : Type u_2} [Group G] [MulAction G Ω] [MulAction.IsPretransitive G Ω] {A B : Finset Ω} (h : A.card * B.card < Nat.card Ω) : ∃ (g : G), ∀ a ∈ A, g • a ∉ B

Separation lemma, finite/transitive version (Cameron, "Synchronization", Lecture 3, Theorem 6b). If G acts pretransitively on Ω and A B : Finset Ω satisfy A.card * B.card < Nat.card Ω, then some g : G maps A off B.

No finiteness is assumed of G or Ω: the hypothesis forces Ω finite nonempty (Nat.card of an infinite type is 0), and the counting runs through subgroup indices rather than |G|.

theorem TotD.separation_lemma_of_pretransitive' (G : Type u_1) {Ω : Type u_2} [Group G] [MulAction G Ω] [Fintype Ω] [MulAction.IsPretransitive G Ω] {A B : Finset Ω} (h : A.card * B.card < Fintype.card Ω) : ∃ (g : G), ∀ a ∈ A, g • a ∉ B

Fintype.card form of separation_lemma_of_pretransitive.

theorem TotD.neumann_separation_lemma (G : Type u_1) {Ω : Type u_2} [Group G] [MulAction G Ω] {A B : Set Ω} (hA : A.Finite) (hB : B.Finite) (horb : ∀ a ∈ A, (MulAction.orbit G a).Infinite) : ∃ (g : G), g • A ∩ B = ∅

P. M. Neumann's separation lemma (1974), sharp hypothesis: if the orbit of every point of A is infinite, then for finite A B : Set Ω some g : G satisfies (g • A) ∩ B = ∅.

Proof: otherwise the sets {g | g • a = b}, (a, b) ∈ A × B — left cosets of the stabilizers of points of A — cover G, so by B. H. Neumann's covering lemma some stabilizer G a has finite index; but its index is (orbit G a).ncard = 0.

theorem TotD.neumann_separation_lemma' (G : Type u_1) {Ω : Type u_2} [Group G] [MulAction G Ω] {A B : Set Ω} (hA : A.Finite) (hB : B.Finite) (horb : ∀ (x : Ω), (MulAction.orbit G x).Infinite) : ∃ (g : G), g • A ∩ B = ∅

P. M. Neumann's separation lemma, classical statement: if all G-orbits on Ω are infinite, then any two finite subsets of Ω can be separated by some g : G.