Kaplansky's Conjectures

Reference: Wikipedia

theorem Kaplansky.zero_divisor_conjecture (K : Type u_1) [Field K] (G : Type u_2) [Group G] (hG : Monoid.IsTorsionFree G) : NoZeroDivisors (MonoidAlgebra K G)

The zero-divisor conjecture

If G is torsion-free, then the group algebra K[G] has no non-trivial zero divisors.

theorem Kaplansky.idempotent_conjecture (K : Type u_1) [Field K] (G : Type u_2) [Group G] (hG : Monoid.IsTorsionFree G) (a : MonoidAlgebra K G) (h : IsIdempotentElem a) : a = 0 ∨ a = 1

The idempotent conjecture

If G is torsion-free, then K[G] has no non-trivial idempotents.

def Kaplansky.IsTrivialUnit {K : Type u_1} [Field K] {G : Type u_2} (u : MonoidAlgebra K G) : Prop

A unit in K[G] is trivial if it is exactly of the form kg where:

• k is a unit in the base field K
• g is an element of the group G

Equations

• Kaplansky.IsTrivialUnit u = ∃ (k : Kˣ) (g : G), u = MonoidAlgebra.single g ↑k

theorem Kaplansky.IsTrivialUnit.isUnit (K : Type u_1) [Field K] (G : Type u_2) [Group G] {u : MonoidAlgebra K G} (h : IsTrivialUnit u) : IsUnit u

Counterexamples

@[reducible, inline]

abbrev Kaplansky.PromislowGroup : Type

The Promislow group ⟨ a, b | b⁻¹a²ba², a⁻¹b²ab² ⟩

Equations

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

theorem Kaplansky.promislow_group_is_torsionfree : Monoid.IsTorsionFree PromislowGroup

The Promislow group is torsion-free.

theorem Kaplansky.UnitConjecture.counterexamples.i (p : ℕ) [hp : Fact (Nat.Prime p)] : ∃ (u : (MonoidAlgebra (ZMod p) PromislowGroup)ˣ), ¬IsTrivialUnit ↑u

If $P$ is the Promislow group, then the group ring $\mathbb{F}_p[P]$ has a non-trivial unit.

theorem Kaplansky.UnitConjecture.counterexamples.ii : ∃ (u : (MonoidAlgebra ℂ PromislowGroup)ˣ), ¬IsTrivialUnit ↑u

If $P$ is the Promislow group, then the group ring $\mathbb{C}[P]$ has a non-trivial unit.

theorem Kaplansky.counter_unit_conjecture : ∃ (G : Type) (x : Group G) (_ : Monoid.IsTorsionFree G), ∀ (p : ℕ), p = 0 ∨ Nat.Prime p → ∃ (K : Type) (x_3 : Field K) (_ : CharP K p) (u : (MonoidAlgebra K G)ˣ), ¬IsTrivialUnit ↑u

The Unit Conjecture is false.

At least there is a counterexample for any prime and zero characteristic: [Mu21] Murray, A. (2021). More Counterexamples to the Unit Conjecture for Group Rings. [Pa21] Passman, D. (2021). On the counterexamples to the unit conjecture for group rings. [Ga24] Gardam, G. (2024). Non-trivial units of complex group rings.

theorem Kaplansky.counter_unit_conjecture_weak (p : ℕ) (hp : p = 0 ∨ Nat.Prime p) : ∃ (G : Type) (x : Group G) (_ : Monoid.IsTorsionFree G) (K : Type) (x_2 : Field K) (_ : CharP K p) (u : (MonoidAlgebra K G)ˣ), ¬IsTrivialUnit ↑u

There is a counterexample to Unit Conjecture in any characteristic.