# 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.

Exercise 5: Given $$b \, c : G$$, show that the inverse of $$(b * c)$$ is $$(c^{-1}*b^{-1})$$ in Lean. (Hint: Think about what it means for an element to be an inverse).
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
Exercise 6: Show that the identity element of a group is unique in Lean.
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.