Theorems · Theorem · group theory

FreeGroup.injective_lift_of_ping_pong

∀ {ι : Type u_1} [Nontrivial ι] {G : Type u_1} [inst : Group G] (a : ι → G) {α : Type u_4} [inst_1 : MulAction G α]
  (X Y : ι → Set α),
  (∀ (i : ι), (X i).Nonempty) →
    Pairwise (Function.onFun Disjoint X) →
      Pairwise (Function.onFun Disjoint Y) →
        (∀ (i j : ι), Disjoint (X i) (Y j)) →
          (∀ (i : ι), a i • (Y i)ᶜ ⊆ X i) → (∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i) → Function.Injective ⇑(FreeGroup.lift a)

The Ping-Pong-Lemma. Given a group action of G on X so that the generators of the free groups act in specific ways on disjoint subsets X i and Y i we can prove that lift f is injective, and thus the image of lift f is isomorphic to the free group. Often the Ping-Pong-Lemma is stated with regard to group elements that generate the whole group; we generalize to arbitrary group homomorphisms from the free group to G and do not require the group to be generated by the elements.

Defined in

Mathlib.GroupTheory.CoprodI

Cited by

0 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontrivialGroupMulAction