# mathlib3documentation

group_theory.free_product

# The free product of groups or monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given an ι-indexed family M of monoids, we define their free product (categorical coproduct) free_product M. When ι and all M i have decidable equality, the free product bijects with the type word M of reduced words. This bijection is constructed by defining an action of free_product M on word M.

When M i are all groups, free_product M is also a group (and the coproduct in the category of groups).

## Main definitions #

• free_product M: the free product, defined as a quotient of a free monoid.
• free_product.of {i} : M i →* free_product M.
• free_product.lift : (Π {i}, M i →* N) ≃ (free_product M →* N): the universal property.
• free_product.word M: the type of reduced words.
• free_product.word.equiv M : free_product M ≃ word M.
• free_product.neword M i j: an inductive description of non-empty words with first letter from M i and last letter from M j, together with an API (singleton, append, head, tail, to_word, prod, inv). Used in the proof of the Ping-Pong-lemma.
• free_product.lift_injective_of_ping_pong: The Ping-Pong-lemma, proving injectivity of the lift. See the documentation of that theorem for more information.

## Remarks #

There are many answers to the question "what is the free product of a family M of monoids?", and they are all equivalent but not obviously equivalent. We provide two answers. The first, almost tautological answer is given by free_product M, which is a quotient of the type of words in the alphabet Σ i, M i. It's straightforward to define and easy to prove its universal property. But this answer is not completely satisfactory, because it's difficult to tell when two elements x y : free_product M are distinct since free_product M is defined as a quotient.

The second, maximally efficient answer is given by word M. An element of word M is a word in the alphabet Σ i, M i, where the letter ⟨i, 1⟩ doesn't occur and no adjacent letters share an index i. Since we only work with reduced words, there is no need for quotienting, and it is easy to tell when two elements are distinct. However it's not obvious that this is even a monoid!

We prove that every element of free_product M can be represented by a unique reduced word, i.e. free_product M and word M are equivalent types. This means that word M can be given a monoid structure, and it lets us tell when two elements of free_product M are distinct.

There is also a completely tautological, maximally inefficient answer given by algebra.category.Mon.colimits. Whereas free_product M at least ensures that (any instance of) associativity holds by reflexivity, in this answer associativity holds because of quotienting. Yet another answer, which is constructively more satisfying, could be obtained by showing that free_product.rel is confluent.

## References #

van der Waerden, Free products of groups

inductive free_product.rel {ι : Type u_1} (M : ι Type u_2) [Π (i : ι), monoid (M i)] :
free_monoid (Σ (i : ι), M i) free_monoid (Σ (i : ι), M i) Prop

A relation on the free monoid on alphabet Σ i, M i, relating ⟨i, 1⟩ with 1 and ⟨i, x⟩ * ⟨i, y⟩ with ⟨i, x * y⟩.

def free_product {ι : Type u_1} (M : ι Type u_2) [Π (i : ι), monoid (M i)] :
Type (max u_1 u_2)

The free product (categorical coproduct) of an indexed family of monoids.

Equations
Instances for free_product
@[protected, instance]
def free_product.inhabited {ι : Type u_1} (M : ι Type u_2) [Π (i : ι), monoid (M i)] :
@[protected, instance]
def free_product.monoid {ι : Type u_1} (M : ι Type u_2) [Π (i : ι), monoid (M i)] :
theorem free_product.word.ext_iff {ι : Type u_1} {M : ι Type u_2} {_inst_1 : Π (i : ι), monoid (M i)} (x y : free_product.word M) :
theorem free_product.word.ext {ι : Type u_1} {M : ι Type u_2} {_inst_1 : Π (i : ι), monoid (M i)} (x y : free_product.word M) (h : x.to_list = y.to_list) :
x = y
@[ext]
structure free_product.word {ι : Type u_1} (M : ι Type u_2) [Π (i : ι), monoid (M i)] :
Type (max u_1 u_2)

The type of reduced words. A reduced word cannot contain a letter 1, and no two adjacent letters can come from the same summand.

Instances for free_product.word
def free_product.of {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i : ι} :
M i →*

The inclusion of a summand into the free product.

