Monoids on Lean

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.

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.

For a concrete example, let’s construct the monoid of natural numbers. In this case the type of elements is \(\mathbb{N} = \{0, 1, 2, \cdots\}\). In Lean4, this type is called 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, which is a term of type Nat.
example: Monoid := {
  element := Nat
  op := Nat.add
  identity :=
  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 multiplication as the operation instead - the element field will be the same, but the operation will be Nat.mul and the identity is 1 instead of 0. There is no, instead we can write Nat.succ, which is the application of Nat.succ, a function, to, 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
  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]}

Homomorphisms as dependent types

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.

There seem to be multiple valid ways to define them in Lean. The simplest one seems to be homomorphisms as dependent types - dependent on the source and target monoid. So, here is the definition I wrote:
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.

Now we can define, for any monoid M, the identity morphism from M to itself.
def (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.