The pro-p class module of a local absolute Galois group

Let K be a nonarchimedean local field, p a prime invertible in K (for instance the residue characteristic when K has characteristic zero), and V an open normal subgroup of G_K. This file proves that the class u_{G_K/V}(p) of the extension

1 → V^ab(p) → G_K ⧸ ⁅V, V⁆V(p) → G_K ⧸ V → 1

generates H²(G_K ⧸ V, V^ab(p)), and that this cyclic group has order the p-part of #(G_K ⧸ V). When V = G_L for a finite Galois extension L / K, local reciprocity identifies V^ab(p) with the p-adic completion of Lˣ, so this is the statement that the class of the arithmetic extension generates H²(Gal(L/K), A(L)). It is the input from strict cohomological dimension to the computation of the generator rank of G_K.

The result is the general class-module theorem TauCeti.abelianizationProPClass_generates at G_K, whose strict p-cohomological dimension is two (TauCeti.ClassFieldTheory.strictCohomologicalDimensionAt_absoluteGaloisGroup_eq_two_of_isUnit). The finite-layer form transports this class to the actual extension over Gal(L/K) along the quotient identification, retaining both generation and the exact order.

Main results

• TauCeti.galoisClassModuleExtension_contCohomologyClass_generates: the class of the actual arithmetic extension over Gal(L/K) generates, with the same exact order.
• TauCeti.contCohomologyClass_absoluteGaloisGroup_generates: u_{G_K/V}(p) generates H²(G_K ⧸ V, V^ab(p)), of order the p-part of #(G_K ⧸ V).

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.6.4)(iii), (7.2.5) and the proof of (7.4.1).

theorem TauCeti.contCohomologyClass_absoluteGaloisGroup_generates {p : ℕ} [Fact (Nat.Prime p)] {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hp : IsUnit ↑p) {V : Subgroup (Field.absoluteGaloisGroup K)} [V.Normal] (hV : IsOpen ↑V) : AddSubgroup.zmultiples (abelianizationProPClass p (Field.absoluteGaloisGroup K) V hV) = ⊤ ∧ Nat.card (ContCohomology.H2 (Field.absoluteGaloisGroup K ⧸ V) (Additive (abelianizationProP p (Field.absoluteGaloisGroup K) V))) = p ^ padicValNat p (Nat.card (Field.absoluteGaloisGroup K ⧸ V))

The class of the arithmetic extension generates. For a nonarchimedean local field K, a prime p invertible in K, and an open normal subgroup V of G_K, the class of the extension 1 → V^ab(p) → G_K ⧸ ⁅V, V⁆V(p) → G_K ⧸ V → 1 generates H²(G_K ⧸ V, V^ab(p)), a cyclic group whose order is the p-part of #(G_K ⧸ V).

theorem TauCeti.galoisClassModuleExtension_contCohomologyClass_generates {p : ℕ} [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Normal K L] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hp : IsUnit ↑p) (j : L →ₐ[K] SeparableClosure K) : let this := galoisClassModuleAction p K L j; have this_1 := ⋯; AddSubgroup.zmultiples (ProfiniteGroupExtension.contCohomologyClass (galoisClassModuleExtension p K L j)) = ⊤ ∧ Nat.card (ContCohomology.H2 Gal(L/K) (Additive (abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K L j)))) = p ^ padicValNat p (Nat.card Gal(L/K))

The class of the arithmetic pro-p extension over Gal(L/K) generates its second cohomology, a cyclic group of order the p-part of the extension degree. The coefficients are the pro-p abelianization of the subgroup fixing the embedded finite layer.