Reducing the bound on H²(Gal(L/K), Lˣ) to subextensions of prime degree

Let L/K be a finite Galois extension of fields whose Galois group is solvable. This file shows that the order of the relative Brauer group H²(Gal(L/K), Lˣ) divides [L : K] as soon as the same holds for every Galois subextension F/E of L/K of prime degree (TauCeti.natCard_groupCohomology_two_units_dvd_finrank).

This is the field-theoretic form of the group-cohomological reduction TauCeti.groupCohomology.natCard_groupCohomology_two_dvd_natCard, whose two hypotheses about subgroups H of Gal(L/K) and their normal subgroups N are discharged by Galois theory:

• H is the Galois group of L over the fixed field E of H, so H¹(H, Lˣ) = 0 is Noether's form of Hilbert's Theorem 90 for L/E (TauCeti.isZero_groupCohomology_one_res_units, in TauCeti.FieldTheory.GaloisCohomology.Hilbert90);
• for F the fixed field of N, the quotient H ⧸ N is Gal(F/E) and the N-invariant units of L are the units of F, compatibly with the two actions, so H²(H ⧸ N, (Lˣ)^N) is H²(Gal(F/E), Fˣ) and [H : N] = [F : E].

For a finite Galois extension of nonarchimedean local fields the Galois group is solvable and every subextension is again an extension of local fields, of which those of prime degree are cyclic. So the local bound #H²(Gal(L/K), Lˣ) ∣ [L : K] reduces to cyclic extensions of prime degree, where it is a Herbrand quotient computation.

Main statements

• TauCeti.natCard_groupCohomology_two_units_dvd_finrank: if Gal(L/K) is solvable and every Galois subextension F/E of prime degree satisfies #H²(Gal(F/E), Fˣ) ∣ [F : E], then #H²(Gal(L/K), Lˣ) ∣ [L : K].

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.natCard_groupCohomology_two_units_dvd_finrank {K L : Type} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [Group.IsSolvable Gal(L/K)] (hprime : ∀ (E : IntermediateField K L) (F : IntermediateField (↥E) L) [IsGalois ↥E ↥F], Nat.Prime (Module.finrank ↥E ↥F) → Nat.card ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(↥F/↥E) (↥F)ˣ) 2) ∣ Module.finrank ↥E ↥F) : Nat.card ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2) ∣ Module.finrank K L

The bound on H²(Gal(L/K), Lˣ) reduces to subextensions of prime degree. Let L/K be a finite Galois extension with solvable Galois group. If every Galois subextension F/E of L/K of prime degree satisfies #H²(Gal(F/E), Fˣ) ∣ [F : E], then #H²(Gal(L/K), Lˣ) ∣ [L : K].