Theorems · Theorem · group theory

Monoid.CoprodI.lift_injective_of_ping_pong

∀ {ι : Type u_1} {G : Type u_4} [inst : Group G] {H : ι → Type u_5} [inst_1 : (i : ι) → Group (H i)]
  (f : (i : ι) → H i →* G),
  (3 ≤ Cardinal.mk ι ∨ ∃ i, 3 ≤ Cardinal.mk (H i)) →
    ∀ {α : Type u_6} [inst_2 : MulAction G α] (X : ι → Set α),
      (∀ (i : ι), (X i).Nonempty) →
        Pairwise (Function.onFun Disjoint X) →
          (Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i) →
            ∀ [Nontrivial ι], Function.Injective ⇑(Monoid.CoprodI.lift f)

The Ping-Pong-Lemma. Given a group action of G on X so that the H i acts in a specific way on disjoint subsets X i we can prove that lift f is injective, and thus the image of lift f is isomorphic to the free product of the H i. Often the Ping-Pong-Lemma is stated with regard to subgroups H i that generate the whole group; we generalize to arbitrary group homomorphisms f i : H i →* G and do not require the group to be generated by the images. Usually the Ping-Pong-Lemma requires that one group H i has at least three elements. This condition is only needed if # ι = 2, and we accept 3 ≤ # ι as an alternative.

Defined in

Mathlib.GroupTheory.CoprodI

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupGroupMulActionNontrivial