Local cohomology with trivial ℤ/n coefficients, by duality

Let K be a nonarchimedean local field and n a natural number invertible in K. Local Tate duality for the trivial module ℤ/n computes its cohomology without a primitive nth root of unity in K; its dual is Hom(ℤ/n, μₙ) = μₙ.

• In degree two, H²(G_K, ℤ/n) is dual to H⁰(G_K, μₙ) = μₙ(K), so it is finite and vanishes when K has no nth root of unity other than 1.
• In degree one, H¹(G_K, ℤ/n) is dual to H¹(G_K, μₙ), which Kummer theory identifies with Kˣ/(Kˣ)ⁿ; so the two have the same order.

For a prime p and a finite compatible extension K of ℚ_[p], combining both cases gives dim H²(G_K, 𝔽_p) (1 when μ_p ⊆ K and 0 when μ_p ⊄ K) and the Euler-characteristic identity dim H¹(G_K, 𝔽_p) = 1 + dim H²(G_K, 𝔽_p) + [K : ℚ_[p]]. When K does not contain a primitive pth root of unity, these are the inputs to the freeness of the maximal pro-p quotient of G_K and to its generator rank.

Main results

• TauCeti.finite_cohomFp_two_absoluteGaloisGroup: H²(G_K, ℤ/n) is finite when n is invertible in K.
• TauCeti.ClassFieldTheory.subsingleton_cohomFp_two_absoluteGaloisGroup: H²(G_K, ℤ/n) vanishes when μₙ(K) is trivial.
• TauCeti.ClassFieldTheory.natCard_cohomFp_one_absoluteGaloisGroup: H¹(G_K, ℤ/n) has as many elements as Kˣ/(Kˣ)ⁿ.
• TauCeti.finrank_cohomFp_one_absoluteGaloisGroup_of_isUnit_of_not_mu: away from the residue characteristic, H¹(G_K, 𝔽_p) has dimension one when K does not contain μ_p.
• TauCeti.finrank_cohomFp_one_absoluteGaloisGroup_le_two_of_coprime_ringChar: away from the residue characteristic, H¹(G_K, 𝔽_p) has dimension at most two.
• TauCeti.subsingleton_cohomFp_two_absoluteGaloisGroup_of_not_mu and TauCeti.finrank_cohomFp_two_absoluteGaloisGroup_of_not_mu: H²(G_K, 𝔽_p) = 0 for a prime p when K contains no primitive pth root of unity.
• TauCeti.finrank_cohomFp_one_absoluteGaloisGroup_of_not_mu: dim H¹(G_K, 𝔽_p) = [K : ℚ_[p]] + 1 for a finite compatible extension K of ℚ_[p] containing no primitive pth root of unity.
• TauCeti.finrank_cohomFp_one_absoluteGaloisGroup: the Euler-characteristic identity dim H¹(G_K, 𝔽_p) = 1 + dim H²(G_K, 𝔽_p) + [K : ℚ_[p]] for a finite compatible extension K of ℚ_[p].

References

• J.-P. Serre, Galois Cohomology, Chapter II, §5.2, Theorem 2, and §5.3.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (7.2.6) and (7.3.9).

theorem TauCeti.ClassFieldTheory.subsingleton_cohomFp_two_absoluteGaloisGroup {K : Type} [Field K] {n : ℕ} [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hn : IsUnit ↑n) (h : rootsOfUnity n K = ⊥) : Subsingleton ↑(cohomFp n (Field.absoluteGaloisGroup K) 2).toModuleCat

H²(G_K, ℤ/n) vanishes when K has no nontrivial nth root of unity, for a nonarchimedean local field K in which n is invertible. By local Tate duality it is dual to H⁰(G_K, Hom(ℤ/n, μₙ)), the nth roots of unity of K.

theorem TauCeti.ClassFieldTheory.natCard_cohomFp_one_absoluteGaloisGroup {K : Type} [Field K] {n : ℕ} [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hn : IsUnit ↑n) : Nat.card ↑(cohomFp n (Field.absoluteGaloisGroup K) 1).toModuleCat = Nat.card (powerClassQuotient Kˣ n)

