Lean statement

Complex Bass trace vanishing and support

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorem selected for verification: OAI.BassTrace.RightProjective.bassTraceModules_vanishing_and_support

Lean statement file: BassTrace.leanShow on the mapFamily 207. OpenAI lists this as a main result in its Lean catalogue.

See the candidate theorem Who ran the proof-verification program Report a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem bassTraceModules_vanishing_and_support {G : Type u} [_root_.Group G]    (x : ModuleK0.{u,v} (MonoidAlgebra ℂ G)) :    (∀ g : G, ¬IsOfFinOrder g → HattoriStallings x (ConjClasses.mk g) = 0) ∧      ↑(HattoriStallings x).support ⊆        {c | ∃ g : G, IsOfFinOrder g ∧ ConjClasses.mk g = c} :=  by sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

definition OAI.BassTrace.classCoefficient line 19

noncomputable def classCoefficient {G : Type*} [Group G]    (g : G) (a : MonoidAlgebra ℂ G) : ℂ := by  classical  exact a.coeff.sum fun h z => if IsConj h g then z else 0

structure OAI.BassTrace.K0.Idempotent line 30

structure Idempotent (R : Type*) [Ring R] where  size : ℕ  matrix : Matrix (Fin size) (Fin size) R  idem : matrix*matrix=matrix

definition OAI.BassTrace.K0.directSum line 37

def directSum (e f : Idempotent R) : Idempotent R where  size := e.size+f.size  matrix := Matrix.reindexRingEquiv R finSumFinEquiv (Matrix.fromBlocks e.matrix 0 0 f.matrix)  idem := by    rw [←map_mul,Matrix.fromBlocks_multiply]    simp only [Matrix.mul_zero,Matrix.zero_mul,add_zero,zero_add,e.idem,f.idem]

definition OAI.BassTrace.K0.relationGenerators line 44

def relationGenerators (R : Type*) [Ring R] : Set (FreeAbelianGroup (Idempotent R)) :=  {x | (∃e f : Idempotent R,∃a : Matrix (Fin e.size) (Fin f.size) R,    ∃b : Matrix (Fin f.size) (Fin e.size) R,    a*b=e.matrix ∧ b*a=f.matrix ∧ x=FreeAbelianGroup.of e-FreeAbelianGroup.of f) ∨    (∃e f : Idempotent R,x=FreeAbelianGroup.of (directSum e f)-FreeAbelianGroup.of e-FreeAbelianGroup.of f)}

definition OAI.BassTrace.K0.relations line 50

def relations (R : Type*) [Ring R] : AddSubgroup (FreeAbelianGroup (Idempotent R)) :=  AddSubgroup.closure (relationGenerators R)

abbreviation OAI.BassTrace.K0.Group line 55

abbrev Group (R : Type*) [Ring R] := FreeAbelianGroup (Idempotent R) ⧸ relations R

definition OAI.BassTrace.K0.rawCoefficient line 63

def rawCoefficient (g : G) : FreeAbelianGroup (Idempotent (MonoidAlgebra ℂ G)) →+ ℂ :=  FreeAbelianGroup.lift (fun e=>classCoefficient g (Matrix.trace e.matrix))

definition OAI.BassTrace.K0.classTrace line 70

def classTrace (a : MonoidAlgebra ℂ G) : ConjClasses G →₀ ℂ :=  Finsupp.mapDomain ConjClasses.mk a.coeff

definition OAI.BassTrace.K0.rawTrace line 73

def rawTrace : FreeAbelianGroup (Idempotent (MonoidAlgebra ℂ G)) →+ (ConjClasses G →₀ ℂ) :=  FreeAbelianGroup.lift (fun e=>classTrace (Matrix.trace e.matrix))

definition OAI.BassTrace.K0.HattoriStallings line 76

def HattoriStallings : Group (MonoidAlgebra ℂ G) →+ (ConjClasses G →₀ ℂ) := by

