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 #
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.
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 #
- of_one : ∀ {ι : Type u_1} {M : ι → Type u_2} [_inst_1 : Π (i : ι), monoid (M i)] (i : ι), free_product.rel M (free_monoid.of ⟨i, 1⟩) 1
- of_mul : ∀ {ι : Type u_1} {M : ι → Type u_2} [_inst_1 : Π (i : ι), monoid (M i)] {i : ι} (x y : M i), free_product.rel M ((free_monoid.of ⟨i, x⟩) * free_monoid.of ⟨i, y⟩) (free_monoid.of ⟨i, x * y⟩)
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⟩.
The free product (categorical coproduct) of an indexed family of monoids.
Equations
- free_product M = (con_gen (free_product.rel M)).quotient
- to_list : list (Σ (i : ι), M i)
- ne_one : ∀ (l : Σ (i : ι), M i), l ∈ self.to_list → l.snd ≠ 1
- chain_ne : list.chain' (λ (l l' : Σ (i : ι), M i), l.fst ≠ l'.fst) self.to_list
The type of reduced words. A reduced word cannot contain a letter 1, and no two adjacent
letters can come from the same summand.
The inclusion of a summand into the free product.
Equations
- free_product.of = {to_fun := λ (x : M i), ⇑((con_gen (free_product.rel M)).mk') (free_monoid.of ⟨i, x⟩), map_one' := _, map_mul' := _}
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
- free_product.lift = {to_fun := λ (fi : Π (i : ι), M i →* N), (con_gen (free_product.rel M)).lift (⇑free_monoid.lift (λ (p : Σ (i : ι), M i), ⇑(fi p.fst) p.snd)) _, inv_fun := λ (f : free_product M →* N) (i : ι), f.comp free_product.of, left_inv := _, right_inv := _}
Equations
- free_product.has_inv G = {inv := mul_opposite.unop ∘ ⇑(⇑free_product.lift (λ (i : ι), (⇑monoid_hom.op free_product.of).comp (mul_equiv.inv' (G i)).to_monoid_hom))}
Equations
- free_product.group G = {mul := monoid.mul (free_product.monoid G), mul_assoc := _, one := monoid.one (free_product.monoid G), one_mul := _, mul_one := _, npow := monoid.npow (free_product.monoid G), npow_zero' := _, npow_succ' := _, inv := has_inv.inv (free_product.has_inv G), div := div_inv_monoid.div._default monoid.mul _ monoid.one _ _ monoid.npow _ _ has_inv.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default monoid.mul _ monoid.one _ _ monoid.npow _ _ has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
The empty reduced word.
Equations
- free_product.word.inhabited = {default := free_product.word.empty (λ (i : ι), _inst_1 i)}
A reduced word determines an element of the free product, given by multiplication.
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.
- head : M i
- tail : free_product.word M
- fst_idx_ne : self.tail.fst_idx ≠ some i
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.
Equations
- free_product.word.pair.inhabited M i = {default := {head := 1, tail := free_product.word.empty (λ (i : ι), _inst_1 i), fst_idx_ne := _}}
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.
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
- free_product.word.equiv_pair i = {to_fun := λ (w : free_product.word M), (equiv_pair_aux i w).val, inv_fun := free_product.word.rcons i, left_inv := _, right_inv := _}
Equations
- free_product.word.summand_action i = {to_has_scalar := {smul := λ (m : M i) (w : free_product.word M), free_product.word.rcons {head := m * (⇑(free_product.word.equiv_pair i) w).head, tail := (⇑(free_product.word.equiv_pair i) w).tail, fst_idx_ne := _}}, one_smul := _, mul_smul := _}
Equations
Each element of the free product corresponds to a unique reduced word.
Equations
- free_product.word.equiv = {to_fun := λ (m : free_product M), m • free_product.word.empty, inv_fun := λ (w : free_product.word M), w.prod, left_inv := _, right_inv := _}
Equations
- free_product.word.decidable_eq = function.injective.decidable_eq free_product.word.decidable_eq._proof_1