Finiteness of H¹ with roots-of-unity coefficients over a local field

Let K be a nonarchimedean local field. For ℓ invertible in K the group Kˣ ⧸ (Kˣ)ˡ of power classes is finite (TauCeti.finiteIndex_range_powMonoidHom), so by the Kummer isomorphism TauCeti.kummerIso so is H¹(G_K, μ_ℓ). When K contains a primitive nth root of unity, every cyclic trivial G_K-module of order ℓ ∣ n is a copy of μ_ℓ, and its H¹ is finite. This is the input from Kummer theory to the finiteness of the Galois cohomology of a finite module over a local field.

Main results

• TauCeti.finite_H1_of_isPrimitiveRoot_of_natCard_dvd: H¹(G_K, M) is finite for every cyclic trivial discrete module M of order dividing n, when K contains a primitive nth root of unity.

References

• J.-P. Serre, Galois Cohomology, Ch. II, §5.2, proof of Proposition 14.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. VII, §1.

theorem TauCeti.finite_H1_of_isPrimitiveRoot_of_natCard_dvd (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) {H : Type u_2} [Group H] [TopologicalSpace H] (φ : AbsoluteGaloisGroup K ≃ₜ* H) (M : Type u_3) [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.H1 H M)

H¹ of a cyclic trivial module over a local field. Let K be a nonarchimedean local field containing a primitive nth root of unity, and H a topological group isomorphic to G_K. Then H¹(H, M) is finite for every cyclic discrete H-module M of order dividing n on which H acts trivially. 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.