Show the remaining 110 lines

  have classCoefficient_zero (g : G) :      classCoefficient g 0 = 0 := by    simp [classCoefficient]  have classCoefficient_single (g h : G) (z : ℂ) :      classCoefficient g (MonoidAlgebra.single h z) = if IsConj h g then z else 0 := by    classical    simp [classCoefficient, Finsupp.sum_single_index]  have classCoefficient_add (g : G) (a b : MonoidAlgebra ℂ G) :      classCoefficient g (a + b) = classCoefficient g a + classCoefficient g b := by    classical    apply Finsupp.sum_add_index    · intro h _      simp    · intro h _ z w      split_ifs <;> simp  have classCoefficient_smul (g : G) (z : ℂ) (a : MonoidAlgebra ℂ G) :      classCoefficient g (z • a) = z * classCoefficient g a := by    classical    unfold classCoefficient    rw [MonoidAlgebra.coeff_smul, Finsupp.sum_smul_index (fun _ => by simp)]    rw [Finsupp.sum, Finsupp.sum, Finset.mul_sum]    apply Finset.sum_congr rfl    intro h _    split_ifs <;> simp  have classCoefficient_sum {ι : Type} (g : G) (s : Finset ι)      (f : ι → MonoidAlgebra ℂ G) :      classCoefficient g (∑ i ∈ s, f i) = ∑ i ∈ s, classCoefficient g (f i) := by    classical    induction s using Finset.induction_on with    | empty => simp [classCoefficient_zero]    | @insert a s ha ih => simp [classCoefficient_add, ha, ih]  have classCoefficient_mul_comm (g : G) (a b : MonoidAlgebra ℂ G) :      classCoefficient g (a * b) = classCoefficient g (b * a) := by    induction a using MonoidAlgebra.induction_on with    | of h =>        induction b using MonoidAlgebra.induction_on with        | of k =>            have hconj : IsConj (h * k) (k * h) := by              apply isConj_iff.mpr              exact ⟨k, by simp [mul_assoc]⟩            have hiff : IsConj (h * k) g ↔ IsConj (k * h) g :=              ⟨hconj.symm.trans, hconj.trans⟩            change classCoefficient g (MonoidAlgebra.single h 1 * MonoidAlgebra.single k 1) =              classCoefficient g (MonoidAlgebra.single k 1 * MonoidAlgebra.single h 1)            simp only [MonoidAlgebra.single_mul_single, classCoefficient_single, hiff]        | add b c hb hc => simp only [mul_add, add_mul, classCoefficient_add, hb, hc]        | smul z b hb => simp only [mul_smul_comm, smul_mul_assoc, classCoefficient_smul, hb]    | add a c ha hc => simp only [add_mul, mul_add, classCoefficient_add, ha, hc]    | smul z a ha => simp only [mul_smul_comm, smul_mul_assoc, classCoefficient_smul, ha]  have classCoefficient_matrix_mul_comm {ι κ : Type} [Fintype ι] [Fintype κ]      (g : G) (a : Matrix ι κ (MonoidAlgebra ℂ G))      (b : Matrix κ ι (MonoidAlgebra ℂ G)) :      classCoefficient g (Matrix.trace (a * b)) =        classCoefficient g (Matrix.trace (b * a)) := by    classical    simp only [Matrix.trace, Matrix.diag, Matrix.mul_apply, classCoefficient_sum]    rw [Finset.sum_comm]    apply Finset.sum_congr rfl    intro i _    apply Finset.sum_congr rfl    intro j _    exact classCoefficient_mul_comm g _ _  have trace_reindex {α β : Type} [Fintype α] [Fintype β]      (j : α≃β) (a : Matrix α α (MonoidAlgebra ℂ G)) :      Matrix.trace (Matrix.reindexRingEquiv (MonoidAlgebra ℂ G) j a)=Matrix.trace a := by    change (∑i, a (j.symm i) (j.symm i))=∑i,a i i    exact Equiv.sum_comp j.symm (fun i=>a i i)  have trace_directSum (e f : Idempotent (MonoidAlgebra ℂ G)) :      Matrix.trace (directSum e f).matrix=Matrix.trace e.matrix+Matrix.trace f.matrix := by    rw [directSum,trace_reindex]    simp only [Matrix.trace,Matrix.diag,Fintype.sum_sum_type,Matrix.fromBlocks_apply₁₁,Matrix.fromBlocks_apply₂₂]  have relations_in_kernel (g : G) : relations (MonoidAlgebra ℂ G)≤(rawCoefficient g).ker := by    apply (AddSubgroup.closure_le _).mpr    intro x hx    rcases hx with ⟨e,f,a,b,hab,hba,rfl⟩|⟨e,f,rfl⟩    · change rawCoefficient g (FreeAbelianGroup.of e-FreeAbelianGroup.of f)=0      simp only [map_sub,rawCoefficient,FreeAbelianGroup.lift_apply_of]      apply sub_eq_zero.mpr      rw [←hab,←hba]      exact classCoefficient_matrix_mul_comm g a b    · change rawCoefficient g (FreeAbelianGroup.of (directSum e f)-FreeAbelianGroup.of e-FreeAbelianGroup.of f)=0      simp only [map_sub,rawCoefficient,FreeAbelianGroup.lift_apply_of,trace_directSum,classCoefficient_add]      rw [add_sub_cancel_left, sub_self]  have classTrace_apply (a : MonoidAlgebra ℂ G) (g : G) :      classTrace a (ConjClasses.mk g)=classCoefficient g a := by    unfold classTrace classCoefficient    simp only [Finsupp.mapDomain,Finsupp.sum_apply,Finsupp.single_apply]    apply Finset.sum_congr rfl    intro h hh    dsimp only    by_cases hc : IsConj h g    · rw [ite_eq_left (ConjClasses.mk_eq_mk_iff_isConj.mpr hc), ite_eq_left hc]    · rw [ite_eq_right (mt ConjClasses.mk_eq_mk_iff_isConj.mp hc), ite_eq_right hc]  have rawTrace_apply (z : FreeAbelianGroup (Idempotent (MonoidAlgebra ℂ G))) (g : G) :      rawTrace z (ConjClasses.mk g)=rawCoefficient g z := by    induction z using FreeAbelianGroup.induction_on with    | zero => simp only [map_zero,Finsupp.zero_apply]    | of e =>      simp only [rawTrace,rawCoefficient,FreeAbelianGroup.lift_apply_of]      exact classTrace_apply _ g    | neg e he => simp only [map_neg,Finsupp.neg_apply,he]    | add x y hx hy => simp only [map_add,Finsupp.add_apply,hx,hy]  have relations_in_trace_kernel : relations (MonoidAlgebra ℂ G)≤(rawTrace (G := G)).ker := by    intro z hz    change rawTrace z=0    ext c    obtain ⟨g,rfl⟩ := ConjClasses.mk_surjective c    rw [rawTrace_apply,Finsupp.zero_apply]    exact relations_in_kernel g hz  exact QuotientAddGroup.lift (relations (MonoidAlgebra ℂ G)) rawTrace relations_in_trace_kernel

structure OAI.BassTrace.RightProjective.Retraction line 209

structure Retraction (R M : Type*) [Ring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] where  size : ℕ  proj : (Fin size →Rᵐᵒᵖ) →ₗ[Rᵐᵒᵖ] M  inc : M →ₗ[Rᵐᵒᵖ] (Fin size →Rᵐᵒᵖ)  split : proj.comp inc=LinearMap.id

definition OAI.BassTrace.RightProjective.freeSplit line 251

