Posted Thursday December 28 2023.

There are a few ways to define a monoid in Lean4. One way would be to use the official Mathlib4 definition. Alternatively, we can just write a new definition ourselves:```
structure Monoid where
element : Type
op : element -> element -> element
identity : element
identity_left : forall x: element, op identity x = x
identity_right : forall x: element, op x identity = x
associativity : forall x y z: element, op x (op y z) = op (op x y) z
```

The above code defines a new type called `Monoid`

. In order to construct a term of this type, you need to provide the six fields listed.

`element`

is some type. Lean has a lot of builtin types, such as integers or natural numbers. You could also pass a custom type here.`op`

is a function that takes two terms of type`element`

and returns a result, another term of type`element`

. In other words, it is a binary operation on`element`

.`identity`

is some specific term of type`element`

- the remaining three,
`identity_left`

,`identity_right`

, and`associativity`

are*propositions*.

Thus, in order to construct a term of type `Monoid`

, you not only need to provide an underlying set of elements and a binary operation with an identity, you also need to present *proofs* of the corresponding propositions that they satisfy the conditions of a monoid.

`Nat`

. Lean4 also comes with the builtin function `Nat.add`

which has type `Nat -> Nat -> Nat`

, which is exactly what we want for the binary operation, and `Nat.zero`

, which is a term of type `Nat`

.
```
example: Monoid := {
element := Nat
op := Nat.add
identity := Nat.zero
identity_left := by {intros; rw [Nat.add_eq, Nat.zero_eq, Nat.zero_add]},
identity_right := by {intros; rw [Nat.add_eq, Nat.zero_eq, Nat.add_zero]},
associativity := by {intros; rw [Nat.add_eq, Nat.add_eq, Nat.add_eq, Nat.add_eq, Nat.add_assoc]}
}
```

The identity and associativity proofs are a little convoluted, and in truth I just found them via trial and error in an interactive prover. But it should not be surprising they are short proofs, because the fact that the natural numbers form a monoid under addition is one of their fundamental properties.

As another example, we could also define the monoid of natural numbers with`element`

field will be the same, but the operation will be `Nat.mul`

and the identity is 1 instead of 0. There is no `Nat.one`

, instead we can write `Nat.succ Nat.zero`

, which is the application of `Nat.succ`

, a function, to `Nat.zero`

, an element. In English - the successor of zero. (We could also simply write `1`

but this would involve type inference.)
```
example: Monoid := {
element := Nat
op := Nat.mul
identity := Nat.succ Nat.zero
identity_left := by {intros; rw [Nat.mul_eq, Nat.one_mul]},
identity_right := by {intros; rw [Nat.mul_eq, Nat.mul_one]},
associativity := by {intros; rw [Nat.mul_eq, Nat.mul_eq, Nat.mul_eq, Nat.mul_eq, Nat.mul_assoc]}
}
```

For many algebraic objects, you want to look at *structure-preserving maps* between them. For monoids, these are called *monoid homomorphisms* (they are also sometimes called *monoid morphisms* since they are the morphisms in the category of monoids). In short, a monoid homomorphism is a function between two monoids that “preserves” the binary operation, as well as the identity element.

```
structure Monoid.morphism (M N: Monoid) where
function: M.element -> N.element
identity_preserving: function M.identity = N.identity
operation_preserving: forall x y: M.element, function (M.op x y) = N.op (function x) (function y)
```

This code defines, for any two monoids `M`

and `N`

, a new type `Monoid.morphism M N`

, the type of monoid homomorphisms from M to N. To construct a term of this type, you need to provide the function between the underlying element types as well as proofs it is identity- and operation-preserving.

`M`

, the identity morphism from `M`

to itself.
```
def Monoid.morphism.id (M: Monoid): Monoid.morphism M M := {
function := fun x => x,
identity_preserving := by simp,
operation_preserving := by simp
}
```

Note that the input type is `Monoid`

, while the output type is a `Monoid.morphism M M`

. The type of the output depends on the input value - that’s a dependent type!

Luckily the proofs of structure-preserving-ness were simple enough that Lean could handle them “by simp”.

We can also define the composition of two monoid morphisms:```
def Monoid.morphism.comp (f: Monoid.morphism M1 M2) (g: Monoid.morphism M2 M3): Monoid.morphism M1 M3 := {
function := fun x => g.function (f.function x),
identity_preserving := by {simp; rw [f.identity_preserving, g.identity_preserving]}
operation_preserving := by {intros; simp; rw [f.operation_preserving, g.operation_preserving]}
}
```

This definition takes as input two monoid homomorphisms from M1 to M2 and from M2 to M3 and returns a monoid homomorphism from M1 to M3. Note that the types of `M1, M2, M3`

are actually implicit in the definition. It would be more verbose to explicitly introduce them, but Lean4 allows this shorthand.

**TODO**: some interesting theorem to cap off this post.