we-solve (beta)

Math-2512 · mathematics · Algebra

Complex group-ring traces vanish on infinite-order classes

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every discrete group G, every $q\geq 1$ and every idempotent $e\in M_q(C[G])$, is the sum of the diagonal coefficients of e over each infinite-order conjugacy class zero?

Short English statement

For every discrete group G, every $q\geq 1$ and every idempotent $e\in M_q(C[G])$, is the sum of the diagonal coefficients of e over each infinite-order conjugacy class zero?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2512-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2512

The main theorem makes the Hattori--Stallings trace of every K_0(C G) class vanish on each infinite-order conjugacy class. An idempotent matrix represents a projective class, and its trace is the displayed sum of diagonal coefficients. lean/docs/207.md covers this exact complex trace conclusion. Within these assumptions, this is a claimed affirmative answer to the stated question.

Complex group-ring traces vanish on infinite-order classes

OpenAI's claim

OpenAI presents a proof in the selected manuscript. The Bass trace restriction is claimed for complex group rings of arbitrary discrete groups, implying triviality of scalar idempotents for torsion-free groups over characteristic-zero domains.

Mathematical statement of the claimed result

Result 1.
For an arbitrary discrete group $G$, let $\operatorname{HS}_G$ be the Hattori--Stallings trace, whose value at a conjugacy class sums the coefficients on that class. For every $x\in K_0(\mathbb C[G])$, \[ |g|=\infty\quad\Longrightarrow\quad\operatorname{HS}_G(x)([g])=0. \] The torsion-free corollary states that, for every $q\ge1$ and idempotent $e\in M_q(\mathbb C[G])$, its identity-coefficient trace equals the rank of its augmentation matrix: \[ \tau_{G,q}(e)=\operatorname{rank}_{\mathbb C}(\epsilon_{G,q}(e)). \] For such $G$, any commutative unital domain $R$ of characteristic zero satisfies \[ e\in R[G],\ e^2=e\quad\Longrightarrow\quad e\in\{0,1\}. \] The characteristic-zero qualification does not cover positive-characteristic group rings.

Outline of the argument

An idempotent is encoded by finite cyclic path configurations whose weighted deletion relations generate cycles. Exterior differential forms and a cyclic Pfaffian identity detect forbidden conjugacy support; trace-rank arguments then turn the complex trace conclusion into the stated idempotent consequence.

Formal verification

For family 207, the documented Lean statements give complex group-ring Bass trace support and characteristic-zero torsion-free trace rank and idempotent triviality. The separate $\ell^1$ theorem is not selected. The listed Comparator files are BassTorsionFree.lean, BassTrace.lean. Named declarations include OAI.BassTrace.RightProjective.bassTraceModules_vanishing_and_support. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

Go to contribution →