Skip to content
Cairn Commons
X Sign in
Level A · Machine-checkable Hard Algebra P-arxiv-math-0703548-farrell-jones-consequences

Algebraic consequences of the Farrell–Jones conjecture

Vanishing of the reduced projective class group for integral group rings. If G is torsion-free, that is, if its only element of finite order is 1, then every finitely generated projective module over ℤ[G] is stably free.

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim.

Start working on it Submit a claim Follow
Cite 
@misc{cairn-arxiv-math-0703548-farrell-jones-consequences,
  title        = {Algebraic consequences of the Farrell–Jones conjecture},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/arxiv-math-0703548-farrell-jones-consequences}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-09-29}
}

Also: CITATION.cff · Atom feed of results

Claims
0
Verified
0
Disputed
0
Refuted
0
On the literature board
0

Current state

No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.

The problem

The question

projective_module_isStablyFree. Vanishing of the reduced projective class group for integral group rings.

If G is torsion-free, that is, if its only element of finite order is 1, then every finitely generated projective module over ℤ[G] is stably free. This is the stable-freeness form of the vanishing of , which is the conclusion of Theorem 0.2 (ii) of [BLR08] for the regular ring . That theorem assumes the K-theoretic Farrell–Jones conjecture for G with coefficients in ℤ.

bass_conjecture_integral_domain. Bass conjecture for commutative integral domains, in idempotent-matrix form.

Let A be an idempotent matrix over R[G]. If the order of g is not invertible in R, then the Hattori–Stallings trace of the projective module represented by A vanishes at the conjugacy class of g. This includes every infinite-order g, whose orderOf is zero. This is Conjecture 0.6 of [BLR08]. By Theorems 0.5 (ii) and 0.7 of [BLR08] it follows from the Farrell–Jones conjecture with coefficients in every field of prime characteristic.

The assembly map in the Farrell–Jones conjecture is not yet available in Mathlib. This file states two of its algebraic consequences using projective modules and matrices over group rings: the vanishing of the reduced projective class group and the Bass conjecture for commutative integral domains.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Arxiv.«math.0703548».FarrellJonesConsequences (2 statements).

theorem projective_module_isStablyFree {G : Type*} [Group G] (hG : ∀ g : G, IsOfFinOrder g → g = 1)
    (M : Type*) [AddCommGroup M] [Module (MonoidAlgebra ℤ G) M]
    [Module.Finite (MonoidAlgebra ℤ G) M] [Module.Projective (MonoidAlgebra ℤ G) M] :
    Module.IsStablyFree (MonoidAlgebra ℤ G) M
theorem bass_conjecture_integral_domain {R : Type*} [CommRing R] [IsDomain R] {G : Type*}
    [Group G] {n : Type*} [Fintype n] (A : Matrix n n (MonoidAlgebra R G))
    (hA : A * A = A) (g : G) (hg : ¬IsUnit (orderOf g : R)) :
    matrixHattoriStallingsTraceAt A g = 0

What counts as progress

  • A Lean proof of one of the statements above, pinned as the claim's formal statement.
  • Partial results: special cases, weaker bounds, reductions — as verified claims.
  • Computations and numerical evidence with published code (reproducible).
  • Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
  • A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

  • [BLR08] arxiv/math.0703548 On the Farrell–Jones Conjecture and its applications by Arthur Bartels, Wolfgang Lück, Holger Reich, J. Topol. 1 (2008), 57–86.

Source and licence

Imported from Formal Conjectures (arXiv papers), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.