Formalization: Gardam's disproof of the Kaplansky Unit Conjecture
This folder contains the formalization of the disproof of the Kaplansky Unit Conjecture by Giles Gardam in a paper in the Annals of Mathematics. Here is an outline of the code:
You can also browse the docs in the folder build/doc/
(if these are not present they can be generated by lake build -Kdoc=on UnitConjecture:docs
). The best way to view these is to run a static web server, for example to run python3 -m http.server
from the build/docs
directory. A good starting point is the file UnitConjecture.html
.
The Proof
Gardam proved that for a group P
(the Promislow or Hantzsche–Wendt group), we have the following (all files mentioned are in the folder UnitConjecture
):
P
is torsion free; this is proved inTorsionFree.lean
P
has non-trivial units; this is proved inGardamTheorem.lean
The rest of the code is required to construct
Constructing the group P
The group P
is a so called Metabelian Group, an extension of an abelian group by an abelian group.
- In the file
GardamGroup.lean
, the specific construction ofP
is given using the general construction of Metabelian groups. - In the file
MetabelianGroup.lean
, Metabelian Groups are constructed based on appropriate data, and proved to be groups. - The data for a Metabelian group includes a group action and a cocycle. These are defined and their basic properties proved in
Cocycle.lean
.
Constructing group rings
A group ring
- Free modules are constructed in
FreeModule.lean
with properties proved. This crucially includes decidable equality of elements, assuming decidable equality forand . - The Group Ring structure is defined in
GroupRing.lean
and shown to give a ring.
Proofs and Definitions by Computation and Enumeration
We set things up to use typeclasses to deduce decidable equality, both by finite enumeration and by checking equality on a basis for finitely generated abelian groups.
- In
EnumDecide.lean
we set up the typeclasses for deducing decidable equality, and prove the basic cases. - In
AddFreeGroup.lean
we define bases of free abelian groups via a universal property, show that products ofhave bases, show that homormorphisms can be defined by giving functions on a basis, and show that we have decidable equality for homomorphisms on finitely generated free abelian groups.