module Algebra.Monoid where

# Monoidsπ

A **monoid** is a semigroup equipped with a
*two-sided identity* element: An element
$eβM$
such that
$eβx=x=xβe.$
For any particular choice of binary operator
$β,$
if a two-sided identity exists, then it is unique; In this sense, βbeing
a monoidβ could be considered an βaxiomβ that semigroups may
satisfy.

However, since semigroup homomorphisms do not automatically preserve
the identity element^{1}, it is part of the type signature
for `is-monoid`

, being considered
*structure* that a semigroup may be equipped with.

record is-monoid (id : A) (_β_ : A β A β A) : Type (level-of A) where field has-is-semigroup : is-semigroup _β_ open is-semigroup has-is-semigroup public field idl : {x : A} β id β x β‘ x idr : {x : A} β x β id β‘ x open is-monoid

The condition of
$(A,0,β)$
defining a monoid is a proposition, so that we may safely decompose
monoids as the *structure*
$(0,β),$
which has to satisfy the *property* of being a monoid.

private unquoteDecl eqv = declare-record-iso eqv (quote is-monoid) instance H-Level-is-monoid : β {id : A} {_β_ : A β A β A} {n} β H-Level (is-monoid id _β_) (suc n) H-Level-is-monoid = prop-instance Ξ» x β let open is-monoid x in Isoβis-hlevel! 1 eqv x

A `monoid structure on`

a type is
given by the choice of identity element, the choice of binary operation,
and the witness that these choices form a monoid. A `Monoid`

, then, is a `type with`

a monoid structure.

record Monoid-on (A : Type β) : Type β where field identity : A _β_ : A β A β A has-is-monoid : is-monoid identity _β_ open is-monoid has-is-monoid public Monoid : (β : Level) β Type (lsuc β) Monoid β = Ξ£ (Type β) Monoid-on open Monoid-on

There is also a predicate which witnesses when an equivalence between monoids is a monoid homomorphism. It has to preserve the identity, and commute with the multiplication:

record Monoid-hom {β β'} {A : Type β} {B : Type β'} (s : Monoid-on A) (t : Monoid-on B) (e : A β B) : Type (β β β') where private module A = Monoid-on s module B = Monoid-on t field pres-id : e A.identity β‘ B.identity pres-β : (x y : A) β e (x A.β y) β‘ e x B.β e y open Monoid-hom Monoidβ : (A B : Monoid β) (e : A .fst β B .fst) β Type _ Monoidβ A B (e , _) = Monoid-hom (A .snd) (B .snd) e

# Relationships to unital magmasπ

open import Algebra.Magma.Unital

By definition, every monoid is exactly a `unital magma`

that is also a `semigroup`

. However, adopting this
as a definition yields several issues especially when it comes to
metaprogramming, which is why this is instead expressed by explicitly
proving the implications between the properties.

First, we show that every monoid is a unital magma:

module _ {id : A} {_β_ : A β A β A} where is-monoidβis-unital-magma : is-monoid id _β_ β is-unital-magma id _β_ is-monoidβis-unital-magma mon .has-is-magma = mon .has-is-semigroup .has-is-magma is-monoidβis-unital-magma mon .idl = mon .idl is-monoidβis-unital-magma mon .idr = mon .idr

βReshufflingβ the record fields also allows us to show the reverse direction, namely, that every unital semigroup is a monoid.

is-unital-magmaβis-semigroupβis-monoid : is-unital-magma id _β_ β is-semigroup _β_ β is-monoid id _β_ is-unital-magmaβis-semigroupβis-monoid uni sem .has-is-semigroup = sem is-unital-magmaβis-semigroupβis-monoid uni sem .idl = uni .idl is-unital-magmaβis-semigroupβis-monoid uni sem .idr = uni .idr

# Inversesπ

A useful application of the monoid laws is in showing that *having
an inverse* is a

*property*of a specific element, not structure on that element. To make this precise: Let $e$ be an element of a monoid, say $(M,1,β);$ If there are $x$ and $y$ such that $xβe=1$ and $eβy=1,$ then $x=y.$

monoid-inverse-unique : β {1M : A} {_β_ : A β A β A} β (m : is-monoid 1M _β_) β (e x y : A) β (x β e β‘ 1M) β (e β y β‘ 1M) β x β‘ y

This is a happy theorem where stating the assumptions takes as many lines as the proof, which is a rather boring calculation. Since $1$ is an identity for $β,$ we can freely multiply by $1$ to βsneak inβ a $y:$

monoid-inverse-unique {1M = 1M} {_β_} m e x y li1 ri2 = x β‘β¨ sym (m .idr) β©β‘ x β β 1M β β‘Λβ¨ apΒ‘ ri2 β©β‘Λ x β (e β y) β‘β¨ m .associative β©β‘ β x β e β β y β‘β¨ ap! li1 β©β‘ 1M β y β‘β¨ m .idl β©β‘ y β

Counterexample: The map $f:(Z,β)β(Z,β)$ which sends everything to zero is a semigroup homomorphism, but does not preserve the unit of $(Z,β).$β©οΈ