The lattice defect of the trivial module ℤ

Let G be a finite group and k a field of characteristic ℓ. The group ℤ with the trivial action of G has no ℓ-torsion, and its reduction k ⊗_ℤ (ℤ ⧸ ℓℤ) is the trivial line k. So its lattice defect is the unit 1 = [k] of the ring G₀(k[G]) (TauCeti.latticeDefect_int_eq_one).

This is the contribution of the value group whenever a G-module V is an extension of ℤ with trivial action, 0 → V₀ → V → ℤ → 0: by additivity, the defect of V is 1 plus that of V₀. The main example is the valuation sequence 0 → 𝒪[L]ˣ → Lˣ → ℤ → 0 of a Galois extension of local fields.

The action of G on ℤ is an arbitrary DistribMulAction together with the hypothesis that it is trivial, since Mathlib has no trivial-action instance on ℤ. The finiteness of ℤ ⧸ ℓℤ and of the ℓ-torsion of ℤ, which the definition of the defect asks for, are the instances TauCeti.finite_quotSMulTop_int and TauCeti.subsingleton_torsionBy_int.

Main results

• TauCeti.latticeDefect_int_eq_one: the lattice defect of ℤ with the trivial action is 1.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), §VII.3, (7.3.3) and the proof of (7.3.1).

theorem TauCeti.latticeDefect_int_eq_one (k G : Type) [Field k] [Monoid G] [Finite G] (ℓ : ℕ) [NeZero ℓ] [CharP k ℓ] [DistribMulAction G ℤ] (h : ∀ (g : G) (n : ℤ), g • n = n) : latticeDefect k G ℓ ℤ = 1

The lattice defect of ℤ with the trivial action is the class of the trivial line: in G₀(k[G]) with k of characteristic ℓ, [k ⊗_ℤ (ℤ ⧸ ℓℤ)] - [k ⊗_ℤ ℤ[ℓ]] = [k] = 1.