The local second-cohomology bound

For a cyclic extension L/K of nonarchimedean local fields, Hilbert 90 and two-periodicity identify the order of H²(Gal(L/K), Lˣ) with the Herbrand quotient of Lˣ, and the equivariant valuation sequence gives h(Lˣ) = [L : K] · h(U_L). Since the valuation-zero units have Herbrand quotient h(U_L) = 1 (TauCeti.TateCohomology.herbrandQuotient_unitFiltration_zero), this gives

#H²(Gal(L/K), Lˣ) = [L : K].

Since two-periodicity also identifies H²(Gal(L/K), Lˣ) with the norm quotient Kˣ / N_{L/K}(Lˣ) (TauCeti.cyclicNormQuotientEquiv), this is the cyclic norm index [Kˣ : N_{L/K}(Lˣ)] = [L : K]. It is a Herbrand-quotient computation and uses no reciprocity.

For a general finite Galois extension, the local Galois group is solvable, and the field-theoretic solvable reduction propagates the prime-degree cyclic case to the bound #H²(Gal(L/K), Lˣ) ∣ [L : K]. This bounds the relative Brauer group of a finite Galois layer; compared with the unramified layer of the same degree, it shows that every local Brauer class is split by an unramified extension.

Main results

• TauCeti.natCard_H2_units_eq_finrank: #H²(Gal(L/K), Lˣ) = [L : K] for cyclic L/K.
• TauCeti.index_normGroup_of_isCyclic: [Kˣ : N_{L/K}(Lˣ)] = [L : K] for cyclic L/K.
• TauCeti.natCard_H2_units_dvd_finrank: #H²(Gal(L/K), Lˣ) ∣ [L : K] for every finite Galois L/K.

References

• J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer (1979), Chapter IX, §3 and Chapter XIII, §1.
• J.-P. Serre, Local class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VI, §1.

theorem TauCeti.natCard_H2_units_eq_finrank (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] [IsCyclic Gal(L/K)] : Nat.card ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2) = Module.finrank K L

The local H² of a cyclic extension. For a cyclic extension L/K of nonarchimedean local fields, H²(Gal(L/K), Lˣ) has order [L : K].

theorem TauCeti.index_normGroup_of_isCyclic (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] [IsCyclic Gal(L/K)] : (normGroup K L).index = Module.finrank K L

The cyclic norm index. For a cyclic extension L/K of nonarchimedean local fields, the norm group N_{L/K}(Lˣ) has index [L : K] in Kˣ.

theorem TauCeti.natCard_H2_units_dvd_finrank (K L : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [Algebra K L] [Module.Finite K L] [IsGalois K L] : Nat.card ↑(groupCohomology (Rep.ofMulDistribMulAction Gal(L/K) Lˣ) 2) ∣ Module.finrank K L

The local H² bound. For a finite Galois extension L/K of nonarchimedean local fields, the order of H²(Gal(L/K), Lˣ) divides [L : K]. The statement involves only the field structure of L (a finite Galois extension of K); no valuation or topology on L is assumed.