Groups I

Note: To follow along with this post create a new Lean file and write the following at the top of your Lean file. If you do not have a copy of Lean installed you can follow along here (but it will run slower).

import algebra.group
import tactic

variables (G : Type*) [group G]

Groups are algebraic objects, and it is the study of these objects that forms an important part of abstract algebra, Group Theory. Before we see the definition of a group we must first familiarise ourselves with composition laws (also known as binary operations). Addition and multiplication on the integers \(\mathbb{Z}\) are examples of composition laws. They are essentially operations that take two elements of a set and combine them to make a third element.

Definition 1: Composition Law/Binary Operation

A composition law \(*\) on a set X is a rule assigning to \(a : X\) and \(b : X\) an element \(a * b : X\).

Exercise 1: Give another example of a composition law on the integers.

Is subtraction a composition law on the natural numbers \(\mathbb{N}\)? If we consider the natural numbers 3 and 7 we see that 3 – 7 = -4 which is not a natural number, so subtraction is not a composition law on \(\mathbb{N}\). Subtraction is however a composition law on the integers \(\mathbb{Z}\).

We are familiar with the following property of multiplication: \(a \times b = b \times a\). We generalize this notion with the following definition:

Definition 2: Commutativity

A composition law \(*\) on a set X is commutative if \(\forall a \,b : X\) we have that \(a * b = b * a\).

Note: a composition law is commutative if the order doesn’t matter.

Exercise 2:

1. Is addition on the natural numbers \(\mathbb{N}\) commutative?
2. Is subtraction on the integers \(\mathbb{Z}\) commutative?

We are also familiar with the fact that among the integers (a + b) + c = a + (b + c), as before we generalize this with the following definition:

Definition 3: Associativity

A composition law \(*\) on a set X is associative if \(\forall a\, b\, c : X\) we have that \((a*b)*c=a*(b*c)\).

Example 1: Addition is associative on the integers \(\mathbb{Z}\) because \(\forall a\, b\, c : \mathbb{Z}\) we have that \((a+b)+c = a+(b+c)\).

Example 2: Subtraction is not associative on the integers. Examine the following counter example \((3-7)-5=-9\) but \(3-(7-5)=1\) and clearly \(-9 \neq 1\).

Exercise 3: Is function composition associative?

Definition 4: Group

A pair \((G, *)\), where G is a non-empty set and \((*)\) is a composition law, is a group if:

• \((*)\) is associative: \(\forall a\, b \,c : G \,, (a*b)*c=a*(b*c)\).
• \((*)\) admits a neutral element: \(\exists 1_{G}, \,, \forall a : G, a*1_{G}=1_{G}*a=a\).
• Every element of G has an inverse element in G: \(\forall a : G, \exists a^{-1} : G, a * a^{-1} = a^{-1}*a=1_{G}\).

A group is called abelian if its composition law is commutative.

Here are the group axioms as they appear in mathlib:

#check (mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))
#check (one_mul : ∀ a : G, 1 * a = a)
#check (mul_one : ∀ a : G, a * 1 = a)
#check (mul_left_inv : ∀ a : G, a⁻¹ * a = 1)
#check (mul_right_inv : ∀ a : G, a * a⁻¹ = 1)

Exercise 4:

1. Is \((\mathbb{Z}, +)\) (The set of integers endowed with addition) a group? If so what is the neutral element.
2. Is \((\mathbb{Z}, \times)\) (The set of integers endowed with multiplication) a group? If so what is the neutral element.

Example 1: Given that \((G, *)\) is a group and \(a : G\), show that \(a * a = a \leftrightarrow a = 1_{G}\). (i.e if a * a = a then a is the neutral element of the group).

We first prove the → direction, let \(a : G\) then \((a*a)*a^{-1}=a*a^{-1}\) from which we see that \(a*(a*a^{-1})=a*a^{-1}\) which clearly reduces to \(a*1_{G}=1_{G}\) giving the required result \(a = 1_{G}\).

Conversely suppose that \(a = 1_{G}\) then \(a * a = 1_{G} * a = a\).

example (a : G) : a * a = a ↔ a = 1 :=
begin
  split,--spliting the ↔
  {--proving the → direction
  intro h₁, --implication introduction
  rw ← mul_right_inv a, -- using a * a⁻¹ = 1
  nth_rewrite 1 ← h₁, --using the hypothesis a = a * a
  --"nth_rewrite n" tells lean to only rewrite the nth a
  rw mul_assoc, -- using associativity: a * b * c = a * (b * c)
  rw mul_right_inv, -- using a * a⁻¹ = 1
  rw mul_one, --using a * 1 = a
  },
  {--proving the ← direction
    intro h₂,--implication introduction
    rw h₂, --using a = 1
    rw mul_one, --using a * 1 = a
  }
end

Note: You can also use the “group” tactic to instantly solve goals like this.

theorem bc_inv (b c : G) : (b * c) * (c⁻¹ * b⁻¹) = 1 :=
begin
  rw mul_assoc, -- using associativity: a * b * c = a * (b * c)
  have h₁ : c * (c⁻¹ * b⁻¹) = b⁻¹, --delaring a hypothesis that we must now prove
  {
   rw ← mul_assoc, -- using associativity: a * (b * c) = a * b * c
   rw mul_right_inv, -- using a * a⁻¹ = 1
   rw one_mul, --using 1 * a = a
  },
  rw h₁, -- using the hypothesis we just proved
  rw mul_right_inv, -- using a * a⁻¹ = 1
end

Tip: You can click on the exercise to view a solution.

We will now prove that the inverse of an element of a group is unique. We will do this by supposing that there are two such inverses and then showing that they must be equal.

Theorem 1: Let \((G, *)\) be a group and \(a \, b \, c : G\) such that \(h_{1} : a * b= 1_{G}\) and \(h_{2} : a * c = 1_{G}\) then we have \(b = c\).

Proof: Using \(h_{1}\) and \(h_{2}\) we see that \(a * b = a * c\) from which we can easily deduce that \(b = c\) as required.

QED

theorem unique_inv (a b c : G) (h₁ : a * b = 1) (h₂ : a * c = 1) : b = c :=
begin
rw ← h₁ at h₂,
rw mul_right_inj a at h₂,
rw eq.symm h₂,
end

theorem unique_id (a b c : G) (h₁ : a * b = a) (h₂ : a * c = a) : b = c:=
begin
nth_rewrite 1 ← h₁ at h₂,
rw mul_right_inj a at h₂,
rw eq.symm h₂,
end

Notation: There are a few common systems of notation that we use with groups.

You may have noticed that under our imports we had the line

variables (G : Type*) [group G]

This essentially is us telling lean “Let G be a group in multiplicative notation”, and so now we can freely use G in our theorem, lemmas and examples as we have done in this post.