The coproduct (a.k.a. the free product) of groups or monoids #
Given an ι
-indexed family M
of monoids,
we define their coproduct (a.k.a. free product) Monoid.CoprodI M
.
As usual, we use the suffix I
for an indexed (co)product,
leaving Coprod
for the coproduct of two monoids.
When ι
and all M i
have decidable equality,
the free product bijects with the type Monoid.CoprodI.Word M
of reduced words.
This bijection is constructed
by defining an action of Monoid.CoprodI M
on Monoid.CoprodI.Word M
.
When M i
are all groups, Monoid.CoprodI M
is also a group
(and the coproduct in the category of groups).
Main definitions #
Monoid.CoprodI M
: the free product, defined as a quotient of a free monoid.Monoid.CoprodI.of {i} : M i →* Monoid.CoprodI M
.Monoid.CoprodI.lift : (∀ {i}, M i →* N) ≃ (Monoid.CoprodI M →* N)
: the universal property.Monoid.CoprodI.Word M
: the type of reduced words.Monoid.CoprodI.Word.equiv M : Monoid.CoprodI M ≃ word M
.Monoid.CoprodI.NeWord M i j
: an inductive description of non-empty words with first letter fromM i
and last letter fromM j
, together with an API (singleton
,append
,head
,tail
,to_word
,Prod
,inv
). Used in the proof of the Ping-Pong-lemma.Monoid.CoprodI.lift_injective_of_ping_pong
: The Ping-Pong-lemma, proving injectivity of thelift
. See the documentation of that theorem for more information.
Remarks #
There are many answers to the question "what is the coproduct 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 Monoid.CoprodI 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 : Monoid.CoprodI M
are distinct
since Monoid.CoprodI M
is defined as a quotient.
The second, maximally efficient answer is given by Monoid.CoprodI.Word M
.
An element of Monoid.CoprodI.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 Monoid.CoprodI M
can be represented by a unique reduced word,
i.e. Monoid.CoprodI M
and Monoid.CoprodI.Word M
are equivalent types.
This means that Monoid.CoprodI.Word M
can be given a monoid structure,
and it lets us tell when two elements of Monoid.CoprodI M
are distinct.
There is also a completely tautological, maximally inefficient answer
given by MonCat.Colimits.ColimitType
.
Whereas Monoid.CoprodI 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 Monoid.CoprodI.Rel
is confluent.
References #
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⟩
.
- of_one: ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (i : ι), Monoid.CoprodI.Rel M (FreeMonoid.of ⟨i, 1⟩) 1
- of_mul: ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (x y : M i), Monoid.CoprodI.Rel M (FreeMonoid.of ⟨i, x⟩ * FreeMonoid.of ⟨i, y⟩) (FreeMonoid.of ⟨i, x * y⟩)
Instances For
The free product (categorical coproduct) of an indexed family of monoids.
Equations
- Monoid.CoprodI M = (conGen (Monoid.CoprodI.Rel M)).Quotient
Instances For
Equations
- instMonoidCoprodI M = id inferInstance
Equations
- instInhabitedCoprodI M = { default := 1 }
The type of reduced words. A reduced word cannot contain a letter 1
, and no two adjacent
letters can come from the same summand.
- toList : List ((i : ι) × M i)
- ne_one : ∀ l ∈ self.toList, l.snd ≠ 1
A reduced word does not contain
1
- chain_ne : List.Chain' (fun (l l' : (i : ι) × M i) => l.fst ≠ l'.fst) self.toList
Adjacent letters are not from the same summand.
Instances For
A reduced word does not contain 1
Adjacent letters are not from the same summand.
The inclusion of a summand into the free product.
Equations
- Monoid.CoprodI.of = { toFun := fun (x : M i) => (conGen (Monoid.CoprodI.Rel M)).mk' (FreeMonoid.of ⟨i, x⟩), map_one' := ⋯, map_mul' := ⋯ }
Instances For
See note [partially-applied ext lemmas].
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, characterizing it as a categorical coproduct.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Monoid.CoprodI.instInv G = { inv := MulOpposite.unop ∘ ⇑(Monoid.CoprodI.lift fun (i : ι) => (MonoidHom.op Monoid.CoprodI.of).comp (MulEquiv.inv' (G i)).toMonoidHom) }
Equations
The empty reduced word.
Equations
- Monoid.CoprodI.Word.empty = { toList := [], ne_one := ⋯, chain_ne := ⋯ }
Instances For
Equations
- Monoid.CoprodI.Word.instInhabited = { default := Monoid.CoprodI.Word.empty }
A reduced word determines an element of the free product, given by multiplication.
Instances For
fstIdx 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
- w.fstIdx = Option.map Sigma.fst w.toList.head?
Instances For
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.
- head : M i
An element of
M i
, the first letter of the word. - tail : Monoid.CoprodI.Word M
The remaining letters of the word, excluding the first letter
The index first letter of tail of a
Pair M i
is not equal toi
Instances For
The index first letter of tail of a Pair M i
is not equal to i
Equations
- Monoid.CoprodI.Word.instInhabitedPair M i = { default := { head := 1, tail := Monoid.CoprodI.Word.empty, fstIdx_ne := ⋯ } }
Construct a new Word
without any reduction. The underlying list of
cons m w _ _
is ⟨_, m⟩::w
Equations
- Monoid.CoprodI.Word.cons m w hmw h1 = { toList := ⟨i, m⟩ :: w.toList, ne_one := ⋯, chain_ne := ⋯ }
Instances For
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
- Monoid.CoprodI.Word.rcons p = if h : p.head = 1 then p.tail else Monoid.CoprodI.Word.cons p.head p.tail ⋯ h
Instances For
Induct on a word by adding letters one at a time without reduction,
effectively inducting on the underlying List
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- Monoid.CoprodI.Word.equivPair i = { toFun := fun (w : Monoid.CoprodI.Word M) => ↑(Monoid.CoprodI.Word.equivPairAux i w), invFun := Monoid.CoprodI.Word.rcons, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
Equations
- Monoid.CoprodI.Word.instMulAction = MulAction.ofEndHom (Monoid.CoprodI.lift fun (x : ι) => MulAction.toEndHom)
Each element of the free product corresponds to a unique reduced word.
Equations
- Monoid.CoprodI.Word.equiv = { toFun := fun (m : Monoid.CoprodI M) => m • Monoid.CoprodI.Word.empty, invFun := fun (w : Monoid.CoprodI.Word M) => w.prod, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
- Monoid.CoprodI.Word.instDecidableEq = Function.Injective.decidableEq ⋯
Equations
- Monoid.CoprodI.Word.instDecidableEq_1 = Monoid.CoprodI.Word.equiv.decidableEq
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
concatenation, and thus provides a useful induction principle.
- singleton: {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i : ι} → (x : M i) → x ≠ 1 → Monoid.CoprodI.NeWord M i i
- append: {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → {i j k l : ι} → Monoid.CoprodI.NeWord M i j → j ≠ k → Monoid.CoprodI.NeWord M k l → Monoid.CoprodI.NeWord M i l
Instances For
The list represented by a given NeWord
Equations
- (Monoid.CoprodI.NeWord.singleton x_3 a).toList = [⟨x, x_3⟩]
- (w₁.append _hne w₂).toList = w₁.toList ++ w₂.toList
Instances For
The first letter of a NeWord
Equations
- (Monoid.CoprodI.NeWord.singleton x_3 a).head = x_3
- (w₁.append _hne w₂).head = w₁.head
Instances For
The last letter of a NeWord
Equations
- (Monoid.CoprodI.NeWord.singleton x_3 a).last = x_3
- (w₁.append _hne w₂).last = w₂.last
Instances For
The Word M
represented by a NeWord M i j
Equations
- w.toWord = { toList := w.toList, ne_one := ⋯, chain_ne := ⋯ }
Instances For
A non-empty reduced word determines an element of the free product, given by multiplication.
Equations
- w.prod = w.toWord.prod
Instances For
One can replace the first letter in a non-empty reduced word by an element of the same group
Equations
- Monoid.CoprodI.NeWord.replaceHead x_1 x_2 (Monoid.CoprodI.NeWord.singleton x_7 a) = Monoid.CoprodI.NeWord.singleton x_1 x_2
- Monoid.CoprodI.NeWord.replaceHead x_2 x_3 (w₁.append hne w₂) = (Monoid.CoprodI.NeWord.replaceHead x_2 x_3 w₁).append hne w₂
Instances For
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
- w.mulHead x hnotone = Monoid.CoprodI.NeWord.replaceHead (x * w.head) hnotone w
Instances For
The inverse of a non-empty reduced word
Equations
- (Monoid.CoprodI.NeWord.singleton x_4 h).inv = Monoid.CoprodI.NeWord.singleton x_4⁻¹ ⋯
- (w₁.append h w₂).inv = w₂.inv.append ⋯ w₁.inv
Instances For
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.
Given a family of free groups with distinguished bases, then their free product is free, with a basis given by the union of the bases of the components.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The free product of free groups is itself a free group.
Equations
- ⋯ = ⋯
A free group is a free product of copies of the free_group over one generator.
Equations
- freeGroupEquivCoprodI = (FreeGroup.lift fun (i : ι) => Monoid.CoprodI.of (FreeGroup.of ())).toMulEquiv (Monoid.CoprodI.lift fun (i : ι) => FreeGroup.lift fun (x : Unit) => FreeGroup.of i) ⋯ ⋯
Instances For
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.