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

@[instance_reducible]

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

Equations

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

@[instance_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)

@[reducible, inline]

abbrev LeanPool.Polylean.Gardam.groupRingOf (g : P) : 𝔽₂[P]

Embed a group element as the corresponding basis element of 𝔽₂[P].

Equations

• LeanPool.Polylean.Gardam.groupRingOf g = ⟦[(1, g)]⟧

@[reducible, inline]

abbrev LeanPool.Polylean.Gardam.ringMul (u v : 𝔽₂[P]) : 𝔽₂[P]

The group-ring multiplication, made explicit to avoid the monomial HMul R G notation.

Equations

• LeanPool.Polylean.Gardam.ringMul u v = LeanPool.Polylean.GroupRing.mul u v

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. Coefficients are combined before comparison so that checking equality does not repeatedly scan the full uncollected product.

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

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

theorem LeanPool.Polylean.Gardam.α'_mul_α : 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] [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] [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.