The transfer into the commutator subgroup is trivial

Let G be a group whose commutator subgroup G' is finitely generated and of finite index, for instance a finite group. Furtwängler's theorem, the group-theoretic form of the principal ideal theorem of class field theory, says that the transfer V : G → G' ⧸ G'' is trivial; equivalently, the transfer into G' of every homomorphism from G' to a commutative group is trivial (MonoidHom.transfer_commutator_eq_one).

Artin reduced the principal ideal theorem to this statement: if H is the Hilbert class field of a number field K and H' that of H, then G = Gal(H'/K) has G' = Gal(H'/H), and the transfer G^{ab} → G' ⧸ G'' corresponds under the Artin map to the extension of ideals from K to H.

Proof

The proof is the one of Artin and Tate, in the form given by Ferrand. Put Q = G^{ab} and A = G' ⧸ G'', a Q-module by conjugation (Abelianization.of_smul_of). Quotient representatives out q ∈ G give the factor set f(σ, τ) = out σ · out τ · out (στ)⁻¹ of the extension G ⧸ G'' of Q by A, a 2-cocycle, and the transfer of a representative is a column sum of it (MonoidHom.transfer_eq_prod_mul_out):

V(out p) = ∑_{q ∈ Q} f(q, p).

Let B be the splitting module of the class of f (Rep.splittingModule), an extension of the augmentation ideal I_Q by A in which f is the coboundary of a cochain ψ. Then ∑_q f(q, p) is ∑_q (q ψ(p) - ψ(qp) + ψ(q)) = N ψ(p) for the norm N = ∑_q q. Commutators in G have classes in I_Q B, because f(σ, τ) - f(τ, σ) is the class of ⁅out σ, out τ⁆; as A is generated by commutators, A ⊆ I_Q B. Artin and Tate's lemma (Rep.norm_eq_zero_of_ker_le_coinvariantsKer) then makes N vanish on B, so the transfer of each representative is trivial. The transfer kills G', which completes the proof.

Main results

• MonoidHom.transfer_commutator_eq_one: the transfer of a homomorphism from G' to a commutative group is trivial.

Implementation notes

The splitting module and the coefficient module A are representations over ℤ, so G lives in Type, as for TauCeti.FactorSet.cohomologyClass.

References

• Ph. Furtwängler, Beweis des Hauptidealsatzes für die Klassenkörper algebraischer Zahlkörper, Abh. Math. Sem. Hamburg 7 (1929).
• E. Artin and J. Tate, Class Field Theory, Chapter XIII.
• D. Ferrand, La démonstration par Artin–Tate du théorème de l'idéal principal (2011).
• J. Neukirch, Algebraic Number Theory, Chapter VI, Theorem 7.6.

theorem MonoidHom.transfer_commutator_eq_one {G : Type} [Group G] [Group.FG ↥(commutator G)] [(commutator G).FiniteIndex] {A : Type u_1} [CommGroup A] (ϕ : ↥(commutator G) →* A) : ϕ.transfer = 1

Furtwängler's theorem, the group-theoretic principal ideal theorem: if the commutator subgroup G' of G is finitely generated and of finite index (for instance if G is finite), the transfer G → A of every homomorphism ϕ : G' →* A to a commutative group is trivial. For ϕ the abelianization map, this says that the transfer G → G' ⧸ G'' is trivial.