Bounding H² of a finite solvable group from its cyclic subquotients

Let A be a representation of a finite solvable group G. Suppose that H¹(H, A) = 0 for every subgroup H of G, and that for every normal subgroup N of prime index in such an H the order of H²(H ⧸ N, A^N) divides [H : N]. Then the order of H²(G, A) divides #G (natCard_groupCohomology_two_dvd_natCard); in particular H²(G, A) is finite.

This is how the upper bound #H²(Gal(L/K), Lˣ) ≤ [L : K] for a finite Galois extension of local fields is reduced to cyclic extensions of prime degree: Gal(L/K) is solvable, Hilbert's Theorem 90 gives the vanishing of H¹, and the cyclic case is a Herbrand quotient computation.

Main statements

• TauCeti.groupCohomology.natCard_groupCohomology_two_dvd_natCard: the order of H²(G, A) divides #G.

References

• J.-P. Serre, Local class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VI, §1.
• J. S. Milne, Class Field Theory, v4.03, Chapter III, §2.

theorem TauCeti.groupCohomology.natCard_groupCohomology_two_dvd_natCard {k G : Type u} [CommRing k] [Group G] [Finite G] [Group.IsSolvable G] (A : Rep.{u, u, u} k G) (h1 : ∀ (H : Type u) [inst : Group H] (f : H →* G), Function.Injective ⇑f → CategoryTheory.Limits.IsZero (groupCohomology (Rep.res f A) 1)) (hcyc : ∀ (H : Type u) [inst : Group H] (f : H →* G), Function.Injective ⇑f → ∀ (N : Subgroup H) [inst_1 : N.Normal], Nat.Prime N.index → Nat.card ↑(groupCohomology ((Rep.res f A).quotientToInvariants N) 2) ∣ N.index) : Nat.card ↑(groupCohomology A 2) ∣ Nat.card G

H² of a finite solvable group is bounded by its cyclic subquotients. Let A be a representation of a finite solvable group G. Suppose that H¹(H, A) = 0 for every subgroup H of G (given as an injective homomorphism f : H →* G), and that for every normal subgroup N of prime index in such an H, the order of H²(H ⧸ N, A^N) divides [H : N]. Then the order of H²(G, A) divides #G; in particular H²(G, A) is finite.