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

ink

def trivialElem {R : Type} {X : Type} [inst : Ring R] [inst : DecidableEq X] (a : R[X]) : Prop

The definition of an element of a free module being trivial, i.e., of the form k•x for x : X and k ≠ 0.

Equations

• trivialElem a = ∃! x, FreeModule.coordinates x a ≠ 0

ink

def 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

• UnitConjecture = ∀ {F : Type} [inst : Field F] [inst_1 : DecidableEq F] {G : Type} [inst_2 : Group G] [inst_3 : DecidableEq G] [inst_4 : TorsionFree G] (u : (F[G])ˣ), trivialElem ↑u

ink

@[inline]

abbrev 𝔽₂ : Type

The finite field on two elements.

Equations

• 𝔽₂ = Fin 2

ink

instance instField𝔽₂ : Field 𝔽₂

Equations

• instField𝔽₂ = Field.mk zpowRec instField𝔽₂.proof_7 instField𝔽₂.proof_8 (qsmulRec Rat.castRec)

ink

instance ringElem : Coe P (𝔽₂[P])

Equations

• ringElem = { coe := fun g => Quotient.mk (formalSumSetoid 𝔽₂ P) [(1, g)] }

The main constants of the group P.

ink

@[inline]

abbrev P.x : P

Equations

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

ink

@[inline]

abbrev P.y : P

Equations

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

ink

@[inline]

abbrev P.z : P

Equations

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

ink

@[inline]

abbrev P.a : P

Equations

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

ink

@[inline]

abbrev P.b : P

Equations

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

The components of the non-trivial unit α.

ink

def Gardam.p : 𝔽₂[P]

Equations

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

ink

def Gardam.q : 𝔽₂[P]

Equations

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

ink

def Gardam.r : 𝔽₂[P]

Equations

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

ink

def Gardam.s : 𝔽₂[P]

Equations

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

ink

def Gardam.α : 𝔽₂[P]

The non-trivial unit α.

Equations

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

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

ink

def Gardam.p' : 𝔽₂[P]

Equations

• Gardam.p' = Quotient.mk (formalSumSetoid 𝔽₂ P) [(1, P.x⁻¹)] * (Quotient.mk (formalSumSetoid 𝔽₂ P) [(1, P.a⁻¹)] * Gardam.p * Quotient.mk (formalSumSetoid 𝔽₂ P) [(1, P.a)])

ink

def Gardam.q' : 𝔽₂[P]

Equations

• Gardam.q' = -(Quotient.mk (formalSumSetoid 𝔽₂ P) [(1, P.x⁻¹)] * Gardam.q)

ink

def Gardam.r' : 𝔽₂[P]

Equations

• Gardam.r' = -(Quotient.mk (formalSumSetoid 𝔽₂ P) [(1, P.y⁻¹)] * Gardam.r)

ink

def Gardam.s' : 𝔽₂[P]

Equations

• Gardam.s' = Quotient.mk (formalSumSetoid 𝔽₂ P) [(1, P.z⁻¹)] * (Quotient.mk (formalSumSetoid 𝔽₂ P) [(1, P.a⁻¹)] * Gardam.s * Quotient.mk (formalSumSetoid 𝔽₂ P) [(1, P.a)])

ink

def 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.

ink

theorem Gardam.α_nonTrivial : ¬trivialElem Gardam.α

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.

ink

def Gardam.Counterexample : { u // ¬trivialElem ↑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.

ink

theorem Gardam.GardamTheorem : ¬UnitConjecture

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