Finiteness of H⁰ and H¹ of a finite Galois module over a local field

Let F be a nonarchimedean local field, n a natural number invertible in F, and A a finite smooth discrete G_F-module killed by n, an object of TauCeti.ClassFieldTheory.GalRep n F. This file proves that the continuous cohomology groups H⁰(G_F, A) and H¹(G_F, A) are finite (TauCeti.ClassFieldTheory.finite_continuousCohomology_of_le_one).

The proof chooses a finite Galois extension L/F inside Fˢ that contains a primitive nth root of unity and over which A becomes a trivial module: the class field TauCeti.ClassFieldTheory.classField F W of an open normal subgroup W of Gal(Fˢ/F) contained in the kernel of the action and in the stabilizer of the root of unity. The reduction TauCeti.ContinuousCohomology.finite_continuousCohomology_of_isOpen_of_normal_of_prime, through coinduction from the image in G_F of the subgroup Gal(Fˢ/L) ≅ G_L and dévissage, leaves the trivial G_L-modules of prime order ℓ ∣ n. Such a module is μ_ℓ(Lˢ), because L contains the ℓth roots of unity, and the Kummer isomorphism TauCeti.kummerIso identifies H¹(G_L, μ_ℓ) with the group Lˣ ⧸ (Lˣ)ˡ of power classes, finite since L is a local field (TauCeti.finite_H1_of_isPrimitiveRoot_of_natCard_dvd). The finite extension L is a nonarchimedean local field for the spectral norm, TauCeti.finiteExtension_isNonarchimedeanLocalField.

In degree two the same reduction applies verbatim as soon as H²(G_L, μ_ℓ) is finite. That group is the ℓ-torsion of the Brauer group of L, whose finiteness rests on the local invariant; this file does not treat degree two.

Main results

• TauCeti.ClassFieldTheory.exists_classField_trivializing: a finite smooth Galois module becomes trivial over a finite Galois extension containing the roots of unity of its exponent.
• TauCeti.ClassFieldTheory.finite_continuousCohomology_of_prime_ge_two: reduction to trivial prime-order coefficients in degrees at least two over local fields containing roots of unity.
• TauCeti.ClassFieldTheory.finite_continuousCohomology_of_le_one: Hⁱ(G_F, A) is finite for i ≤ 1 and every finite smooth discrete A : GalRep n F, n invertible in F.

References

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

theorem TauCeti.ClassFieldTheory.exists_classField_trivializing {F : Type u} [Field F] {n : ℕ} (hn : ↑n ≠ 0) (A : GalRep n F) (hA : IsSmoothDiscrete (ZMod n) A) [Finite ↑A] : ∃ (W : OpenNormalSubgroup (AbsoluteGaloisGroup F)), (∃ (ζ : ↥(classField F W)), IsPrimitiveRoot ζ n) ∧ ∀ g ∈ W, ∀ (a : ↑A), (absoluteGaloisGroupRestrictEquiv F).symm g • a = a

A finite smooth Galois module becomes trivial over a finite Galois extension containing all the roots of unity of its exponent. The extension is presented by its open normal subgroup.

theorem TauCeti.ClassFieldTheory.finite_continuousCohomology_of_prime_ge_two {F : Type u} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} (hn : ↑n ≠ 0) (A : GalRep n F) (hA : IsSmoothDiscrete (ZMod n) A) [Finite ↑A] (i : ℕ) (h : ∀ (L : Type u) [inst : Field L] [inst_1 : ValuativeRel L] [inst_2 : TopologicalSpace L] [IsNonarchimedeanLocalField L] {ζ : L}, IsPrimitiveRoot ζ n → ∀ (H : Type u) [inst_4 : Group H] [inst_5 : TopologicalSpace H] [inst_6 : IsTopologicalGroup H] [CompactSpace H] (a : AbsoluteGaloisGroup L ≃ₜ* H) (j : ℕ), 1 < j → j ≤ i → ∀ (M : Type u) [inst : AddCommGroup M] [inst_8 : TopologicalSpace M] [inst_9 : DiscreteTopology M] [inst_10 : DistribMulAction H M] [ContinuousSMul H M] [Finite M], Nat.Prime (Nat.card M) → Nat.card M ∣ n → (∀ (g : H) (m : M), g • m = m) → Finite ↑(continuousCohomology j (ofDiscreteModule ℤ H M)).toModuleCat) : Finite ↑(continuousCohomology i A).toModuleCat

Finiteness of local Galois cohomology reduces to trivial modules of prime order over local fields containing the roots of unity of the exponent. Only degrees 2 ≤ j ≤ i need arithmetic input; degree one follows from Kummer theory. The test group can be any compact topological copy of the absolute Galois group of such a field.

theorem TauCeti.ClassFieldTheory.finite_continuousCohomology_of_le_one {F : Type u} [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 ≤ 1) : Finite ↑(continuousCohomology i A).toModuleCat

Finiteness of H⁰ and H¹ of a finite Galois module over a local field. Let F be a nonarchimedean local field and n a natural number invertible in F. For every finite smooth discrete G_F-module A killed by n, the continuous cohomology Hⁱ(G_F, A) is finite for i ≤ 1.