Baum–Connes conjecture

[franzhusch]

What is the conjecture

Let $G$ be a discrete group. The assembly map is a homomorphism $$\mu: K_^{\text{top}}(G) \to K_(C_r^(G))$$ from the topological K-theory of $G$ to the K-theory of the reduced group C-algebra $C_r^*(G)$, defined via the Kasparov descent construction.

The Baum–Connes conjecture asserts that this assembly map is an isomorphism for every discrete group $G$. Equivalently, the assembly map is both injective and surjective.

The conjecture is known to hold for several classes of groups, including:

• Compact groups
• Abelian groups
• Lie groups with finitely many connected components
• Groups with the Haagerup property (a-T-menable groups)
• Discrete cocompact subgroups of real Lie groups of real rank 1

However, a counterexample to the Baum–Connes conjecture with coefficients was discovered in 2002 by Higson, Lafforgue, and Skandalis. The conjecture for the coefficient-free case remains open.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

Sources:

• https://en.wikipedia.org/wiki/Baum%E2%80%93Connes_conjecture, https://ncatlab.org/nlab/show/Baum-Connes+conjecture, https://arxiv.org/abs/1905.10081, https://chatterj.perso.math.cnrs.fr/papers/Valette.pdf

Prerequisites needed

Formalizability Rating: 5/5 (0 is best) (as of 2026-02-04)

Building blocks (1-3; from search results):

• K-theory and KK-theory (Mathlib has basic K-theory infrastructure)
• Topological groups and group C*-algebras (Mathlib has group C*-algebra definitions in Analysis.CstarAlgebra.Nnnorm)
• Assembly maps and index theory constructions (partially available)

Missing pieces (exactly 2; unclear/absent from search results):

• Equivariant K-theory and equivariant KK-theory framework (Kasparov descent constructions)
• Rigorous formalization of the reduced group C*-algebra as a functor from groups to C*-algebras with its functorial properties

Rating justification (1-2 sentences): The basic objects (groups, C*-algebras, K-theory) exist or have partial infrastructure in Mathlib, but formalizing the assembly map requires substantial development of equivariant KK-theory and the descent machinery, which is not standard in Mathlib. This is a moderate-to-significant infrastructure lift.

AMS categories

• ams-19
• ams-46
• ams-47

Choose either option

• 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

---

This issue was generated by an AI agent and reviewed by me.

See more information here: link

Feedback on mistakes/hallucinations: link