FormalConjectures/Arxiv/math.0703548/FarrellJonesConsequences.lean

GitHub source file

3 declarations, 2 contain sorry, 0 declared as axioms

1. def Arxiv.«math.0703548».matrixHattoriStallingsTraceAt The value at the conjugacy class of g of the universal trace of a matrix over R[G] line 47 source

   Source documentation

   The value at the conjugacy class of g of the universal trace of a matrix over R[G].

   For each diagonal entry, this sums the coefficients of the elements conjugate to g. If the matrix is idempotent, these values give the Hattori–Stallings rank of the projective module represented by the matrix.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: CommRing, Group, Fintype, Matrix, MonoidAlgebra

   Proof uses: Finset.sum, Finset.univ, Finsupp.sum, MonoidAlgebra.coeff, ite, IsConj, Classical.propDecidable, OfNat.ofNat

   10 instances, coercions and auxiliary constants left out.

   noncomputable def matrixHattoriStallingsTraceAt {R : Type*} [CommRing R] {G : Type*} [Group G]
       {n : Type*} [Fintype n] (A : Matrix n n (MonoidAlgebra R G)) (g : G) : R :=
   …

2. theorem Arxiv.«math.0703548».projective_module_isStablyFree Vanishing of the reduced projective class group for integral group rings sorry line 61 source

   Source documentation

   Vanishing of the reduced projective class group for integral group rings.

   If G is torsion-free, that is, if its only element of finite order is 1, then every finitely generated projective module over ℤ[G] is stably free. This is the stable-freeness form of the vanishing of $\widetilde K_0(\mathbb{Z}[G])$, which is the conclusion of Theorem 0.2 (ii) of [BLR08] for the regular ring $\mathbb{Z}$. That theorem assumes the K-theoretic Farrell–Jones conjecture for G with coefficients in ℤ.

   depends on sorry what this means

   Statement uses: Group, IsOfFinOrder, Eq, OfNat.ofNat, AddCommGroup, Module, MonoidAlgebra, Int, Module.Finite, Module.Projective, Module.IsStablyFree

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

   25 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem projective_module_isStablyFree {G : Type*} [Group G] (hG : ∀ g : G, IsOfFinOrder g → g = 1)
       (M : Type*) [AddCommGroup M] [Module (MonoidAlgebra ℤ G) M]
       [Module.Finite (MonoidAlgebra ℤ G) M] [Module.Projective (MonoidAlgebra ℤ G) M] :
       Module.IsStablyFree (MonoidAlgebra ℤ G) M := by
   …

3. theorem Arxiv.«math.0703548».bass_conjecture_integral_domain Bass conjecture for commutative integral domains, in idempotent-matrix form sorry line 77 source

   Source documentation

   Bass conjecture for commutative integral domains, in idempotent-matrix form.

   Let A be an idempotent matrix over R[G]. If the order of g is not invertible in R, then the Hattori–Stallings trace of the projective module represented by A vanishes at the conjugacy class of g. This includes every infinite-order g, whose orderOf is zero. This is Conjecture 0.6 of [BLR08]. By Theorems 0.5 (ii) and 0.7 of [BLR08] it follows from the Farrell–Jones conjecture with coefficients in every field of prime characteristic.

   depends on sorry what this means

   Statement uses: CommRing, IsDomain, Group, Fintype, Matrix, MonoidAlgebra, Eq, HMul.hMul, Not, IsUnit, orderOf, Arxiv.«math.0703548».matrixHattoriStallingsTraceAt, OfNat.ofNat

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

   39 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem bass_conjecture_integral_domain {R : Type*} [CommRing R] [IsDomain R] {G : Type*}
       [Group G] {n : Type*} [Fintype n] (A : Matrix n n (MonoidAlgebra R G))
       (hA : A * A = A) (g : G) (hg : ¬IsUnit (orderOf g : R)) :
       matrixHattoriStallingsTraceAt A g = 0 := by
   …

   Mentions: Arxiv.«math.0703548».matrixHattoriStallingsTraceAt