Degree-one local Galois cohomology with trivial coefficients

For a nonarchimedean local field K and a prime p invertible in K, the continuous cohomology H¹(G_K, 𝔽_p) is finite and hence finite-dimensional. If K contains a primitive pth root of unity, Kummer theory shows that it is nontrivial, and of dimension two when p is moreover invertible in the valuation ring 𝒪[K]. If K is a finite compatible extension of ℚ_[p] containing a primitive pth root of unity, its dimension is [K : ℚ_[p]] + 2: Kummer theory identifies it with Kˣ/(Kˣ)^p, which for every finite compatible extension of ℚ_[p] has p · #μ_p(K) · p ^ [K : ℚ_[p]] elements.

These degree-one counts are the arithmetic input to generator ranks of maximal pro-p Galois quotients.

References

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

instance TauCeti.finite_cohomFp_one_absoluteGaloisGroup (p : ℕ) (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [NeZero ↑p] : Finite ↑(cohomFp p (Field.absoluteGaloisGroup K) 1).toModuleCat

Degree-one absolute Galois cohomology with trivial ℤ/p coefficients is finite when p is nonzero in the local field, even when p is not prime. At prime p, this also supplies its finite-dimensionality over 𝔽_p.

theorem TauCeti.nontrivial_cohomFp_one_absoluteGaloisGroup_of_isPrimitiveRoot (p : ℕ) (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Fact (1 < p)] {ζ : K} (hζ : IsPrimitiveRoot ζ p) : Nontrivial ↑(cohomFp p (Field.absoluteGaloisGroup K) 1).toModuleCat

If the local field contains a primitive pth root of unity with 1 < p, then H¹(G_K, ℤ/p) with trivial coefficients is nontrivial: by Kummer theory it has as many elements as Kˣ/(Kˣ)^p, a nonzero multiple of p.

theorem TauCeti.natCard_powerClassQuotient_eq_mul_pow_finrank (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [ValuativeExtension ℚ_[p] K] : Nat.card (powerClassQuotient Kˣ p) = p * Nat.card ↥(rootsOfUnity p K) * p ^ Module.finrank ℚ_[p] K

For a finite compatible extension K of ℚ_[p], the group Kˣ/(Kˣ)^p of pth power classes has p · #μ_p(K) · p ^ [K : ℚ_[p]] elements: the residue-field factor of the local count is p ^ (f · e), with f · e = [K : ℚ_[p]].

theorem TauCeti.finrank_cohomFp_one_absoluteGaloisGroup_of_isUnit_of_exists_isPrimitiveRoot (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hpK : IsUnit ↑p) (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : Module.finrank (ZMod p) ↑(cohomFp p (Field.absoluteGaloisGroup K) 1).toModuleCat = 2

Away from the residue characteristic, H¹(G_K, 𝔽_p) has dimension two when μ_p ⊆ K. This follows from Kummer theory: H¹(G_K, 𝔽_p) has as many elements as Kˣ/(Kˣ)^p, whose order is p · #μ_p(K) = p².

theorem TauCeti.finrank_cohomFp_one_absoluteGaloisGroup_of_exists_isPrimitiveRoot (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [ValuativeExtension ℚ_[p] K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : Module.finrank (ZMod p) ↑(cohomFp p (Field.absoluteGaloisGroup K) 1).toModuleCat = Module.finrank ℚ_[p] K + 2

If a finite compatible extension of ℚ_[p] contains μ_p, then dim H¹(G_K, 𝔽_p) = [K : ℚ_[p]] + 2.