Coproduct (free product) of two monoids or groups #

In this file we define Monoid.Coprod M N (notation: M ∗ N) to be the coproduct (a.k.a. free product) of two monoids. The same type is used for the coproduct of two monoids and for the coproduct of two groups.

The coproduct M ∗ N has the following universal property: for any monoid P and homomorphisms f : M →* P, g : N →* P, there exists a unique homomorphism fg : M ∗ N →* P such that fg ∘ Monoid.Coprod.inl = f and fg ∘ Monoid.Coprod.inr = g, where Monoid.Coprod.inl : M →* M ∗ N and Monoid.Coprod.inr : N →* M ∗ N are canonical embeddings. This homomorphism fg is given by Monoid.Coprod.lift f g.

We also define some homomorphisms and isomorphisms about M ∗ N, and provide additive versions of all definitions and theorems.

Main definitions #

Types #

Monoid.Coprod M N (a.k.a. M ∗ N): the free product (a.k.a. coproduct) of two monoids M and N.
AddMonoid.Coprod M N (no notation): the additive version of Monoid.Coprod.

In other sections, we only list multiplicative definitions.

Instances #

MulOneClass, Monoid, and Group structures on the coproduct M ∗ N.

Monoid homomorphisms #

Monoid.Coprod.mk: the projection FreeMonoid (M ⊕ N) →* M ∗ N.
Monoid.Coprod.inl, Monoid.Coprod.inr: canonical embeddings M →* M ∗ N and N →* M ∗ N.
Monoid.Coprod.lift: construct a monoid homomorphism M ∗ N →* P from homomorphisms M →* P and N →* P; see also Monoid.Coprod.liftEquiv.
Monoid.Coprod.clift: a constructor for homomorphisms M ∗ N →* P that allows the user to control the computational behavior.
Monoid.Coprod.map: combine two homomorphisms f : M →* N and g : M' →* N' into M ∗ M' →* N ∗ N'.
Monoid.Coprod.swap: the natural homomorphism M ∗ N →* N ∗ M.
Monoid.Coprod.fst, Monoid.Coprod.snd, and Monoid.Coprod.toProd: natural projections M ∗ N →* M, M ∗ N →* N, and M ∗ N →* M × N.

Monoid isomorphisms #

MulEquiv.coprodCongr: a MulEquiv version of Monoid.Coprod.map.
MulEquiv.coprodComm: a MulEquiv version of Monoid.Coprod.swap.
MulEquiv.coprodAssoc: associativity of the coproduct.
MulEquiv.coprodPUnit, MulEquiv.punitCoprod: free product by PUnit on the left or on the right is isomorphic to the original monoid.

Main results #

The universal property of the coproduct is given by the definition Monoid.Coprod.lift and the lemma Monoid.Coprod.lift_unique.

We also prove a slightly more general extensionality lemma Monoid.Coprod.hom_ext for homomorphisms M ∗ N →* P and prove lots of basic lemmas like Monoid.Coprod.fst_comp_inl.

Implementation details #

The definition of the coproduct of an indexed family of monoids is formalized in Monoid.CoprodI. While mathematically M ∗ N is a particular case of the coproduct of an indexed family of monoids, it is easier to build API from scratch instead of using something like

def Monoid.Coprod M N := Monoid.CoprodI ![M, N]

def Monoid.Coprod M N := Monoid.CoprodI (fun b : Bool => cond b M N)

There are several reasons to build an API from scratch.

API about Con makes it easy to define the required type and prove the universal property, so there is little overhead compared to transferring API from Monoid.CoprodI.
If M and N live in different universes, then the definition has to add ULifts; this makes it harder to transfer API and definitions.
As of now, we have no way to automatically build an instance of (k : Fin 2) → Monoid (![M, N] k) from [Monoid M] and [Monoid N], not even speaking about more advanced typeclass assumptions that involve both M and N.
Using a list of M ⊕ N instead of, e.g., a list of Σ k : Fin 2, ![M, N] k as the underlying type makes it possible to write computationally effective code (though this point is not tested yet).

TODO #

Prove Monoid.CoprodI (f : Fin 2 → Type*) ≃* f 0 ∗ f 1 and Monoid.CoprodI (f : Bool → Type*) ≃* f false ∗ f true.

Tags #

group, monoid, coproduct, free product