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.
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
fg ∘ Monoid.Coprod.inl = f and
fg ∘ Monoid.Coprod.inr = g,
Monoid.Coprod.inl : M →* M ∗ N
Monoid.Coprod.inr : N →* M ∗ N are canonical embeddings.
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 #
Monoid.Coprod M N(a.k.a.
M ∗ N): the free product (a.k.a. coproduct) of two monoids
AddMonoid.Coprod M N(no notation): the additive version of
In other sections, we only list multiplicative definitions.
Monoid homomorphisms #
Monoid.Coprod.clift: a constructor for homomorphisms
M ∗ N →* Pthat allows the user to control the computational behavior.
Monoid.Coprod.map: combine two homomorphisms
f : M →* Nand
g : M' →* N'into
M ∗ M' →* N ∗ N'.
Monoid.Coprod.swap: the natural homomorphism
M ∗ N →* N ∗ M.
Monoid isomorphisms #
MulEquiv.coprodAssoc: associativity of the coproduct.
MulEquiv.punitCoprod: free product by
PUniton the left or on the right is isomorphic to the original monoid.
Main results #
Implementation details #
The definition of the coproduct of an indexed family of monoids is formalized in
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
Conmakes it easy to define the required type and prove the universal property, so there is little overhead compared to transferring API from
Nlive 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 N], not even speaking about more advanced typeclass assumptions that involve both
- Using a list of
M ⊕ Ninstead of, e.g., a list of
Σ k : Fin 2, ![M, N] kas the underlying type makes it possible to write computationally effective code (though this point is not tested yet).
Monoid.CoprodI (f : Fin 2 → Type*) ≃* f 0 ∗ f 1and
Monoid.CoprodI (f : Bool → Type*) ≃* f false ∗ f true.
group, monoid, coproduct, free product
this definition allows a user to provide a custom computational behavior.
Also, it only needs
AddMonoid.Coprod.lift needs an
M ∗ N to
M' ∗ N' by applying
Sum.map f g to each element of the underlying list.
Lift a pair of additive monoid homomorphisms
f : M →+ P,
g : N →+ P
to an additive monoid homomorphism
AddMonoid.Coprod M N →+ P.
Lift a pair of monoid homomorphisms
f : M →* P,
g : N →* P
to a monoid homomorphism
M ∗ N →* P.
Lift two monoid equivalences
e : M ≃* N and
e' : M' ≃* N' to a monoid equivalence
(M ∗ M') ≃* (N ∗ N').