TorsionFree.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Idempotent and trace consequences for torsion-free groups.

lemma OAI.TorsionFreeBass.scalar_trace_eq_augmentation line 16
Source documentation
The scalar specialization of the identity-support trace formula.
```
lemma scalar_trace_eq_augmentation (hG : TorsionFree G)
    (e : MonoidAlgebra ℂ G) (he : e * e = e) : canonicalTrace e = augmentation e := by
…
```
Mentions: OAI.TorsionFreeBass.TorsionFree, OAI.TorsionFreeBass.canonicalTrace, OAI.TorsionFreeBass.augmentation
theorem OAI.TorsionFreeBass.complex_idempotent line 27
Source documentation
Kaplansky's scalar idempotent assertion over the complex numbers.
```
theorem complex_idempotent (hG : TorsionFree G)
    (e : MonoidAlgebra ℂ G) (he : e * e = e) : e = 0 ∨ e = 1 := by
…
```
Mentions: OAI.TorsionFreeBass.TorsionFree
theorem OAI.TorsionFreeBass.domain_idempotent line 43
Source documentation
Kaplansky's assertion over any commutative characteristic-zero domain.
```
theorem domain_idempotent (hG : TorsionFree G)
    (R : Type*) [CommRing R] [IsDomain R] [CharZero R]
    (e : MonoidAlgebra R G) (he : e * e = e) : e = 0 ∨ e = 1 :=
…
```
Mentions: OAI.TorsionFreeBass.TorsionFree
theorem OAI.TorsionFreeBass.torsion_free_corollary line 50
Source documentation
Trace/rank, equality and range on algebraic K₀, and characteristic-zero scalar idempotents for torsion-free groups.
Distinct definitions of this name: ComparatorChallenges/BassTorsionFree.lean:299 (same statement text; different proof or body). Qualify references as OAI.TorsionFreeBass.torsion_free_corollary@path.
```
theorem torsion_free_corollary (G : Type*) [Group G] (hG : TorsionFree G) :
    ((∀ (q : ℕ), 1 ≤ q →
      ∀ e : Matrix (Fin q) (Fin q) (MonoidAlgebra ℂ G), e ^ 2 = e →
        matrixTrace e = ((augmentedMatrix e).rank : ℂ)) ∧
      traceK0 (G := G) = (Int.castAddHom ℂ).comp augmentationRank ∧
…
```
Mentions: OAI.TorsionFreeBass.TorsionFree, OAI.TorsionFreeBass.matrixTrace, OAI.TorsionFreeBass.augmentedMatrix, OAI.TorsionFreeBass.traceK0