Section 3 : An introduction to group theory

Overview of the sheets

Lean has a bunch of group theory already (Sylow’s theorems, nilpotent and solvable groups and other “final year undergraduate level mathematics”). Should we use what is already there, or rebuild from scratch?

In section 3 of the course repository we study groups (in sheets 1 and 2), subgroups (in sheet 3) and group homomorphisms (in sheet 4). The approach we take is the following. In sheets 1 and 2 we make some basic group theory from scratch. In sheet 3 we dump our development and go back to Lean’s groups, but develop the theory of subgroups of a group from scratch. And finally in sheet 4 we dump our theory of subgroups and use Lean’s subgroups, but develop the theory of group homomorphisms from scratch.

Structures and classes

Groups, subgroups, and group homomorphisms in Lean are all encoded via inductive types. These inductive types are of a particular boring nature: they only have one constructor. Thus in contrast to P ∨ Q, which can be proved in two ways (you either prove P or you prove Q), there is only one way to make a subgroup of a group: you have to give a subset of the group, plus proofs that it satisfies the axioms of a subgroup. You can read about the details of structures and classes by following those links; I will not say any more about them here.

What you need to know to do sheets 1 and 2

There will be a lot of rw involved, because we are constantly using the group axioms. Lean’s simplifier simp is introduced in sheet 1; don’t forget to experiment with it. It will do multiple rewrites in one go. As the sheet goes on, the simplifier gets smarter because we tag more and more lemmas with the @[simp] attribute.

Sheet 2 is perhaps mathematically tricky.

What you need to know to do sheet 3

Although you don’t need it, the convert tactic can be useful at times. Otherwise it’s just a case of keeping your head, and using intro, apply and rw.

The ext tactic can be used to prove that two subgroups are equal.

What you need to know to do sheet 4

The ext tactic can be used to prove that two functions are equal.