## 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 in`TorsionFree.lean`

`P`

has non-trivial units; this is proved in`GardamTheorem.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 of`P`

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.