mathlib documentation

group_theory.free_product

The free product of groups or monoids #

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 #

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
@[instance]
def free_product.inhabited {ι : Type u_1} (M : ι → Type u_2) [Π (i : ι), monoid (M i)] :
@[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.

def free_product.of {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] {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 : free_product M →* N) (h : ∀ (i : ι), f.comp free_product.of = g.comp free_product.of) :
f = g

See note [partially-applied ext lemmas].

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) (free_product M →* 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 : free_product M →* 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) :
theorem free_product.induction_on {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] {C : free_product M → Prop} (m : free_product M) (h_one : C 1) (h_of : ∀ (i : ι) (m : M i), C (free_product.of m)) (h_mul : ∀ (x y : free_product M), C xC yC (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 : ι) :
@[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) :
@[instance]
def free_product.group {ι : Type u_1} (G : ι → Type u_4) [Π (i : ι), group (G i)] :
Equations
def free_product.word.empty {ι : Type u_1} {M : ι → Type u_2} [Π (i : ι), monoid (M i)] :

The empty reduced word.

Equations
@[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_nil {ι : 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 : ι} :
w.fst_idx some 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 : free_product.word.pair M i) :
x = y x.head = y.head x.tail = y.tail
@[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.

theorem free_product.word.pair.ext {ι : Type u_1} {M : ι → Type u_2} {_inst_1 : Π (i : ι), monoid (M i)} {i : ι} (x y : free_product.word.pair M i) (h : x.head = y.head) (h_1 : x.tail = y.tail) :
x = y
@[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 : free_product.word.pair M 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⟩ :: lsl.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 : free_product.word.pair M 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 : free_product.word.pair M 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 some i) :
@[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 : ι) :
Equations
@[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⟩ :: lsl.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.of m 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 : free_product.word M → Prop} (h_empty : C free_product.word.empty) (h_smul : ∀ (i : ι) (m : M i) (w : free_product.word M), C wC (free_product.of m 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
@[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
@[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