Kaplansky's Conjectures

zero_divisor_conjecturetheorem

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

theorem zero_divisor_conjecture : NoZeroDivisors (MonoidAlgebra K G) := by
  sorry

idempotent_conjecturetheorem

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

theorem idempotent_conjecture (a : MonoidAlgebra K G) (h : IsIdempotentElem a) :
    a = 0 ∨ a = 1 := by
  sorry

IsTrivialUnitdef

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

def IsTrivialUnit (u : MonoidAlgebra K G) : Prop :=
  ∃ (k : Kˣ) (g : G), u = MonoidAlgebra.single g (k : K)

isUnitlemma

lemma IsTrivialUnit.isUnit {u : MonoidAlgebra K G} (h : IsTrivialUnit u) : IsUnit u := by
  obtain ⟨k, g, rfl⟩ := h
  exact (Prod.isUnit_iff (x := (k.1, g)).mpr ⟨k.isUnit, Group.isUnit g⟩).map MonoidAlgebra.singleHom

PromislowGroupabbrev

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

abbrev PromislowGroup : Type :=
  letI a := FreeGroup.of (0 : Fin 2)
  letI b := FreeGroup.of (1 : Fin 2)
  PresentedGroup {b⁻¹ * a * a * b * a * a, a⁻¹ * b * b * a * b * b}

promislow_group_is_torsionfreelemma

The Promislow group is torsion-free.

lemma promislow_group_is_torsionfree :
    IsMulTorsionFree PromislowGroup := by
  sorry

itheorem

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

theorem UnitConjecture.counterexamples.i (p : ℕ) [hp : Fact p.Prime] :
    ∃ (u : (MonoidAlgebra (ZMod p) PromislowGroup)ˣ), ¬IsTrivialUnit u.val := by
  sorry

iitheorem

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

theorem UnitConjecture.counterexamples.ii :
    ∃ (u : (MonoidAlgebra ℂ PromislowGroup)ˣ), ¬IsTrivialUnit u.val := by
  sorry

counter_unit_conjecturetheorem

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 counter_unit_conjecture :
    ∃ (G : Type) (_ : Group G) (_ : IsMulTorsionFree G),
    ∀ (p : ℕ) (_ : p = 0 ∨ p.Prime),
    ∃ (K : Type) (_ : Field K) (_ :  CharP K p) (u : (MonoidAlgebra K G)ˣ), ¬IsTrivialUnit u.val :=
  ⟨PromislowGroup, _, promislow_group_is_torsionfree, fun p hp ↦
    hp.by_cases (by rintro rfl; exact ⟨ℂ, _, inferInstance, UnitConjecture.counterexamples.ii⟩)
      fun h ↦ have := Fact.mk h; ⟨ZMod p, _, inferInstance, UnitConjecture.counterexamples.i p⟩⟩

counter_unit_conjecture_weaktheorem

There is a counterexample to Unit Conjecture in any characteristic.

theorem counter_unit_conjecture_weak (p : ℕ) (hp : p = 0 ∨ p.Prime) :
    ∃ (G : Type) (_ : Group G) (_ : IsMulTorsionFree G)
      (K : Type) (_ : Field K) (_ :  CharP K p) (u : (MonoidAlgebra K G)ˣ), ¬IsTrivialUnit u.val :=
  have ⟨G, _, _, hG⟩ := counter_unit_conjecture
  ⟨G, _, ‹_›, hG p hp⟩

goaldef

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

def goal : Prop :=
  NoZeroDivisors (MonoidAlgebra K G)

import Conjectura.Problems.WP0020.Statement · maintainer — open · raw source

Adapted for Conjectura from formal-conjectures (Google DeepMind), `Wikipedia/Kaplansky.lean`. The problem is catalogued at https://en.wikipedia.org/wiki/Kaplansky%27s_conjectures. LOCKED: solvers cannot modify this file.

Copyright (c) 2025 The Formal Conjectures Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Formal Conjectures Authors

Full credits