Invertible elements in a monoid

HEGL Illustrating Mathematics Seminar
Winter Semester 2024-2025

Florent Schaffhauser
Heidelberg University

Invertible elements

• The notion of invertible element in a monoid is used in various of the projects in our seminar.
• Recall that, if is a monoid, then a term is said to be invertible if there exists a term such that .
• The example to keep in mind is the underlying multiplicative monoid of a ring , for instance , or .
• How do we implement this? We have to be careful with:
  • the notion of monoid.
  • the existential quantifier in the notion of invertible element.

Monoids

• What does it mean to say that is a monoid?
• It means that is a set and is an operation on (Verknüpfung).
• It also means that is associative and that is a neutral element for .
  • .
  • .
• So a monoid is really a quintuple It can be implemented in Lean using structure, with five fields. Note that and are properties (terms whose type is a proposition).

Property versus data

We can also separate property from data and implement first the type of pointed magmas, whose terms are triples , using a structure with three fields.

structure PtdMagma where
  carrier  : Type
  op       : carrier → carrier → carrier
  neut_elt : carrier

In this approach, we could implement the properties of pointed magmas using type classes, so that we can instantiate them on concrete types. We probably will not need to implement monoids in this way.

Groups

• A group should be a pair where is a monoid and inv is a proof of the proposition .
• We prove by equational reasoning that the in the proposition is unique:

• If we denote that element by , this defines a function .

Group implementation

Due to the previous remark, a group is often implemented in the following way.

structure Group where
  M   : Monoid
  ι   : M.carrier → M.carrier
  inv : ∀ x : M.carrier, μ x (ι x) = M.elt ∧ μ (ι x) x = M.neut_elt

Note that this implementation does not include an existential quantifier, but carries more data (namely, the map ι : M.carrier → M.carrier).

Group of invertible elements

• In a monoid , a term is called invertible if there exists a term such that .
• This defines a predicate , namely

• We then want to define a group , whose carrier will be the subtype

• It is not too difficult to construct a monoid whose carrier is . However, an issue arises when we wish to define the map .

Submonoid

• If we want to show that there is a submonoid of whose carrier is , we need to prove:
  • that the product of two invertible elements is invertible.
  • that the neutral element is invertible.
• The monoid thus constructed will be the underlying monoid of the group . In order to construct that group, we can:
  • either use the definition of a group that contains an existential quantifier.
  • or modify the implementation of the type , to interpret the existential quantifier there more constructively.

The type of invertible elements

Recall that we can write a monoid under the form . Here is another way to implement the type .

structure InvElts (M : Monoid) where
  elt   : X
  inv   : X
  isInv : μ(elt, inv) = e ∧ μ(inv, elt) = e

Then we can implement the map as follows.

def invMap {M : Monoid} InvElts M → InvElts M :=
  fun ⟨x, y, p⟩ ↦ ⟨y, x, q⟩

where and .

The inverse map

• All you need to do to make the previous definition works is define in terms of , which is proved similarly to !
• Then one can prove that the type , together with the function , indeed define a group .
• If you prefer, you can also introduce the following subtype and turn it into the carrier of .

• The upshot is that is now a subtype of . But it also introduces a layer of complexity in the construction.

Pending tasks

• Making design choices and implementing all of the above would be a great achievement for our seminar.
• If you want to formalise the fact that is a subtype of , you can prove that .
• Then the next task would be to talk about GCDs in a monoid and prove results about them. Maybe next week?