Algebraic consequences of the Farrell–Jones conjecture: vanishing of $\widetilde K_0(\mathbb{Z}[G])$ and the Bass conjecture

### What is the conjecture

Two algebraic consequences of the Farrell–Jones conjecture, both stated in the introduction of
Bartels–Lück–Reich. Unlike the conjecture itself (#1792), each is expressible with the algebra
already in Mathlib.

**1. Vanishing of the reduced projective class group.** If $G$ is torsionfree then
$\widetilde K_0(\mathbb{Z}[G]) = 0$, equivalently every finitely generated projective
$\mathbb{Z}[G]$-module is stably free. This is the conclusion of Theorem 0.2 (ii) for the regular
ring $\mathbb{Z}$; that theorem assumes the K-theoretic Farrell–Jones conjecture for $G$ with
coefficients in $\mathbb{Z}$.

**2. Bass conjecture for commutative integral domains** (Conjecture 0.6). Let $R$ be a commutative
integral domain, $G$ a group and $g \in G$. Suppose the order $|g|$ is infinite, or that $|g|$ is
finite and not invertible in $R$. Then for every finitely generated projective $RG$-module $P$ the
value of the Hattori–Stallings rank $\mathrm{HS}_{RG}(P)$ at $(g)$ is zero. By Theorems 0.5 (ii)
and 0.7 this follows from the Farrell–Jones conjecture with coefficients in every field of prime
characteristic.

Known cases of Conjecture 0.6: Bass for $R = \mathbb{C}$ and $G$ linear, Linnell for
$|g| < \infty$ and $R = \mathbb{Z}$, Eckmann for $R = \mathbb{Q}$ and
$\mathrm{cd}_{\mathbb{Q}} G \le 2$. The general case is open.

**Sources:**
- [arxiv/math.0703548](https://arxiv.org/abs/math/0703548) **On the Farrell–Jones Conjecture and
its applications** by *Arthur Bartels, Wolfgang Lück, Holger Reich*, J. Topol. 1 (2008), 57–86.
Theorem 0.2, Conjecture 0.6, and definitions (4.1), (4.2).

### Prerequisites needed

Mathlib has no algebraic K-theory of rings, so the assembly map is out of reach and #1792 stays
blocked. These two consequences are not:

- Statement 1 needs only `Module.IsStablyFree`, `Module.Finite` and `Module.Projective` over
`MonoidAlgebra ℤ G`, all of which exist.
- Statement 2 needs the Hattori–Stallings rank, which Mathlib does not have. It can be stated on
idempotent matrices instead, following (4.1) and (4.2) of the reference: the universal trace of
the sum of the diagonal entries, evaluated at one conjugacy class. That is a short local
definition.

One thing to watch: "torsionfree" here must not be rendered as Mathlib's `IsMulTorsionFree`, which
asks that every power map be injective. That is equivalent to torsion-freeness only for commutative
groups — `isMulTorsionFree_iff_not_isOfFinOrder` lives in `section CommGroup`. The Klein bottle
group is torsionfree but has $(ab)^2 = b^2$ with $ab \ne b$.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-16
* ams-19
* ams-20

### Choose either option

- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Choose one of the two consequences, then read the cited Bartels–Lück–Reich definitions (4.1) and (4.2) alongside Mathlib's Module.IsStablyFree, Module.Finite, and Module.Projective declarations over MonoidAlgebra ℤ G. For the Bass statement, inspect how an idempotent-matrix formulation could provide the missing local definition. Done means the selected consequence is stated in Lean with its prerequisites represented without using algebraic K-theory or IsMulTorsionFree.

Written by the indexing model from the issue text.