Equations
theorem free_product.of_apply {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i : ι} (m : M i) :
@[ext]
theorem free_product.ext_hom {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {N : Type u_3} [monoid N] (f g : →* N) (h : (i : ι), ) :
f = g
def free_product.lift {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {N : Type u_3} [monoid N] :
(Π (i : ι), M i →* N) →* N)

A map out of the free product corresponds to a family of maps out of the summands. This is the universal property of the free product, charaterizing it as a categorical coproduct.

Equations
@[simp]
theorem free_product.lift_symm_apply {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {N : Type u_3} [monoid N] (f : →* N) (i : ι) :
@[simp]
theorem free_product.lift_of {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {N : Type u_3} [monoid N] (fi : Π (i : ι), M i →* N) {i : ι} (m : M i) :
= (fi i) m
theorem free_product.induction_on {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {C : Prop} (m : free_product M) (h_one : C 1) (h_of : (i : ι) (m : M i), C ) (h_mul : (x y : , C x C y C (x * y)) :
C m
theorem free_product.of_left_inverse {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [decidable_eq ι] (i : ι) :
theorem free_product.of_injective {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] (i : ι) :
theorem free_product.lift_mrange_le {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {N : Type u_3} [monoid N] (f : Π (i : ι), M i →* N) {s : submonoid N} (h : (i : ι), monoid_hom.mrange (f i) s) :
theorem free_product.mrange_eq_supr {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {N : Type u_3} [monoid N] (f : Π (i : ι), M i →* N) :
= (i : ι), monoid_hom.mrange (f i)
@[protected, instance]
def free_product.has_inv {ι : Type u_1} (G : ι Type u_4) [Π (i : ι), group (G i)] :
Equations
theorem free_product.inv_def {ι : Type u_1} (G : ι Type u_4) [Π (i : ι), group (G i)] (x : free_product G) :
@[protected, instance]
def free_product.group {ι : Type u_1} (G : ι Type u_4) [Π (i : ι), group (G i)] :
Equations
theorem free_product.lift_range_le {ι : Type u_1} (G : ι Type u_4) [Π (i : ι), group (G i)] {N : Type u_2} [group N] (f : Π (i : ι), G i →* N) {s : subgroup N} (h : (i : ι), (f i).range s) :
s
theorem free_product.range_eq_supr {ι : Type u_1} (G : ι Type u_4) [Π (i : ι), group (G i)] {N : Type u_2} [group N] (f : Π (i : ι), G i →* N) :
= (i : ι), (f i).range
def free_product.word.empty {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] :

The empty reduced word.

Equations
@[protected, instance]
def free_product.word.inhabited {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] :
Equations
def free_product.word.prod {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] (w : free_product.word M) :

A reduced word determines an element of the free product, given by multiplication.

Equations
@[simp]
theorem free_product.word.prod_empty {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] :
def free_product.word.fst_idx {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] (w : free_product.word M) :

fst_idx w is some i if the first letter of w is ⟨i, m⟩ with m : M i. If w is empty then it's none.

Equations
theorem free_product.word.fst_idx_ne_iff {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {w : free_product.word M} {i : ι} :
(l : Σ (i : ι), M i), l w.to_list.head' i l.fst
theorem free_product.word.pair.ext_iff {ι : Type u_1} {M : ι Type u_2} {_inst_1 : Π (i : ι), monoid (M i)} {i : ι} (x y : i) :
@[ext]
structure free_product.word.pair {ι : Type u_1} (M : ι Type u_2) [Π (i : ι), monoid (M i)] (i : ι) :
Type (max u_1 u_2)

Given an index i : ι, pair M i is the type of pairs (head, tail) where head : M i and tail : word M, subject to the constraint that first letter of tail can't be ⟨i, m⟩. By prepending head to tail, one obtains a new word. We'll show that any word can be uniquely obtained in this way.

Instances for free_product.word.pair
theorem free_product.word.pair.ext {ι : Type u_1} {M : ι Type u_2} {_inst_1 : Π (i : ι), monoid (M i)} {i : ι} (x y : i) (h : x.head = y.head) (h_1 : x.tail = y.tail) :
x = y
@[protected, instance]
def free_product.word.pair.inhabited {ι : Type u_1} (M : ι Type u_2) [Π (i : ι), monoid (M i)] (i : ι) :
Equations
def free_product.word.rcons {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] {i : ι} (p : i) :

Given a pair (head, tail), we can form a word by prepending head to tail, except if head is 1 : M i then we have to just return word since we need the result to be reduced.

Equations
theorem free_product.word.cons_eq_rcons {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] {i : ι} {m : M i} {ls : list (Σ (i : ι), M i)} {h1 : (l : Σ (i : ι), M i), l i, m⟩ :: ls l.snd 1} {h2 : list.chain' (λ (l l' : Σ (i : ι), M i), l.fst l'.fst) (i, m⟩ :: ls)} :
{to_list := i, m⟩ :: ls, ne_one := h1, chain_ne := h2} = free_product.word.rcons {head := m, tail := mk_aux ls h1 h2, fst_idx_ne := _}
@[simp]
theorem free_product.word.prod_rcons {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] {i : ι} (p : i) :
theorem free_product.word.rcons_inj {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] {i : ι} :
def free_product.word.equiv_pair {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] (i : ι) :

The equivalence between words and pairs. Given a word, it decomposes it as a pair by removing the first letter if it comes from M i. Given a pair, it prepends the head to the tail.

Equations
theorem free_product.word.equiv_pair_symm {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] (i : ι) (p : i) :
theorem free_product.word.equiv_pair_eq_of_fst_idx_ne {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] {i : ι} {w : free_product.word M} (h : w.fst_idx ) :
= {head := 1, tail := w, fst_idx_ne := h}
@[protected, instance]
def free_product.word.summand_action {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] (i : ι) :
mul_action (M i)
Equations
@[protected, instance]
def free_product.word.mul_action {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] :
Equations
theorem free_product.word.of_smul_def {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] (i : ι) (w : free_product.word M) (m : M i) :
theorem free_product.word.cons_eq_smul {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] {i : ι} {m : M i} {ls : list (Σ (i : ι), M i)} {h1 : (l : Σ (i : ι), M i), l i, m⟩ :: ls l.snd 1} {h2 : list.chain' (λ (l l' : Σ (i : ι), M i), l.fst l'.fst) (i, m⟩ :: ls)} :
{to_list := i, m⟩ :: ls, ne_one := h1, chain_ne := h2} = mk_aux ls h1 h2
theorem free_product.word.smul_induction {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] {C : Prop} (h_empty : C free_product.word.empty) (h_smul : (i : ι) (m : M i) (w : , C w C w)) (w : free_product.word M) :
C w
@[simp]
theorem free_product.word.prod_smul {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] (m : free_product M) (w : free_product.word M) :
(m w).prod = m * w.prod
def free_product.word.equiv {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] :

Each element of the free product corresponds to a unique reduced word.

Equations
@[protected, instance]
def free_product.word.decidable_eq {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] :
Equations
@[protected, instance]
def free_product.word.free_product.decidable_eq {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] [Π (i : ι), decidable_eq (M i)] [decidable_eq ι] :
Equations
@[nolint]
inductive free_product.neword {ι : Type u_1} (M : ι Type u_2) [Π (i : ι), monoid (M i)] :
ι ι Type (max u_1 u_2)

A neword M i j is a representation of a non-empty reduced words where the first letter comes from M i and the last letter comes from M j. It can be constructed from singletons and via concatentation, and thus provides a useful induction principle.

Instances for free_product.neword
• free_product.neword.has_sizeof_inst
@[simp]
def free_product.neword.to_list {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (w : j) :
list (Σ (i : ι), M i)

The list represented by a given neword

Equations
theorem free_product.neword.to_list_ne_nil {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (w : j) :
@[simp]
def free_product.neword.head {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (w : j) :
M i

The first letter of a neword

Equations
@[simp]
def free_product.neword.last {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (w : j) :
M j

The last letter of a neword

Equations
@[simp]
theorem free_product.neword.to_list_head' {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (w : j) :
@[simp]
theorem free_product.neword.to_list_last' {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (w : j) :
def free_product.neword.to_word {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (w : j) :

The word M represented by a neword M i j

Equations
theorem free_product.neword.of_word {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] (w : free_product.word M) (h : w free_product.word.empty) :
(i j : ι) (w' : j), w'.to_word = w

Every nonempty word M can be constructed as a neword M i j

def free_product.neword.prod {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (w : j) :

A non-empty reduced word determines an element of the free product, given by multiplication.

Equations
@[simp]
theorem free_product.neword.singleton_head {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i : ι} (x : M i) (hne_one : x 1) :
@[simp]
theorem free_product.neword.singleton_last {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i : ι} (x : M i) (hne_one : x 1) :
hne_one).last = x
@[simp]
theorem free_product.neword.prod_singleton {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i : ι} (x : M i) (hne_one : x 1) :
hne_one).prod =
@[simp]
theorem free_product.neword.append_head {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j k l : ι} {w₁ : j} {hne : j k} {w₂ : l} :
@[simp]
theorem free_product.neword.append_last {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j k l : ι} {w₁ : j} {hne : j k} {w₂ : l} :
(w₁.append hne w₂).last = w₂.last
@[simp]
theorem free_product.neword.append_prod {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j k l : ι} {w₁ : j} {hne : j k} {w₂ : l} :
(w₁.append hne w₂).prod = w₁.prod * w₂.prod
def free_product.neword.replace_head {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (x : M i) (hnotone : x 1) (w : j) :
j

One can replace the first letter in a non-empty reduced word by an element of the same group

Equations
@[simp]
theorem free_product.neword.replace_head_head {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (x : M i) (hnotone : x 1) (w : j) :
def free_product.neword.mul_head {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (w : j) (x : M i) (hnotone : x * w.head 1) :
j

One can multiply an element from the left to a non-empty reduced word if it does not cancel with the first element in the word.

Equations
@[simp]
theorem free_product.neword.mul_head_head {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (w : j) (x : M i) (hnotone : x * w.head 1) :
@[simp]
theorem free_product.neword.mul_head_prod {ι : Type u_1} {M : ι Type u_2} [Π (i : ι), monoid (M i)] {i j : ι} (w : j) (x : M i) (hnotone : x * w.head 1) :
def free_product.neword.inv {ι : Type u_1} {G : ι Type u_4} [Π (i : ι), group (G i)] {i j : ι} (w : j) :
i

The inverse of a non-empty reduced word

Equations
@[simp]
theorem free_product.neword.inv_prod {ι : Type u_1} {G : ι Type u_4} [Π (i : ι), group (G i)] {i j : ι} (w : j) :
@[simp]
theorem free_product.neword.inv_head {ι : Type u_1} {G : ι Type u_4} [Π (i : ι), group (G i)] {i j : ι} (w : j) :
@[simp]
theorem free_product.neword.inv_last {ι : Type u_1} {G : ι Type u_4} [Π (i : ι), group (G i)] {i j : ι} (w : j) :
theorem free_product.lift_word_ping_pong {ι : Type u_1} {G : Type u_4} [group G] {H : ι Type u_5} [Π (i : ι), group (H i)] (f : Π (i : ι), H i →* G) {α : Type u_6} [ α] (X : ι set α) (hpp : pairwise (λ (i j : ι), (h : H i), h 1 (f i) h X j X i)) {i j k : ι} (w : j) (hk : j k) :
w.prod X k X i
theorem free_product.lift_word_prod_nontrivial_of_other_i {ι : Type u_1} {G : Type u_4} [group G] {H : ι Type u_5} [Π (i : ι), group (H i)] (f : Π (i : ι), H i →* G) {α : Type u_6} [ α] (X : ι set α) (hXnonempty : (i : ι), (X i).nonempty) (hXdisj : pairwise (λ (i j : ι), disjoint (X i) (X j))) (hpp : pairwise (λ (i j : ι), (h : H i), h 1 (f i) h X j X i)) {i j k : ι} (w : j) (hhead : k i) (hlast : k j) :
w.prod 1
theorem free_product.lift_word_prod_nontrivial_of_head_eq_last {ι : Type u_1} [hnontriv : nontrivial ι] {G : Type u_4} [group G] {H : ι Type u_5} [Π (i : ι), group (H i)] (f : Π (i : ι), H i →* G) {α : Type u_6} [ α] (X : ι set α) (hXnonempty : (i : ι), (X i).nonempty) (hXdisj : pairwise (λ (i j : ι), disjoint (X i) (X j))) (hpp : pairwise (λ (i j : ι), (h : H i), h 1 (f i) h X j X i)) {i : ι} (w : i) :
w.prod 1
theorem free_product.lift_word_prod_nontrivial_of_head_card {ι : Type u_1} [hnontriv : nontrivial ι] {G : Type u_4} [group G] {H : ι Type u_5} [Π (i : ι), group (H i)] (f : Π (i : ι), H i →* G) {α : Type u_6} [ α] (X : ι set α) (hXnonempty : (i : ι), (X i).nonempty) (hXdisj : pairwise (λ (i j : ι), disjoint (X i) (X j))) (hpp : pairwise (λ (i j : ι), (h : H i), h 1 (f i) h X j X i)) {i j : ι} (w : j) (hcard : 3 cardinal.mk (H i)) (hheadtail : i j) :
w.prod 1
theorem free_product.lift_word_prod_nontrivial_of_not_empty {ι : Type u_1} [hnontriv : nontrivial ι] {G : Type u_4} [group G] {H : ι Type u_5} [Π (i : ι), group (H i)] (f : Π (i : ι), H i →* G) (hcard : 3 (i : ι), 3 cardinal.mk (H i)) {α : Type u_6} [ α] (X : ι set α) (hXnonempty : (i : ι), (X i).nonempty) (hXdisj : pairwise (λ (i j : ι), disjoint (X i) (X j))) (hpp : pairwise (λ (i j : ι), (h : H i), h 1 (f i) h X j X i)) {i j : ι} (w : j) :
w.prod 1
theorem free_product.empty_of_word_prod_eq_one {ι : Type u_1} [hnontriv : nontrivial ι] {G : Type u_4} [group G] {H : ι Type u_5} [Π (i : ι), group (H i)] (f : Π (i : ι), H i →* G) (hcard : 3 (i : ι), 3 cardinal.mk (H i)) {α : Type u_6} [ α] (X : ι set α) (hXnonempty : (i : ι), (X i).nonempty) (hXdisj : pairwise (λ (i j : ι), disjoint (X i) (X j))) (hpp : pairwise (λ (i j : ι), (h : H i), h 1 (f i) h X j X i)) {w : free_product.word H} (h : w.prod = 1) :
theorem free_product.lift_injective_of_ping_pong {ι : Type u_1} [hnontriv : nontrivial ι] {G : Type u_4} [group G] {H : ι Type u_5} [Π (i : ι), group (H i)] (f : Π (i : ι), H i →* G) (hcard : 3 (i : ι), 3 cardinal.mk (H i)) {α : Type u_6} [ α] (X : ι set α) (hXnonempty : (i : ι), (X i).nonempty) (hXdisj : pairwise (λ (i j : ι), disjoint (X i) (X j))) (hpp : pairwise (λ (i j : ι), (h : H i), h 1 (f i) h X j X i)) :

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.

@[simp]
theorem free_product.is_free_group_mul_equiv {ι : Type u_1} (G : ι Type u_2) [Π (i : ι), group (G i)] [hG : Π (i : ι), is_free_group (G i)] :
@[protected, instance]
def free_product.is_free_group {ι : Type u_1} (G : ι Type u_2) [Π (i : ι), group (G i)] [hG : Π (i : ι), is_free_group (G i)] :

The free product of free groups is itself a free group

Equations
@[simp]
theorem free_product.is_free_group_generators {ι : Type u_1} (G : ι Type u_2) [Π (i : ι), group (G i)] [hG : Π (i : ι), is_free_group (G i)] :
= Σ (i : ι),
@[simp]
theorem free_group_equiv_free_product_symm_apply {ι : Type u_1} (ᾰ : free_product (λ (_x : ι), ) :
= (free_product.lift (λ (i : ι), free_group.lift (λ (pstar : unit), free_group.of i)))
@[simp]
theorem free_group_equiv_free_product_apply {ι : Type u_1} (ᾰ : free_group ι) :
= (free_group.lift (λ (i : ι),
def free_group_equiv_free_product {ι : Type u_1} :
≃* free_product (λ (_x : ι),

A free group is a free product of copies of the free_group over one generator.

Equations
theorem free_group.injective_lift_of_ping_pong {ι : Type u_1} [nontrivial ι] {G : Type u_1} [group G] (a : ι G) {α : Type u_4} [ α] (X Y : ι set α) (hXnonempty : (i : ι), (X i).nonempty) (hXdisj : pairwise (λ (i j : ι), disjoint (X i) (X j))) (hYdisj : pairwise (λ (i j : ι), disjoint (Y i) (Y j))) (hXYdisj : (i j : ι), disjoint (X i) (Y j)) (hX : (i : ι), a i (Y i) X i) (hY : (i : ι), a⁻¹ i (X i) Y i) :

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.