Reservoir

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 , construct group rings, and to prove the required properties.

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 is the free module on with basis elements of a group with a natural ring structure.

• Free modules are constructed in FreeModule.lean with properties proved. This crucially includes decidable equality of elements, assuming decidable equality for and .
• 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 of have 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.