H¹(G_K, ℤ/n) has as many elements as Kˣ/(Kˣ)ⁿ, for a nonarchimedean local field K in which n is invertible. By local Tate duality H¹(G_K, ℤ/n) is the group of homomorphisms from H¹(G_K, Hom(ℤ/n, μₙ)) = H¹(G_K, μₙ) to H²(G_K, μₙ) ≃ ℤ/n, and Kummer theory identifies H¹(G_K, μₙ) with Kˣ/(Kˣ)ⁿ, a finite group killed by n. No root of unity in K is needed.

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

Degree-two 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.subsingleton_cohomFp_two_absoluteGaloisGroup_of_not_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [NeZero ↑p] (hmu : ¬∃ (ζ : K), IsPrimitiveRoot ζ p) : Subsingleton ↑(cohomFp p (Field.absoluteGaloisGroup K) 2).toModuleCat

H²(G_K, 𝔽_p) vanishes for a nonarchimedean local field K containing no primitive pth root of unity, p being invertible in K: by local duality it is dual to μ_p(K) = 1.

theorem TauCeti.finrank_cohomFp_two_absoluteGaloisGroup_of_not_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [NeZero ↑p] (hmu : ¬∃ (ζ : K), IsPrimitiveRoot ζ p) : Module.finrank (ZMod p) ↑(cohomFp p (Field.absoluteGaloisGroup K) 2).toModuleCat = 0

If a nonarchimedean local field K contains no primitive pth root of unity, with p invertible in K, then dim H²(G_K, 𝔽_p) = 0.

theorem TauCeti.finrank_cohomFp_one_absoluteGaloisGroup_of_isUnit_of_not_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [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 = 1

Away from the residue characteristic, H¹(G_K, 𝔽_p) has dimension one when μ_p ⊄ K. This follows from local duality and Kummer theory: H¹(G_K, 𝔽_p) has as many elements as Kˣ/(Kˣ)^p, whose order is p when K has no nontrivial pth root of unity.

theorem TauCeti.finrank_cohomFp_one_absoluteGaloisGroup_le_two_of_isUnit (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hpK : IsUnit ↑p) : Module.finrank (ZMod p) ↑(cohomFp p (Field.absoluteGaloisGroup K) 1).toModuleCat ≤ 2

Away from the residue characteristic, H¹(G_K, 𝔽_p) has dimension at most two.

theorem TauCeti.finrank_cohomFp_one_absoluteGaloisGroup_le_two_of_coprime_ringChar (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hp : p.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))) : Module.finrank (ZMod p) ↑(cohomFp p (Field.absoluteGaloisGroup K) 1).toModuleCat ≤ 2

Degree-one local Galois cohomology has dimension at most two at every prime different from the residue characteristic.

theorem TauCeti.finrank_cohomFp_one_absoluteGaloisGroup_of_isUnit (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hpK : IsUnit ↑p) : Module.finrank (ZMod p) ↑(cohomFp p (Field.absoluteGaloisGroup K) 1).toModuleCat = 1 + Module.finrank (ZMod p) ↑(cohomFp p (Field.absoluteGaloisGroup K) 2).toModuleCat

Away from the residue characteristic, the Euler-characteristic identity for trivial 𝔽_p coefficients holds: dim H¹(G_K, 𝔽_p) = 1 + dim H²(G_K, 𝔽_p).

theorem TauCeti.finrank_cohomFp_one_absoluteGaloisGroup_of_not_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [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 + 1

If a finite compatible extension K of ℚ_[p] contains no primitive pth root of unity, then dim H¹(G_K, 𝔽_p) = [K : ℚ_[p]] + 1: by local duality and Kummer theory H¹(G_K, 𝔽_p) has as many elements as Kˣ/(Kˣ)^p, that is p · #μ_p(K) · p ^ [K : ℚ_[p]] with μ_p(K) = 1.

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

The Euler-characteristic identity for trivial 𝔽_p coefficients over a finite compatible extension K of ℚ_[p]: dim H¹(G_K, 𝔽_p) = 1 + dim H²(G_K, 𝔽_p) + [K : ℚ_[p]]. When μ_p ⊆ K, dim H² = 1 and dim H¹ = [K : ℚ_[p]] + 2; when μ_p ⊄ K, dim H² = 0 and dim H¹ = [K : ℚ_[p]] + 1.