The norm of an extension of the augmentation ideal

For a finite abelian group Q, this file proves Artin and Tate's lemma on the norm of an extension of the augmentation ideal I_Q (Rep.norm_eq_zero_of_ker_le_coinvariantsKer): if B surjects onto I_Q with a finitely generated kernel contained in I_Q B, then the norm ∑_{q ∈ Q} q kills B. Applied to the splitting module of the extension G ⧸ G'' of G^{ab}, whose kernel G' ⧸ G'' lies in I_Q B because it is generated by commutators, this is the algebraic core of the theorem that the transfer of a finite group into its commutator subgroup is trivial.

Proof

View B as a module over ℤ[Q]. Choose a basis σ of Q whose orders multiply to |Q|, lifts x i ∈ B of the generators [σ i] - 1 of I_Q, and generators of the kernel. Together they span B, and ord(σ i) • x i and the kernel generators lie in I_Q B. The determinant trick gives γ ≡ |Q| (mod I_Q) killing B. As γ also kills I_Q, it is invariant under multiplication by every [q], so it is a constant multiple of the norm element, and its augmentation |Q| makes that constant 1.

Main results

• Rep.norm_eq_zero_of_ker_le_coinvariantsKer: for a finite abelian group Q, the norm kills every extension of I_Q by a finitely generated submodule of I_Q B.

References

• E. Artin and J. Tate, Class Field Theory, Chapter XIII (the splitting-module lemma).
• D. Ferrand, La démonstration par Artin–Tate du théorème de l'idéal principal (2011), §2.

theorem Rep.norm_eq_zero_of_ker_le_coinvariantsKer {Q : Type} [CommGroup Q] [Fintype Q] (B : Rep ℤ Q) (π : B ⟶ augmentationIdeal ℤ Q) (hπ : Function.Surjective ⇑(Hom.hom π)) (hfg : (Hom.hom π).ker.FG) (hker : (Hom.hom π).ker ≤ Representation.Coinvariants.ker B.ρ) : B.ρ.norm = 0

The norm kills an extension of the augmentation ideal by part of I_Q B (Artin–Tate). Let Q be a finite abelian group and π : B → I_Q a surjection of integral representations whose kernel is finitely generated and contained in I_Q B, the span of the elements q • b - b. Then the norm ∑_{q ∈ Q} q vanishes on B.