Finiteness of local Galois cohomology through degree two

For a nonarchimedean local field F, every finite smooth discrete Galois module killed by an integer invertible in F has finite cohomology in degrees zero, one and two. In particular this includes every nonzero exponent over a field of characteristic zero, even an exponent divisible by the residue characteristic.

The degree-two arithmetic input is the local Brauer invariant: Kummer theory embeds H²(G_F, μₙ) in Br F, and its invariant lies in the finite n-torsion subgroup of ℚ/ℤ. Over a finite extension containing the roots of unity, every trivial module of prime order is a roots-of-unity module. The open-normal-subgroup finiteness theorem then uses Shapiro and coinduction to pass to arbitrary finite coefficients. This does not require a filtration by trivial modules for the original Galois action.

The construction uses h2MuToBr, invMap, and ContinuousCohomology.finite_continuousCohomology_of_isOpen_of_normal_of_prime.

Main results

• finite_continuousCohomology_muNRep_two: finiteness with roots-of-unity coefficients.
• finite_H2_of_isPrimitiveRoot_of_natCard_dvd: finiteness for cyclic trivial coefficients.
• finite_H: finiteness with arbitrary finite smooth discrete coefficients through degree two.

References

• J.-P. Serre, Galois Cohomology, Chapter II, §5.2, Proposition 14.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter VII, §1, and (6.2.1) for the Kummer sequence.

theorem TauCeti.ClassFieldTheory.finite_continuousCohomology_muNRep_two {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} (hn : IsUnit ↑n) : Finite ↑(continuousCohomology 2 (muNRep n F)).toModuleCat

Roots-of-unity cohomology in degree two is finite when the exponent is invertible in the local field, since its Brauer invariant is killed by that exponent.

theorem TauCeti.ClassFieldTheory.finite_H2_of_isPrimitiveRoot_of_natCard_dvd {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) {H : Type} [Group H] [TopologicalSpace H] [ContinuousMul H] (φ : AbsoluteGaloisGroup F ≃ₜ* H) (M : Type) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction H M] [IsAddCyclic M] (hMn : Nat.card M ∣ n) (htriv : ∀ (h : H) (m : M), h • m = m) (x✝ : ContinuousSMul H M := ⋯) : Finite (ContCohomology.H2 H M)

Degree-two cohomology of a cyclic trivial module of order dividing n is finite over a local field containing a primitive nth root of unity. The group may be any topological copy of G_F. Continuity of the action, needed to state H²(H, M), holds automatically because the action is trivial; the final argument defaults to that proof, so callers never need to supply it.

theorem TauCeti.ClassFieldTheory.finite_H {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} (hn : ↑n ≠ 0) (A : GalRep n F) (hA : IsSmoothDiscrete (ZMod n) A) [Finite ↑A] {i : ℕ} (hi : i ≤ 2) : Finite ↑(continuousCohomology i A).toModuleCat

Cohomology in degrees zero through two of a finite smooth discrete Galois module over a nonarchimedean local field is finite, provided its exponent is invertible in the field.