TraceRank.lean`

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Canonical trace, augmentation rank and algebraic K₀.

def OAI.TorsionFreeBass.TorsionFree line 13
Source documentation
A group is torsion-free when its only finite-order element is the identity. This is the usual group-theoretic condition, not the stronger unique-roots condition.
Also declared: ComparatorChallenges/BassTorsionFree.lean:196 (same declaration text).
```
def TorsionFree (G : Type*) [Group G] : Prop := ∀ g : G, IsOfFinOrder g → g = 1
…
```
def OAI.TorsionFreeBass.augmentation line 18
Source documentation
The sum of coefficients, or augmentation, of the complex group algebra.
Also declared: ComparatorChallenges/BassTorsionFree.lean:201 (same declaration text).
```
def augmentation : MonoidAlgebra ℂ G →+* ℂ :=
…
```
lemma OAI.TorsionFreeBass.augmentation_apply line 21
def OAI.TorsionFreeBass.canonicalTrace line 26
Source documentation
The canonical trace is the coefficient of the identity.
Also declared: ComparatorChallenges/BassTorsionFree.lean:205 (same declaration text).
```
def canonicalTrace (a : MonoidAlgebra ℂ G) : ℂ := a.coeff 1
```
def OAI.TorsionFreeBass.matrixTrace line 29
Source documentation
The matrix trace obtained by applying the canonical trace to each diagonal entry.
Also declared: ComparatorChallenges/BassTorsionFree.lean:208 (same declaration text).
```
def matrixTrace {q : ℕ} (e : Matrix (Fin q) (Fin q) (MonoidAlgebra ℂ G)) : ℂ :=
…
```
def OAI.TorsionFreeBass.augmentedMatrix line 33
Source documentation
Entrywise augmentation.
Also declared: ComparatorChallenges/BassTorsionFree.lean:212 (same declaration text).
```
def augmentedMatrix {m n : ℕ} (e : Matrix (Fin m) (Fin n) (MonoidAlgebra ℂ G)) :
    Matrix (Fin m) (Fin n) ℂ := e.map augmentation
```
Mentions: OAI.TorsionFreeBass.augmentation
lemma OAI.TorsionFreeBass.canonicalTrace_eq_classCoefficient line 36
lemma OAI.TorsionFreeBass.matrixTrace_eq_classCoefficient line 40
lemma OAI.TorsionFreeBass.augmentedMatrix_mul line 45
Also declared: ComparatorChallenges/BassTorsionFree.lean:215 (same declaration text).
lemma OAI.TorsionFreeBass.augmentedMatrix_trace line 51
Also declared: ComparatorChallenges/BassTorsionFree.lean:221 (same declaration text).
lemma OAI.TorsionFreeBass.idempotent_matrix_trace_eq_rank line 56
Distinct definitions of this name: ComparatorChallenges/BassTorsionFree.lean:226 (same statement text; different proof or body). Qualify references as OAI.TorsionFreeBass.idempotent_matrix_trace_eq_rank@path.
lemma OAI.TorsionFreeBass.classTrace_sum line 64
lemma OAI.TorsionFreeBass.matrix_trace_eq_augmentation line 70
Source documentation
Bass support reduces to the identity conjugacy class in a torsion-free group.
```
lemma matrix_trace_eq_augmentation (hG : TorsionFree G) {q : ℕ}
    (e : Matrix (Fin q) (Fin q) (MonoidAlgebra ℂ G)) (he : e * e = e) :
    matrixTrace e = augmentation (Matrix.trace e) := by
…
```
Mentions: OAI.TorsionFreeBass.TorsionFree, OAI.TorsionFreeBass.matrixTrace, OAI.TorsionFreeBass.augmentation
theorem OAI.TorsionFreeBass.matrix_trace_eq_rank line 89
Source documentation
The matrix assertion holds also for the empty matrix.
```
theorem matrix_trace_eq_rank (hG : TorsionFree G) {q : ℕ}
    (e : Matrix (Fin q) (Fin q) (MonoidAlgebra ℂ G)) (he : e * e = e) :
    matrixTrace e = ((augmentedMatrix e).rank : ℂ) := by
…
```
Mentions: OAI.TorsionFreeBass.TorsionFree, OAI.TorsionFreeBass.matrixTrace, OAI.TorsionFreeBass.augmentedMatrix
def OAI.TorsionFreeBass.rawAugmentationRank line 100
Source documentation
The augmentation rank on the free abelian group of idempotents, before imposing isomorphism and direct-sum relations.
Also declared: ComparatorChallenges/BassTorsionFree.lean:237 (same declaration text).
```
def rawAugmentationRank : FreeAbelianGroup (Idempotent (MonoidAlgebra ℂ G)) →+ ℤ :=
…
```
lemma OAI.TorsionFreeBass.rawAugmentationRank_of line 103
Also declared: ComparatorChallenges/BassTorsionFree.lean:240 (same declaration text).
lemma OAI.TorsionFreeBass.augmentationRank_relations line 111
Also declared: ComparatorChallenges/BassTorsionFree.lean:248 (same declaration text).
def OAI.TorsionFreeBass.augmentationRank line 132
Source documentation
The integer-valued augmentation rank on the usual idempotent presentation of algebraic K₀: on a generator it is the complex dimension of the augmented image.
Distinct definitions of this name: ComparatorChallenges/BassTorsionFree.lean:269 (same statement text; different proof or body). Qualify references as OAI.TorsionFreeBass.augmentationRank@path.
```
def augmentationRank : BassTrace.K0.Group (MonoidAlgebra ℂ G) →+ ℤ :=
…
```
lemma OAI.TorsionFreeBass.augmentationRank_classOf line 136
lemma OAI.TorsionFreeBass.traceK0_relations line 141
Also declared: ComparatorChallenges/BassTorsionFree.lean:274 (same declaration text).
def OAI.TorsionFreeBass.traceK0 line 160
Source documentation
Coefficient at the identity class of the Hattori--Stallings trace on K₀.
Also declared: ComparatorChallenges/BassTorsionFree.lean:293 (same declaration text).
```
def traceK0 : BassTrace.K0.Group (MonoidAlgebra ℂ G) →+ ℂ :=
…
```
lemma OAI.TorsionFreeBass.traceK0_classOf line 164
theorem OAI.TorsionFreeBass.traceK0_eq_augmentationRank line 169
Source documentation
The maps agree, with the integers included in the complex numbers.
```
theorem traceK0_eq_augmentationRank (hG : TorsionFree G) :
    traceK0 (G := G) = (Int.castAddHom ℂ).comp augmentationRank := by
…
```
Mentions: OAI.TorsionFreeBass.TorsionFree, OAI.TorsionFreeBass.traceK0
def OAI.TorsionFreeBass.unitIdempotent line 186
Source documentation
The free module of rank one, represented by the one by one identity matrix.
```
def unitIdempotent : BassTrace.K0.Idempotent (MonoidAlgebra ℂ G) where
…
```
Mentions: OAI.BassTrace.K0.Idempotent
lemma OAI.TorsionFreeBass.traceK0_unit line 191
theorem OAI.TorsionFreeBass.traceK0_range line 197
Source documentation
Its image is exactly the subgroup of integers.
```
theorem traceK0_range (hG : TorsionFree G) :
    Set.range (traceK0 (G := G)) = Set.range (fun z : ℤ => (z : ℂ)) := by
…
```
Mentions: OAI.TorsionFreeBass.TorsionFree, OAI.TorsionFreeBass.traceK0