Reduction classes of ZMod n-representations

A representation ρ of G over ZMod n is in particular a representation on an abelian group, ρ.restrictScalars ℤ. Its reduction ZMod n ⊗_ℤ W is W again: since every element of ZMod n is the image of an integer, Mathlib's TensorProduct.lidOfCompatibleSMul identifies ZMod n ⊗_ℤ W with W by r ⊗ w ↦ r • w, and this identification is G-equivariant (Representation.baseChangeRestrictScalarsIntEquiv, in TauCeti.RepresentationTheory.BaseChange). Hence the reduction class of ρ.restrictScalars ℤ in G₀(ZMod n[G]) is the class of ρ itself (TauCeti.reductionK0_restrictScalars).

This is how the reduction classes computed for groups such as Lˣ ⧸ (Lˣ)^ℓ, which are naturally ZMod ℓ-modules, are compared with the classes of the corresponding ZMod ℓ-representations.

theorem TauCeti.reductionK0_restrictScalars {n : ℕ} {G : Type} [Monoid G] {W : Type} [AddCommGroup W] [Module (ZMod n) W] [Module.Finite (ZMod n) W] (ρ : Representation (ZMod n) G W) : reductionK0 (ZMod n) (Representation.restrictScalars ℤ ρ) = ExactK0.of ↧ρ.asModule

The reduction class of a ZMod n-representation is its class. In G₀(ZMod n[G]), the class of ZMod n ⊗_ℤ W is the class of the ZMod n[G]-module of ρ.