Degree-two inflation for local maximal pro-p Galois groups

Let K be a nonarchimedean local field containing a primitive pth root of unity, for a prime p. Inflation along G_K → G_K(p) is injective on H²(-, 𝔽_p) for every field (TauCeti.inflH2AbsoluteGaloisProP_injective). This file proves that it is also surjective: by local duality H²(G_K, 𝔽_p) is one-dimensional and spanned by cup products of classes in H¹(G_K, 𝔽_p), all of which are inflated from G_K(p), since degree-one inflation is bijective and inflation commutes with the cup product.

The resulting isomorphisms in degrees one and two transport the cohomological invariants of G_K to its maximal pro-p quotient: H²(G_K(p), 𝔽_p) is one-dimensional, and the cup square on H¹(G_K(p), 𝔽_p) is perfect. These are the cohomological clauses of the Demushkin property of G_K(p); the dimension of H¹(G_K(p), 𝔽_p) is TauCeti.finrank_cohomFp_one_absoluteGaloisGroupProP_of_exists_isPrimitiveRoot.

Main definitions

• TauCeti.inflH2AbsoluteGaloisProP: degree-two inflation H²(G_K(p), 𝔽_p) ≃ H²(G_K, 𝔽_p), as a linear equivalence.

Main results

• TauCeti.inflH2AbsoluteGaloisProP_surjective_of_mu: degree-two inflation from G_K(p) to G_K is surjective.
• TauCeti.finrank_cohomFp_two_absoluteGaloisGroupProP_of_mu: H²(G_K(p), 𝔽_p) is one-dimensional.
• TauCeti.cupFp_bijective_absoluteGaloisGroupProP_of_mu: the cup square on H¹(G_K(p), 𝔽_p) is a perfect pairing.

References

• J.-P. Serre, Galois Cohomology, Chapter II, §5.6.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (7.5.11).

theorem TauCeti.inflH2AbsoluteGaloisProP_surjective_of_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (cohomFpMap p (absoluteGaloisGroupProPQuotientMap p K) 2))

Degree-two inflation from G_K(p) to G_K is surjective when the nonarchimedean local field K contains a primitive pth root of unity: every class of H²(G_K, 𝔽_p) is inflated from H²(G_K(p), 𝔽_p).

noncomputable def TauCeti.inflH2AbsoluteGaloisProP (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : ↑(cohomFp p (absoluteGaloisGroupProP p K) 2).toModuleCat ≃ₗ[ZMod p] ↑(cohomFp p (Field.absoluteGaloisGroup K) 2).toModuleCat

Degree-two inflation from the maximal pro-p quotient of the absolute Galois group of a nonarchimedean local field K containing a primitive pth root of unity: pullback along G_K → G_K(p) identifies H²(G_K(p), 𝔽_p) with H²(G_K, 𝔽_p).

@[simp]

theorem TauCeti.inflH2AbsoluteGaloisProP_apply (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) (x : ↑(cohomFp p (absoluteGaloisGroupProP p K) 2).toModuleCat) : (inflH2AbsoluteGaloisProP p K hmu) x = (CategoryTheory.ConcreteCategory.hom (cohomFpMap p (absoluteGaloisGroupProPQuotientMap p K) 2)) x

The degree-two equivalence is the usual contravariant cohomology map along G_K → G_K(p).

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

If a nonarchimedean local field K contains a primitive pth root of unity, then H²(G_K(p), 𝔽_p) is one-dimensional.

theorem TauCeti.cupFp_bijective_absoluteGaloisGroupProP_of_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : Function.Bijective ⇑(cupFp p (absoluteGaloisGroupProP p K))

The cup square on H¹(G_K(p), 𝔽_p) is a perfect pairing when the nonarchimedean local field K contains a primitive pth root of unity: a ↦ (b ↦ a ⌣ b) is a bijection from H¹(G_K(p), 𝔽_p) onto the 𝔽_p-linear maps H¹(G_K(p), 𝔽_p) → H²(G_K(p), 𝔽_p).