Giles Gardam's result

The proof of the theorem 𝔽₂[P] has non-trivial units. Together with the main result of TorsionFree -- that P is torsion-free, this completes the formal proof of Gardam's theorem that Kaplansky's Unit Conjecture is false.

Preliminaries

def LeanPool.Polylean.trivialNonZeroElem {R X : Type} [Ring R] [DecidableEq X] [DecidableEq R] (a : R[X]) : Prop

An element of a free module is trivial but not zero if it is supported on one basis vector.

Equations

• LeanPool.Polylean.trivialNonZeroElem a = ∃! x : X, LeanPool.Polylean.FreeModule.coordinates x a ≠ 0

def LeanPool.Polylean.UnitConjecture : Prop

The statement of Kaplansky's Unit Conjecture: The only units in a group ring, when the group is torsion-free and the ring is a field, are the trivial units.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LeanPool.Polylean.𝔽₂ : Type

The finite field on two elements.

Equations

• LeanPool.Polylean.𝔽₂ = Fin 2

@[implicit_reducible]

instance LeanPool.Polylean.instField𝔽₂ : Field 𝔽₂

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance LeanPool.Polylean.ringElem : Coe P (𝔽₂[P])

Equations

• LeanPool.Polylean.ringElem = { coe := fun (g : LeanPool.Polylean.P) => ⟦[(1, g)]⟧ }

The main constants of the group P.

@[reducible, inline]

abbrev LeanPool.Polylean.P.x : P

The first kernel generator of the Promislow group.

Equations

• LeanPool.Polylean.P.x = (LeanPool.Polylean.K.x, LeanPool.Polylean.Q.e)

@[reducible, inline]

abbrev LeanPool.Polylean.P.y : P

The second kernel generator of the Promislow group.

Equations

• LeanPool.Polylean.P.y = (LeanPool.Polylean.K.y, LeanPool.Polylean.Q.e)

@[reducible, inline]

abbrev LeanPool.Polylean.P.z : P

The third kernel generator of the Promislow group.

Equations

• LeanPool.Polylean.P.z = (LeanPool.Polylean.K.z, LeanPool.Polylean.Q.e)

@[reducible, inline]

abbrev LeanPool.Polylean.P.a : P

The first nontrivial quotient generator of the Promislow group.

Equations

• LeanPool.Polylean.P.a = ((0, 0, 0), LeanPool.Polylean.Q.a)

@[reducible, inline]

abbrev LeanPool.Polylean.P.b : P

The second nontrivial quotient generator of the Promislow group.

Equations

• LeanPool.Polylean.P.b = ((0, 0, 0), LeanPool.Polylean.Q.b)

def LeanPool.Polylean.Gardam.p : 𝔽₂[P]

The p component of Gardam's non-trivial unit α.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Polylean.Gardam.q : 𝔽₂[P]

The q component of Gardam's non-trivial unit α.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Polylean.Gardam.r : 𝔽₂[P]

The r component of Gardam's non-trivial unit α.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Polylean.Gardam.s : 𝔽₂[P]

The s component of Gardam's non-trivial unit α.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Polylean.Gardam.α : 𝔽₂[P]

The non-trivial unit α.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Polylean.Gardam.p' : 𝔽₂[P]

The p' component of the inverse α'.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Polylean.Gardam.q' : 𝔽₂[P]

The q' component of the inverse α'.

Equations

• LeanPool.Polylean.Gardam.q' = -LeanPool.Polylean.Gardam.ringMul✝ (LeanPool.Polylean.Gardam.groupRingOf✝ LeanPool.Polylean.P.x⁻¹) LeanPool.Polylean.Gardam.q

def LeanPool.Polylean.Gardam.r' : 𝔽₂[P]

The r' component of the inverse α'.

Equations

• LeanPool.Polylean.Gardam.r' = -LeanPool.Polylean.Gardam.ringMul✝ (LeanPool.Polylean.Gardam.groupRingOf✝ LeanPool.Polylean.P.y⁻¹) LeanPool.Polylean.Gardam.r

def LeanPool.Polylean.Gardam.s' : 𝔽₂[P]

The s' component of the inverse α'.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Polylean.Gardam.α' : 𝔽₂[P]

The inverse α' of the non-trivial unit α.

Equations

• One or more equations did not get rendered due to their size.

Verification

The main verification of Giles Gardam's result.

theorem LeanPool.Polylean.Gardam.α_nonTrivial : ¬trivialNonZeroElem α

A proof that the unit is non-trivial.

The fact that the counter-example α is in fact a unit of the group ring 𝔽₂[P] is verified by computing the product of α with its inverse α' and checking that the result is (1 : 𝔽₂[P]).

The computational aspects of the group ring implementation and the Metabelian construction are used here.

theorem LeanPool.Polylean.Gardam.α_mul_α' : LeanPool.Polylean.Gardam.ringMul✝ α α' = 1

The product of Gardam's unit and its inverse is one.

theorem LeanPool.Polylean.Gardam.α'_mul_α : LeanPool.Polylean.Gardam.ringMul✝ α' α = 1

The product of Gardam's inverse and its unit is one.

def LeanPool.Polylean.Gardam.Counterexample : { u : (𝔽₂[P])ˣ // ¬trivialNonZeroElem ↑u }

A proof of the existence of a non-trivial unit in 𝔽₂[P].

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Polylean.Gardam.GardamTheorem : ¬UnitConjecture

Giles Gardam's result - Kaplansky's Unit Conjecture is false.

We check that our definition of "trivial but not zero" is correct by showing it equivalent to a more direct definition.

theorem LeanPool.Polylean.trivialNonZeroElem_trivial_nonzeroAux {R G : Type} [Ring R] [Group G] [DecidableEq G] [DecidableEq R] (p : FormalSum R G) : trivialNonZeroElem ⟦p⟧ ↔ ∃ (a : R) (g : G), p ≈ [(a, g)] ∧ a ≠ 0

theorem LeanPool.Polylean.trivialNonZeroElem_trivial_nonzero {R G : Type} [Ring R] [Group G] [DecidableEq G] [DecidableEq R] (p : R[G]) : trivialNonZeroElem p ↔ ∃ (a : R) (g : G), p = a * g ∧ a ≠ 0

Triviality of p : R[G] coincides with the direct definition p = a ⬝ g, a ≠ 0.