Section 5 : 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 sheet 1 of section 5 we go through a brief tour of how to use Lean’s groups. In sheet 2 we make new “class”es WeakGroup and BadGroup (so now you can guess how to make groups), and show that a WeakGroup is the same as a Group but that there are BadGroup s which aren’t groups. In sheet 3 we give a brief overview of subgroups and group homomorphisms.

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 the sheets

Sheet 1: There will be a lot of rw involved, because we are constantly using the group axioms. Sheet 2 is perhaps mathematically tricky. Sheet 3 is refine and ext and apply practice.