def freeSplit (n m : ℕ) : (Fin (n+m)→Rᵐᵒᵖ) ≃ₗ[Rᵐᵒᵖ] (Fin n→Rᵐᵒᵖ) × (Fin m→Rᵐᵒᵖ) :=  (LinearEquiv.piCongrLeft' Rᵐᵒᵖ (fun _ : Fin (n+m)=>Rᵐᵒᵖ) finSumFinEquiv.symm).trans    (LinearEquiv.sumArrowLequivProdArrow (Fin n) (Fin m) Rᵐᵒᵖ Rᵐᵒᵖ)

definition OAI.BassTrace.RightProjective.Retraction.prod line 255

def Retraction.prod (r : Retraction R M) (s : Retraction R N) : Retraction R (M×N) where

Show the remaining 12 lines

  size := r.size+s.size  proj := (r.proj.prodMap s.proj).comp (freeSplit r.size s.size).toLinearMap  inc := (freeSplit r.size s.size).symm.toLinearMap.comp (r.inc.prodMap s.inc)  split := by    apply LinearMap.ext    intro x    change ((r.proj.prodMap s.proj) ((freeSplit r.size s.size)      ((freeSplit r.size s.size).symm ((r.inc.prodMap s.inc) x))))=x    rw [LinearEquiv.apply_symm_apply]    have hr := LinearMap.congr_fun r.split x.1    have hs := LinearMap.congr_fun s.split x.2    exact Prod.ext hr hs

structure OAI.BassTrace.RightProjective.Object line 275

structure Object (R : Type u) [Ring R] where  carrier : Type v  [addCommGroup : AddCommGroup carrier]  [module : Module Rᵐᵒᵖ carrier]  [finite : Module.Finite Rᵐᵒᵖ carrier]  [projective : Module.Projective Rᵐᵒᵖ carrier]

definition OAI.BassTrace.RightProjective.moduleRelationGenerators line 297

def moduleRelationGenerators (R : Type u) [Ring R] : Set (FreeAbelianGroup (Object.{u,v} R)) :=  {x | (∃P Q : Object.{u,v} R, Nonempty (P.carrier≃ₗ[Rᵐᵒᵖ] Q.carrier) ∧    x=FreeAbelianGroup.of P-FreeAbelianGroup.of Q) ∨    (∃P Q : Object.{u,v} R,      x=FreeAbelianGroup.of (P.prod Q)-FreeAbelianGroup.of P-FreeAbelianGroup.of Q)}

definition OAI.BassTrace.RightProjective.moduleRelations line 303

def moduleRelations (R : Type u) [Ring R] : AddSubgroup (FreeAbelianGroup (Object.{u,v} R)) :=  AddSubgroup.closure (moduleRelationGenerators R)

abbreviation OAI.BassTrace.RightProjective.ModuleK0 line 306

abbrev ModuleK0 (R : Type u) [Ring R] :=  FreeAbelianGroup (Object.{u,v} R) ⧸ moduleRelations R

Possible paper match, with no recorded review

No paper statement clearly matched the Lean wording. Statement Map, the program that collects Atlas’s source records, selected this possible match using words in OpenAI’s catalogue and Lean note. No review of whether the statements mean the same thing is recorded.

Shared with the catalogue’s wording or OpenAI’s note, none of them matched in the Lean text: characteristic, commutative, domain, free, group, idempotent, rank, torsion and two more.

Statements in The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture come first because the release lists only that paper for this Lean statement.

Corollary 1.2 of The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture

Corollary

Let G be any torsion-free discrete group.

(i)
For every q\geq1 and every idempotent e\in M_q(\C G),
\tau_{G,q}(e)=\operatorname{rank}_{\C}\bigl(\epsilon_{G,q}(e)\bigr).
Consequently \tau_{G,*}=\operatorname{rk}_{\epsilon}, with \Z viewed as a subgroup of \C, and
\tau_{G,*}\bigl(K_0(\C G)\bigr)=\Z.
(ii)
For every commutative unital domain R of characteristic zero, every e\in RG satisfying e^2=e is either 0 or 1.

Section 1, Introduction Read it in the paper TeX source, line 98

Show the TeX

Let $G$ be any torsion-free discrete group.
\begin{enumerate}[label=\textup{(\roman*)}]
 \item For every $q\geq1$ and every idempotent $e\in M_q(\C G)$,
 \[
  \tau_{G,q}(e)=\operatorname{rank}_{\C}\bigl(\epsilon_{G,q}(e)\bigr).
 \]
 Consequently $\tau_{G,*}=\operatorname{rk}_{\epsilon}$, with
 $\Z$ viewed as a subgroup of $\C$, and
 \[
  \tau_{G,*}\bigl(K_0(\C G)\bigr)=\Z.
 \]
 \item For every commutative unital domain $R$ of characteristic zero,
 every $e\in RG$ satisfying $e^2=e$ is either $0$ or $1$.
\end{enumerate}

Other possible paper matches, closest wording first

Corollary 9.1 of The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture. Words of the Lean statement, its names split into words, that also appear in the theorem: hattori, stallings, supported, trace and group.
Theorem 1.1 of The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture. Words of the Lean statement, its names split into words, that also appear in the theorem: order, finite and group. Found in the paper’s title, which its main theorem states: bass, idempotent, zero and trace. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: element, conjugacy and infinite.
Proposition 2.2 of The ℓ¹-Bass Conjecture for Discrete Groups. Words of the Lean statement, its names split into words, that also appear in the theorem: subgroup, support, order, finite, idempotent, trace and one more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: conjugacy, generated and finitely.
Theorem 2.1 of The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture. Words of the Lean statement, its names split into words, that also appear in the theorem: vanishing, integer, zero and group. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: countable, generated and finitely.
Corollary 9.2 of The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture. Words of the Lean statement, its names split into words, that also appear in the theorem: id, pi, map, free, lift and traces.
Proposition 7.3 of The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture. Words of the Lean statement, its names split into words, that also appear in the theorem: complex and integer. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: generated and finitely.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

Accepted Their term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

Accepted Their term: “comparator-sandboxed-pass”.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Reported 8 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 207’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

MathVet
Finds part of it stated, or a narrower or weaker statement Their term: “weaker-statement”.
The challenge statements do not imply the headline claim: they state a nontrivially weaker statement. Their record
Their note: Headline is the ℓ¹-Bass conjecture over ℓ¹(G), but bassTraceModules_vanishing_and_support is only about the group algebra MonoidAlgebra ℂ G (Hattori-Stallings trace of every K0 class vanishes off finite-order classes and is supported on them); no ℓ¹(G) appears anywhere (docs: 'proves the complex Bass trace conjecture for every group'; docs title says ℓ¹ but scope does not). The algebraic companion IS stated: torsion_free_corollary gives trace = augmentation rank on K0(ℂ[G]) and ∀ R comm. domain with CharZero, e^2 = e → e = 0 ∨ e = 1 for torsion-free G.
Definitions the group asks readers to compare with the paper: Hand-rolled K0: BassTrace.K0.Group R := FreeAbelianGroup (Idempotent R) ⧸ relations R (relations: e ~ f when a*b = e ∧ b*a = f, plus direct sums) and ModuleK0 of f.g. projective right modules, HattoriStallings into ConjClasses G →₀ ℂ; standard presentations, not Mathlib objects.
Carlos Toledo’s cert-machine
Finds part of it stated, or a narrower or weaker statement Their term: “NARROWER — UNDECLARED”.
The challenge statements state less than the headline, and OpenAI’s Lean note does not say so. Their record
Their note: The ℓ¹(G) version (the family's titular result and the October 5 paper) and the integral Bass trace conjecture for K₀(ℤG) are not stated. Only the ℂ[G] Bass conjecture and the torsion-free consequences are.

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“The formalization proves the complex Bass trace conjecture for every group: the Hattori–Stallings trace of each virtual class of finitely generated projective right $\mathbb C[G]$-modules vanishes on conjugacy classes of infinite-order elements. No finiteness, countability, or geometric hypothesis on $G$ is imposed.”
Quoted from OpenAI’s Lean note for this family

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

483 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 185 to its own declarations, 421 to Mathlib’s documentation. 32 declared names also link to the same declaration in OpenAI’s library. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlib.Algebra.Group.Conjimport Mathlib.Algebra.MonoidAlgebra.Basicimport Mathlib.Basic.Complex.Basicimport Mathlib.GroupTheory.FreeAbelianGroupimport Mathlib.GroupTheory.OrderOfElementimport Mathlib.LinearAlgebra.Matrix.Traceimport Mathlib.LinearAlgebra.Matrix.ToLinimport Mathlib.RingTheory.Finiteness.Projectiveimport Mathlib.Tacticnamespace OAInoncomputable sectionnamespace BassTraceopen scoped Classicalnoncomputable def classCoefficient {G : Type*} [Group G]    (g : G) (a : MonoidAlgebra ℂ G) : ℂ := by  classical  exact a.coeff.sum fun h z => if IsConj h g then z else 0namespace K0open scoped Classical BigOperatorssectionstructure Idempotent (R : Type*) [Ring R] where  size : ℕ  matrix : Matrix (Fin size) (Fin size) R  idem : matrix*matrix=matrixvariable {R : Type*} [Ring R]def directSum (e f : Idempotent R) : Idempotent R where  size := e.size+f.size  matrix := Matrix.reindexRingEquiv R finSumFinEquiv (Matrix.fromBlocks e.matrix 0 0 f.matrix)  idem := by    rw [←map_mul,Matrix.fromBlocks_multiply]    simp only [Matrix.mul_zero,Matrix.zero_mul,add_zero,zero_add,e.idem,f.idem]def relationGenerators (R : Type*) [Ring R] : Set (FreeAbelianGroup (Idempotent R)) :=  {x | (∃e f : Idempotent R,∃a : Matrix (Fin e.size) (Fin f.size) R,    ∃b : Matrix (Fin f.size) (Fin e.size) R,    a*b=e.matrix ∧ b*a=f.matrix ∧ x=FreeAbelianGroup.of e-FreeAbelianGroup.of f) ∨    (∃e f : Idempotent R,x=FreeAbelianGroup.of (directSum e f)-FreeAbelianGroup.of e-FreeAbelianGroup.of f)}def relations (R : Type*) [Ring R] : AddSubgroup (FreeAbelianGroup (Idempotent R)) :=  AddSubgroup.closure (relationGenerators R)instance relations_normal (R : Type*) [Ring R] : (relations R).Normal := inferInstanceabbrev Group (R : Type*) [Ring R] := FreeAbelianGroup (Idempotent R) ⧸ relations Rdef classOf (e : Idempotent R) : Group R := QuotientAddGroup.mk' (relations R) (FreeAbelianGroup.of e)variable {G : Type*} [_root_.Group G]instance groupRingRelations_normal : (relations (MonoidAlgebra ℂ G)).Normal := inferInstancedef rawCoefficient (g : G) : FreeAbelianGroup (Idempotent (MonoidAlgebra ℂ G)) →+ ℂ :=  FreeAbelianGroup.lift (fun e=>classCoefficient g (Matrix.trace e.matrix))endvariable {G : Type*} [_root_.Group G]def classTrace (a : MonoidAlgebra ℂ G) : ConjClasses G →₀ ℂ :=  Finsupp.mapDomain ConjClasses.mk a.coeffdef rawTrace : FreeAbelianGroup (Idempotent (MonoidAlgebra ℂ G)) →+ (ConjClasses G →₀ ℂ) :=  FreeAbelianGroup.lift (fun e=>classTrace (Matrix.trace e.matrix))def HattoriStallings : Group (MonoidAlgebra ℂ G) →+ (ConjClasses G →₀ ℂ) := by  have classCoefficient_zero (g : G) :      classCoefficient g 0 = 0 := by    simp [classCoefficient]  have classCoefficient_single (g h : G) (z : ℂ) :      classCoefficient g (MonoidAlgebra.single h z) = if IsConj h g then z else 0 := by    classical    simp [classCoefficient, Finsupp.sum_single_index]  have classCoefficient_add (g : G) (a b : MonoidAlgebra ℂ G) :      classCoefficient g (a + b) = classCoefficient g a + classCoefficient g b := by    classical    apply Finsupp.sum_add_index    · intro h _      simp    · intro h _ z w      split_ifs <;> simp  have classCoefficient_smul (g : G) (z : ℂ) (a : MonoidAlgebra ℂ G) :      classCoefficient g (z • a) = z * classCoefficient g a := by    classical    unfold classCoefficient    rw [MonoidAlgebra.coeff_smul, Finsupp.sum_smul_index (fun _ => by simp)]    rw [Finsupp.sum, Finsupp.sum, Finset.mul_sum]    apply Finset.sum_congr rfl    intro h _    split_ifs <;> simp  have classCoefficient_sum {ι : Type} (g : G) (s : Finset ι)      (f : ι → MonoidAlgebra ℂ G) :      classCoefficient g (∑ i ∈ s, f i) = ∑ i ∈ s, classCoefficient g (f i) := by    classical    induction s using Finset.induction_on with    | empty => simp [classCoefficient_zero]    | @insert a s ha ih => simp [classCoefficient_add, ha, ih]  have classCoefficient_mul_comm (g : G) (a b : MonoidAlgebra ℂ G) :      classCoefficient g (a * b) = classCoefficient g (b * a) := by    induction a using MonoidAlgebra.induction_on with    | of h =>        induction b using MonoidAlgebra.induction_on with        | of k =>            have hconj : IsConj (h * k) (k * h) := by              apply isConj_iff.mpr              exact ⟨k, by simp [mul_assoc]⟩            have hiff : IsConj (h * k) g ↔ IsConj (k * h) g :=              ⟨hconj.symm.trans, hconj.trans⟩            change classCoefficient g (MonoidAlgebra.single h 1 * MonoidAlgebra.single k 1) =              classCoefficient g (MonoidAlgebra.single k 1 * MonoidAlgebra.single h 1)            simp only [MonoidAlgebra.single_mul_single, classCoefficient_single, hiff]        | add b c hb hc => simp only [mul_add, add_mul, classCoefficient_add, hb, hc]        | smul z b hb => simp only [mul_smul_comm, smul_mul_assoc, classCoefficient_smul, hb]    | add a c ha hc => simp only [add_mul, mul_add, classCoefficient_add, ha, hc]    | smul z a ha => simp only [mul_smul_comm, smul_mul_assoc, classCoefficient_smul, ha]  have classCoefficient_matrix_mul_comm {ι κ : Type} [Fintype ι] [Fintype κ]      (g : G) (a : Matrix ι κ (MonoidAlgebra ℂ G))      (b : Matrix κ ι (MonoidAlgebra ℂ G)) :      classCoefficient g (Matrix.trace (a * b)) =        classCoefficient g (Matrix.trace (b * a)) := by    classical    simp only [Matrix.trace, Matrix.diag, Matrix.mul_apply, classCoefficient_sum]    rw [Finset.sum_comm]    apply Finset.sum_congr rfl    intro i _    apply Finset.sum_congr rfl    intro j _    exact classCoefficient_mul_comm g _ _  have trace_reindex {α β : Type} [Fintype α] [Fintype β]      (j : α≃β) (a : Matrix α α (MonoidAlgebra ℂ G)) :      Matrix.trace (Matrix.reindexRingEquiv (MonoidAlgebra ℂ G) j a)=Matrix.trace a := by    change (∑i, a (j.symm i) (j.symm i))=∑i,a i i    exact Equiv.sum_comp j.symm (fun i=>a i i)  have trace_directSum (e f : Idempotent (MonoidAlgebra ℂ G)) :      Matrix.trace (directSum e f).matrix=Matrix.trace e.matrix+Matrix.trace f.matrix := by    rw [directSum,trace_reindex]    simp only [Matrix.trace,Matrix.diag,Fintype.sum_sum_type,Matrix.fromBlocks_apply₁₁,Matrix.fromBlocks_apply₂₂]  have relations_in_kernel (g : G) : relations (MonoidAlgebra ℂ G)≤(rawCoefficient g).ker := by    apply (AddSubgroup.closure_le _).mpr    intro x hx    rcases hx with ⟨e,f,a,b,hab,hba,rfl⟩|⟨e,f,rfl⟩    · change rawCoefficient g (FreeAbelianGroup.of e-FreeAbelianGroup.of f)=0      simp only [map_sub,rawCoefficient,FreeAbelianGroup.lift_apply_of]      apply sub_eq_zero.mpr      rw [←hab,←hba]      exact classCoefficient_matrix_mul_comm g a b    · change rawCoefficient g (FreeAbelianGroup.of (directSum e f)-FreeAbelianGroup.of e-FreeAbelianGroup.of f)=0      simp only [map_sub,rawCoefficient,FreeAbelianGroup.lift_apply_of,trace_directSum,classCoefficient_add]      rw [add_sub_cancel_left, sub_self]  have classTrace_apply (a : MonoidAlgebra ℂ G) (g : G) :      classTrace a (ConjClasses.mk g)=classCoefficient g a := by    unfold classTrace classCoefficient    simp only [Finsupp.mapDomain,Finsupp.sum_apply,Finsupp.single_apply]    apply Finset.sum_congr rfl    intro h hh    dsimp only    by_cases hc : IsConj h g    · rw [ite_eq_left (ConjClasses.mk_eq_mk_iff_isConj.mpr hc), ite_eq_left hc]    · rw [ite_eq_right (mt ConjClasses.mk_eq_mk_iff_isConj.mp hc), ite_eq_right hc]  have rawTrace_apply (z : FreeAbelianGroup (Idempotent (MonoidAlgebra ℂ G))) (g : G) :      rawTrace z (ConjClasses.mk g)=rawCoefficient g z := by    induction z using FreeAbelianGroup.induction_on with    | zero => simp only [map_zero,Finsupp.zero_apply]    | of e =>      simp only [rawTrace,rawCoefficient,FreeAbelianGroup.lift_apply_of]      exact classTrace_apply _ g    | neg e he => simp only [map_neg,Finsupp.neg_apply,he]    | add x y hx hy => simp only [map_add,Finsupp.add_apply,hx,hy]  have relations_in_trace_kernel : relations (MonoidAlgebra ℂ G)≤(rawTrace (G := G)).ker := by    intro z hz    change rawTrace z=0    ext c    obtain ⟨g,rfl⟩ := ConjClasses.mk_surjective c    rw [rawTrace_apply,Finsupp.zero_apply]    exact relations_in_kernel g hz  exact QuotientAddGroup.lift (relations (MonoidAlgebra ℂ G)) rawTrace relations_in_trace_kernelend K0namespace RightProjectiveopen scoped Classical BigOperatorsopen MulOppositesectionvariable {R : Type*} [Ring R]instance rightModuleIdentityRingHomInvPair :    RingHomInvPair (RingHom.id Rᵐᵒᵖ) (RingHom.id Rᵐᵒᵖ) := RingHomInvPair.idsdef unopTranspose {m n : Type*} (a : Matrix m n Rᵐᵒᵖ) : Matrix n m R :=  fun i j=>unop (a j i)def rightMatrix {m n : ℕ} (f : (Fin m → Rᵐᵒᵖ) →ₗ[Rᵐᵒᵖ] (Fin n → Rᵐᵒᵖ)) :    Matrix (Fin n) (Fin m) R := unopTranspose (LinearMap.toMatrixRight' f)structure Retraction (R M : Type*) [Ring R] [AddCommGroup M] [Module Rᵐᵒᵖ M] where  size : ℕ  proj : (Fin size →Rᵐᵒᵖ) →ₗ[Rᵐᵒᵖ] M  inc : M →ₗ[Rᵐᵒᵖ] (Fin size →Rᵐᵒᵖ)  split : proj.comp inc=LinearMap.idvariable {M N : Type*} [AddCommGroup M] [Module Rᵐᵒᵖ M]  [AddCommGroup N] [Module Rᵐᵒᵖ N]def Retraction.idempotent (r : Retraction R M) : K0.Idempotent R := by  have unopTranspose_mul {l m n : Type} [Fintype m]      (a : Matrix l m Rᵐᵒᵖ) (b : Matrix m n Rᵐᵒᵖ) :      unopTranspose (a*b)=unopTranspose b*unopTranspose a := by    ext i j    simp only [unopTranspose,Matrix.mul_apply]    change (opAddEquiv.symm : Rᵐᵒᵖ≃+R) (∑k,a j k*b k i)=_    rw [map_sum]    rfl  have rightMatrix_comp {l m n : ℕ}      (f : (Fin l →Rᵐᵒᵖ) →ₗ[Rᵐᵒᵖ] (Fin m →Rᵐᵒᵖ))      (g : (Fin m →Rᵐᵒᵖ) →ₗ[Rᵐᵒᵖ] (Fin n →Rᵐᵒᵖ)) :      rightMatrix (g.comp f)=rightMatrix g*rightMatrix f := by    simp only [rightMatrix,LinearMap.toMatrixRight'_comp,unopTranspose_mul]  exact {    size := r.size    matrix := rightMatrix (r.inc.comp r.proj)    idem := by      rw [←rightMatrix_comp]      congr 1      calc (r.inc.comp r.proj).comp (r.inc.comp r.proj) =          r.inc.comp ((r.proj.comp r.inc).comp r.proj) := by simp only [LinearMap.comp_assoc]        _ = r.inc.comp r.proj := by rw [r.split,LinearMap.id_comp] }def Retraction.transport (r : Retraction R M) (u : M≃ₗ[Rᵐᵒᵖ] N) : Retraction R N where  size := r.size  proj := u.toLinearMap.comp r.proj  inc := r.inc.comp u.symm.toLinearMap  split := by    calc (u.toLinearMap.comp r.proj).comp (r.inc.comp u.symm.toLinearMap) =      u.toLinearMap.comp ((r.proj.comp r.inc).comp u.symm.toLinearMap) := by simp only [LinearMap.comp_assoc]      _ = LinearMap.id := by rw [r.split,LinearMap.id_comp,LinearEquiv.comp_symm]def freeSplit (n m : ℕ) : (Fin (n+m)→Rᵐᵒᵖ) ≃ₗ[Rᵐᵒᵖ] (Fin n→Rᵐᵒᵖ) × (Fin m→Rᵐᵒᵖ) :=  (LinearEquiv.piCongrLeft' Rᵐᵒᵖ (fun _ : Fin (n+m)=>Rᵐᵒᵖ) finSumFinEquiv.symm).trans    (LinearEquiv.sumArrowLequivProdArrow (Fin n) (Fin m) Rᵐᵒᵖ Rᵐᵒᵖ)def Retraction.prod (r : Retraction R M) (s : Retraction R N) : Retraction R (M×N) where  size := r.size+s.size  proj := (r.proj.prodMap s.proj).comp (freeSplit r.size s.size).toLinearMap  inc := (freeSplit r.size s.size).symm.toLinearMap.comp (r.inc.prodMap s.inc)  split := by    apply LinearMap.ext    intro x    change ((r.proj.prodMap s.proj) ((freeSplit r.size s.size)      ((freeSplit r.size s.size).symm ((r.inc.prodMap s.inc) x))))=x    rw [LinearEquiv.apply_symm_apply]    have hr := LinearMap.congr_fun r.split x.1    have hs := LinearMap.congr_fun s.split x.2    exact Prod.ext hr hsendopen scoped Classicaluniverse u vstructure Object (R : Type u) [Ring R] where  carrier : Type v  [addCommGroup : AddCommGroup carrier]  [module : Module Rᵐᵒᵖ carrier]  [finite : Module.Finite Rᵐᵒᵖ carrier]  [projective : Module.Projective Rᵐᵒᵖ carrier]attribute [instance] Object.addCommGroup Object.module Object.finite Object.projectivevariable {R : Type u} [Ring R]def Object.prod (P Q : Object.{u,v} R) : Object.{u,v} R where  carrier := P.carrier × Q.carrierdef Object.retraction (P : Object.{u,v} R) : Retraction R P.carrier :=  Classical.choice (by    obtain ⟨n, f, g, _, _, h⟩ := Module.Finite.exists_comp_eq_id_of_projective Rᵐᵒᵖ P.carrier    exact ⟨⟨n, f, g, h⟩⟩)def Object.presentationClass (P : Object.{u,v} R) : K0.Group R :=  K0.classOf P.retraction.idempotentdef moduleRelationGenerators (R : Type u) [Ring R] : Set (FreeAbelianGroup (Object.{u,v} R)) :=  {x | (∃P Q : Object.{u,v} R, Nonempty (P.carrier≃ₗ[Rᵐᵒᵖ] Q.carrier) ∧    x=FreeAbelianGroup.of P-FreeAbelianGroup.of Q) ∨    (∃P Q : Object.{u,v} R,      x=FreeAbelianGroup.of (P.prod Q)-FreeAbelianGroup.of P-FreeAbelianGroup.of Q)}def moduleRelations (R : Type u) [Ring R] : AddSubgroup (FreeAbelianGroup (Object.{u,v} R)) :=  AddSubgroup.closure (moduleRelationGenerators R)abbrev ModuleK0 (R : Type u) [Ring R] :=  FreeAbelianGroup (Object.{u,v} R) ⧸ moduleRelations Rdef rawPresentation : FreeAbelianGroup (Object.{u,v} R) →+ K0.Group R :=  FreeAbelianGroup.lift Object.presentationClassdef presentation : ModuleK0.{u,v} R →+ K0.Group R := by  have unopTranspose_mul {l m n : ℕ}      (a : Matrix (Fin l) (Fin m) Rᵐᵒᵖ) (b : Matrix (Fin m) (Fin n) Rᵐᵒᵖ) :      unopTranspose (a*b)=unopTranspose b*unopTranspose a := by    ext i j    simp only [unopTranspose,Matrix.mul_apply]    change (opAddEquiv.symm : Rᵐᵒᵖ≃+R) (∑k,a j k*b k i)=_    rw [map_sum]    rfl  have rightMatrix_comp {l m n : ℕ}      (f : (Fin l →Rᵐᵒᵖ) →ₗ[Rᵐᵒᵖ] (Fin m →Rᵐᵒᵖ))      (g : (Fin m →Rᵐᵒᵖ) →ₗ[Rᵐᵒᵖ] (Fin n →Rᵐᵒᵖ)) :      rightMatrix (g.comp f)=rightMatrix g*rightMatrix f := by    simp only [rightMatrix,LinearMap.toMatrixRight'_comp,unopTranspose_mul]  have classOf_eq_of_rectangular (e f : K0.Idempotent R)      (a : Matrix (Fin e.size) (Fin f.size) R)      (b : Matrix (Fin f.size) (Fin e.size) R) (hab : a*b=e.matrix) (hba : b*a=f.matrix) :      K0.classOf e=K0.classOf f := by    apply sub_eq_zero.mp    change (QuotientAddGroup.mk' (K0.relations R)) (FreeAbelianGroup.of e)-      (QuotientAddGroup.mk' (K0.relations R)) (FreeAbelianGroup.of f)=0    rw [←map_sub]    change (QuotientAddGroup.mk (FreeAbelianGroup.of e-FreeAbelianGroup.of f) : K0.Group R)=0    apply (QuotientAddGroup.eq_zero_iff _).mpr    exact AddSubgroup.subset_closure (Or.inl ⟨e,f,a,b,hab,hba,rfl⟩)  have Retraction.class_eq {M : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] (r s : Retraction R M) :      K0.classOf r.idempotent=K0.classOf s.idempotent := by    apply classOf_eq_of_rectangular _ _      (rightMatrix (r.inc.comp s.proj)) (rightMatrix (s.inc.comp r.proj))    · change rightMatrix (r.inc.comp s.proj)*rightMatrix (s.inc.comp r.proj)=        rightMatrix (r.inc.comp r.proj)      rw [←rightMatrix_comp]      congr 1      calc (r.inc.comp s.proj).comp (s.inc.comp r.proj) =          r.inc.comp ((s.proj.comp s.inc).comp r.proj) := by simp only [LinearMap.comp_assoc]        _ = r.inc.comp r.proj := by rw [s.split,LinearMap.id_comp]    · change rightMatrix (s.inc.comp r.proj)*rightMatrix (r.inc.comp s.proj)=        rightMatrix (s.inc.comp s.proj)      rw [←rightMatrix_comp]      congr 1      calc (s.inc.comp r.proj).comp (r.inc.comp s.proj) =          s.inc.comp ((r.proj.comp r.inc).comp s.proj) := by simp only [LinearMap.comp_assoc]        _ = s.inc.comp s.proj := by rw [r.split,LinearMap.id_comp]  have Retraction.transport_idempotent {M N : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] [AddCommGroup N] [Module Rᵐᵒᵖ N] (r : Retraction R M) (u : M≃ₗ[Rᵐᵒᵖ] N) :      (r.transport u).idempotent=r.idempotent := by    dsimp only [Retraction.idempotent]    congr 1    change rightMatrix ((r.inc.comp u.symm.toLinearMap).comp (u.toLinearMap.comp r.proj))=      rightMatrix (r.inc.comp r.proj)    congr 1    apply LinearMap.ext    intro x    change r.inc (u.symm (u (r.proj x)))=r.inc (r.proj x)    rw [u.symm_apply_apply]  have freeSplit_apply_left (n m : ℕ) (v : Fin (n+m)→Rᵐᵒᵖ) (i : Fin n) :      (freeSplit n m v).1 i=v (finSumFinEquiv (Sum.inl i)) := rfl  have freeSplit_apply_right (n m : ℕ) (v : Fin (n+m)→Rᵐᵒᵖ) (i : Fin m) :      (freeSplit n m v).2 i=v (finSumFinEquiv (Sum.inr i)) := rfl  have freeSplit_symm_left (n m : ℕ) (v : Fin n→Rᵐᵒᵖ) (w : Fin m→Rᵐᵒᵖ) (i : Fin n) :      (freeSplit n m).symm (v,w) (finSumFinEquiv (Sum.inl i))=v i := by    have h := congrArg (fun x=>(x.1 : Fin n→Rᵐᵒᵖ) i) ((freeSplit (R := R) n m).apply_symm_apply (v,w))    exact h  have freeSplit_symm_right (n m : ℕ) (v : Fin n→Rᵐᵒᵖ) (w : Fin m→Rᵐᵒᵖ) (i : Fin m) :      (freeSplit n m).symm (v,w) (finSumFinEquiv (Sum.inr i))=w i := by    have h := congrArg (fun x=>(x.2 : Fin m→Rᵐᵒᵖ) i) ((freeSplit (R := R) n m).apply_symm_apply (v,w))    exact h  have freeSplit_single_left (n m : ℕ) (i : Fin n) :      freeSplit (R := R) n m (Pi.single (finSumFinEquiv (Sum.inl i)) 1)=(Pi.single i 1,0) := by    apply Prod.ext    · ext j      rw [freeSplit_apply_left]      simp only [Pi.single_apply,Equiv.apply_eq_iff_eq,Sum.inl.injEq]    · ext j      rw [freeSplit_apply_right]      simp only [Pi.single_apply,Equiv.apply_eq_iff_eq,Sum.inr_ne_inl,ite_false,Pi.zero_apply]  have freeSplit_single_right (n m : ℕ) (i : Fin m) :      freeSplit (R := R) n m (Pi.single (finSumFinEquiv (Sum.inr i)) 1)=(0,Pi.single i 1) := by    apply Prod.ext    · ext j      rw [freeSplit_apply_left]      simp only [Pi.single_apply,Equiv.apply_eq_iff_eq,Sum.inl_ne_inr,ite_false,Pi.zero_apply]    · ext j      rw [freeSplit_apply_right]      simp only [Pi.single_apply,Equiv.apply_eq_iff_eq,Sum.inr.injEq]  have Retraction.prod_matrix {M N : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] [AddCommGroup N] [Module Rᵐᵒᵖ N] (r : Retraction R M) (s : Retraction R N) :      (r.prod s).idempotent.matrix=(K0.directSum r.idempotent s.idempotent).matrix := by    ext i j    obtain ⟨i,rfl⟩ := finSumFinEquiv.surjective i    obtain ⟨j,rfl⟩ := finSumFinEquiv.surjective j    change unop ((freeSplit r.size s.size).symm ((r.inc.prodMap s.inc)      ((r.proj.prodMap s.proj) ((freeSplit r.size s.size)        (Pi.single (finSumFinEquiv j) 1)))) (finSumFinEquiv i))=      Matrix.fromBlocks (rightMatrix (r.inc.comp r.proj)) 0 0 (rightMatrix (s.inc.comp s.proj))        (finSumFinEquiv.symm (finSumFinEquiv i)) (finSumFinEquiv.symm (finSumFinEquiv j))    simp only [Equiv.symm_apply_apply]    cases i with | inl i => ?_ | inr i => ?_    all_goals cases j with | inl j => ?_ | inr j => ?_    · rw [freeSplit_single_left]      simp only [LinearMap.prodMap_apply,map_zero,freeSplit_symm_left,Matrix.fromBlocks_apply₁₁]      rfl    · rw [freeSplit_single_right]      simp only [LinearMap.prodMap_apply,map_zero,freeSplit_symm_left,Matrix.fromBlocks_apply₁₂,        Pi.zero_apply,unop_zero,Matrix.zero_apply]    · rw [freeSplit_single_left]      simp only [LinearMap.prodMap_apply,map_zero,freeSplit_symm_right,Matrix.fromBlocks_apply₂₁,        Pi.zero_apply,unop_zero,Matrix.zero_apply]    · rw [freeSplit_single_right]      simp only [LinearMap.prodMap_apply,map_zero,freeSplit_symm_right,Matrix.fromBlocks_apply₂₂]      rfl  have Retraction.prod_idempotent {M N : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] [AddCommGroup N] [Module Rᵐᵒᵖ N] (r : Retraction R M) (s : Retraction R N) :      (r.prod s).idempotent=K0.directSum r.idempotent s.idempotent := by    dsimp only [Retraction.idempotent, K0.directSum]    congr 1    exact Retraction.prod_matrix r s  have classOf_directSum (e f : K0.Idempotent R) :      K0.classOf (K0.directSum e f)=K0.classOf e+K0.classOf f := by    apply sub_eq_zero.mp    change QuotientAddGroup.mk' (K0.relations R) (FreeAbelianGroup.of (K0.directSum e f))-      (QuotientAddGroup.mk' (K0.relations R) (FreeAbelianGroup.of e)+      QuotientAddGroup.mk' (K0.relations R) (FreeAbelianGroup.of f))=0    rw [←map_add,←map_sub]    change (QuotientAddGroup.mk (FreeAbelianGroup.of (K0.directSum e f)-      (FreeAbelianGroup.of e+FreeAbelianGroup.of f)) : K0.Group R)=0    apply (QuotientAddGroup.eq_zero_iff _).mpr    rw [sub_add_eq_sub_sub]    exact AddSubgroup.subset_closure (Or.inr ⟨e,f,rfl⟩)  have Object.presentationClass_eq (P : Object.{u,v} R) (r : Retraction R P.carrier) :      P.presentationClass=K0.classOf r.idempotent := Retraction.class_eq P.retraction r  have Object.presentationClass_iso (P Q : Object.{u,v} R)      (i : P.carrier ≃ₗ[Rᵐᵒᵖ] Q.carrier) : P.presentationClass=Q.presentationClass := by    rw [Object.presentationClass_eq Q (P.retraction.transport i), Retraction.transport_idempotent]    rfl  have Object.presentationClass_prod (P Q : Object.{u,v} R) :      (P.prod Q).presentationClass=P.presentationClass+Q.presentationClass := by    calc      _ = K0.classOf (P.retraction.prod Q.retraction).idempotent :=        Object.presentationClass_eq (P.prod Q) (P.retraction.prod Q.retraction)      _ = P.presentationClass+Q.presentationClass := by        rw [Retraction.prod_idempotent,classOf_directSum]        rfl  have moduleRelations_in_kernel : moduleRelations R≤(rawPresentation.{u,v} (R := R)).ker := by    apply (AddSubgroup.closure_le _).mpr    intro x hx    rcases hx with ⟨P,Q,⟨i⟩,rfl⟩ | ⟨P,Q,rfl⟩    · change rawPresentation (FreeAbelianGroup.of P-FreeAbelianGroup.of Q)=0      simp only [map_sub,rawPresentation,FreeAbelianGroup.lift_apply_of]      exact sub_eq_zero.mpr (Object.presentationClass_iso P Q i)    · change rawPresentation        (FreeAbelianGroup.of (P.prod Q)-FreeAbelianGroup.of P-FreeAbelianGroup.of Q)=0      simp only [map_sub,rawPresentation,FreeAbelianGroup.lift_apply_of,Object.presentationClass_prod]      abel  exact QuotientAddGroup.lift (moduleRelations R) rawPresentation moduleRelations_in_kernelvariable {G : Type u} [_root_.Group G]def HattoriStallings : ModuleK0.{u,v} (MonoidAlgebra ℂ G) →+ (ConjClasses G →₀ ℂ) :=  K0.HattoriStallings.comp presentationtheorem bassTraceModules_vanishing_and_support {G : Type u} [_root_.Group G]    (x : ModuleK0.{u,v} (MonoidAlgebra ℂ G)) :    (∀ g : G, ¬IsOfFinOrder g → HattoriStallings x (ConjClasses.mk g) = 0) ∧      ↑(HattoriStallings x).support ⊆        {c | ∃ g : G, IsOfFinOrder g ∧ ConjClasses.mk g = c} :=  by sorryend RightProjectiveend BassTraceendend OAI

Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture

Theorem

Let G be any discrete group. For every x\in K_0(\C G) and every infinite-order element g\in G,

\HS_G(x)([g]_G)=0.

Equivalently, if \con_{\mathrm{fin}}(G) denotes the conjugacy classes of finite-order elements, then

\HS_G\bigl(K_0(\C G)\bigr) \subseteq\bigoplus_{C\in\con_{\mathrm{fin}}(G)}\C C.

Section 1, Introduction Read it in the paper TeX source, line 45

Show the TeX

Let $G$ be any discrete group. For every $x\in K_0(\C G)$ and every
infinite-order element $g\in G$,
\[
 \HS_G(x)([g]_G)=0.
\]
Equivalently, if $\con_{\mathrm{fin}}(G)$ denotes the conjugacy classes of
finite-order elements, then
\[
 \HS_G\bigl(K_0(\C G)\bigr)
 \subseteq\bigoplus_{C\in\con_{\mathrm{fin}}(G)}\C C.
\]

Corollary

Let G be any torsion-free discrete group.

(i)
For every q\geq1 and every idempotent e\in M_q(\C G),
\tau_{G,q}(e)=\operatorname{rank}_{\C}\bigl(\epsilon_{G,q}(e)\bigr).
Consequently \tau_{G,*}=\operatorname{rk}_{\epsilon}, with \Z viewed as a subgroup of \C, and
\tau_{G,*}\bigl(K_0(\C G)\bigr)=\Z.
(ii)
For every commutative unital domain R of characteristic zero, every e\in RG satisfying e^2=e is either 0 or 1.

Section 1, Introduction Read it in the paper TeX source, line 98

Show the TeX

Let $G$ be any torsion-free discrete group.
\begin{enumerate}[label=\textup{(\roman*)}]
 \item For every $q\geq1$ and every idempotent $e\in M_q(\C G)$,
 \[
  \tau_{G,q}(e)=\operatorname{rank}_{\C}\bigl(\epsilon_{G,q}(e)\bigr).
 \]
 Consequently $\tau_{G,*}=\operatorname{rk}_{\epsilon}$, with
 $\Z$ viewed as a subgroup of $\C$, and
 \[
  \tau_{G,*}\bigl(K_0(\C G)\bigr)=\Z.
 \]
 \item For every commutative unital domain $R$ of characteristic zero,
 every $e\in RG$ satisfying $e^2=e$ is either $0$ or $1$.
\end{enumerate}

Configuration and file facts

File: lean/ComparatorChallenges/BassTrace.lean
OpenAI’s Lean catalogue: OpenAI lists this as a main result in its Lean catalogue.
Solution module: OAI/RingTheory/BassTrace/Main.lean
Allowed axioms: propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports: Mathlib.Algebra.Group.Conj, Mathlib.Algebra.MonoidAlgebra.Basic, Mathlib.Basic.Complex.Basic, Mathlib.GroupTheory.FreeAbelianGroup, Mathlib.GroupTheory.OrderOfElement, Mathlib.LinearAlgebra.Matrix.Trace, Mathlib.LinearAlgebra.Matrix.ToLin, Mathlib.RingTheory.Finiteness.Projective, Mathlib.Tactic
Imports from outside Mathlib: None
Local vocabulary: 31 local vocabulary declarations
Lines of Lean, without comments or blank lines: 387
Second proof-verification program (nanoda): Off in OpenAI's configuration.

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas