Documentation

TauCeti.Algebra.MonoidAlgebra.ProjectiveTrace

Characters of projective modules vanish at p-singular elements #

Let A be a commutative local ring in which the prime p is not a unit (for instance ℤ_p, or a field of characteristic p), let G be a finite group and let X be a finitely generated projective A[G]-module. Then every element g ∈ G whose order is divisible by p acts on X with trace zero.

The proof restricts X to the group algebra A[Q] of the p-part Q = ⟨q⟩ of ⟨g⟩, where g = s * q with q ≠ 1 of p-power order and s of order m prime to p, both powers of g. The ring A[Q] is local, and A[G] is free over it, so X is a free A[Q]-module of finite rank. The element s commutes with Q, so it acts A[Q]-linearly, with s ^ m = 1; as m is a unit in A, its A[Q]-trace is a constant c ∈ A. Then g acts as the scalar q times s, and the A-trace is the algebra trace Tr_{A[Q]/A}(q * c) = c * |Q| * [q = 1] = 0.

With A = ℤ_p this is the vanishing of the characters of projective ℤ_p[G]-modules away from the p-regular elements, one of the inputs to Swan's theorem that a finitely generated projective ℤ_p[G]-module is determined by its rationalization (NSW (5.6.10)(ii)).

Main results #

References #

theorem TauCeti.trace_ofModule'_eq_zero_of_dvd_orderOf {A : Type u_1} [CommRing A] [IsLocalRing A] {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_2} [Group G] [Finite G] (X : Type u_3) [AddCommMonoid X] [Module A X] [Module (MonoidAlgebra A G) X] [IsScalarTower A (MonoidAlgebra A G) X] [Module.Finite (MonoidAlgebra A G) X] [Module.Projective (MonoidAlgebra A G) X] (hp : ¬IsUnit ↑p) {g : G} (hg : p ∣ orderOf g) :

Characters of projective modules vanish at p-singular elements. Let A be a local ring in which the prime p is not a unit and G a finite group. If p divides the order of g ∈ G, then g acts with trace zero on every finitely generated projective A[G]-module.