Inflation from the maximal pro-p quotient of an absolute Galois group

For a field K and a prime p, pullback along the quotient G_K → G_K(p) identifies degree-one continuous cohomology with trivial 𝔽_p coefficients. In degree two the same inflation map is injective. These are the low-degree comparison results between the absolute Galois group and its maximal pro-p quotient, specialized from the statements TauCeti.inflH1MaximalProP and TauCeti.inflH2MaximalProP_injective for an arbitrary profinite group.

Main results

• TauCeti.inflH1AbsoluteGaloisProP: degree-one inflation from G_K(p) to G_K is a linear equivalence.
• TauCeti.inflH2AbsoluteGaloisProP_injective: degree-two inflation from G_K(p) to G_K is injective.

References

• J.-P. Serre, Galois Cohomology, Chapter I, §2.6 and §4.3.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, I §1.6.

noncomputable def TauCeti.inflH1AbsoluteGaloisProP (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) [Field K] : ↑(cohomFp p (absoluteGaloisGroupProP p K) 1).toModuleCat ≃ₗ[ZMod p] ↑(cohomFp p (Field.absoluteGaloisGroup K) 1).toModuleCat

Degree-one inflation from the maximal pro-p quotient. Pullback along G_K → G_K(p) identifies H¹(G_K(p), 𝔽_p) with H¹(G_K, 𝔽_p).

Equations

• TauCeti.inflH1AbsoluteGaloisProP p K = TauCeti.inflH1MaximalProP p (Field.absoluteGaloisGroup K)

@[simp]

theorem TauCeti.inflH1AbsoluteGaloisProP_apply (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) [Field K] (x : ↑(cohomFp p (absoluteGaloisGroupProP p K) 1).toModuleCat) : (inflH1AbsoluteGaloisProP p K) x = (CategoryTheory.ConcreteCategory.hom (cohomFpMap p (absoluteGaloisGroupProPQuotientMap p K) 1)) x

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

theorem TauCeti.inflH2AbsoluteGaloisProP_injective (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) [Field K] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (cohomFpMap p (absoluteGaloisGroupProPQuotientMap p K) 2))

Degree-two inflation from G_K(p) to G_K is injective. The inflation map H²(G_K(p), 𝔽_p) → H²(G_K, 𝔽_p) is injective.