Unramified Kummer classes over a local field

Let K be a nonarchimedean local field, I_K its inertia subgroup, and n a natural number prime to the residue characteristic. A class in H¹(G_K, μₙ) is unramified when its restriction to I_K vanishes. Under the Kummer isomorphism Kˣ ⧸ (Kˣ)ⁿ ≃ H¹(G_K, μₙ) these are exactly the classes of units:

the Kummer class of a ∈ Kˣ is unramified ↔ n ∣ v_K(a).

This is the local input to the finiteness of Selmer groups: a global Kummer class unramified at a finite place prime to n comes from an element whose valuation there is divisible by n, and the classes unramified outside a finite set of places are then controlled by the S-units and the S-class group.

The proof compares the Kummer cocycle g ↦ g α / α of an nth root α of a with the inertia subgroup, transported from Gal(K^{alg}/K) to AbsoluteGaloisGroup K along TauCeti.absoluteGaloisGroupRestrictEquiv. Inertia fixes the nth roots of unity, since n is prime to the residue characteristic, so on inertia a coboundary vanishes and the class restricts to zero exactly when inertia fixes α.

• If n ∣ v_K(a), then a is a unit times an nth power, so its Kummer class is that of a unit u, and the nth roots of u lie in the maximal unramified extension, which inertia fixes.
• If inertia fixes α, then K(α) is unramified over K, so the normalized valuation of K(α) restricts to that of K, and v_K(a) = v_{K(α)}(αⁿ) = n · v_{K(α)}(α).

Main results

• TauCeti.explicitRes1_kummerMap_eq_zero_iff: the Kummer class of a restricts to zero on inertia exactly when n divides the normalized valuation of a.
• TauCeti.explicitRes1_eq_zero_iff_exists_kummerMap: the classes of H¹(G_K, μₙ) vanishing on inertia are exactly the Kummer classes of units of the valuation ring.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VIII.1, proof of Proposition VIII.1.6, and X.4.

theorem TauCeti.explicitRes1_kummerMap_eq_zero_iff (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (hp : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n) (a : Kˣ) : (ContCohomology.explicitRes1 (AbsoluteGaloisGroup K) (KummerCoeff K n) (Subgroup.map (absoluteGaloisGroupRestrictEquiv K).toMonoidHom (inertiaSubgroup K))) (Multiplicative.toAdd ((kummerMap K n hn) a)) = 0 ↔ ↑n ∣ Multiplicative.toAdd ((normalizedValuation K) a)

Unramified Kummer classes. Let n be prime to the residue characteristic of the nonarchimedean local field K. The Kummer class of a ∈ Kˣ in H¹(G_K, μₙ) restricts to zero on the inertia subgroup exactly when n divides the normalized valuation of a.

theorem TauCeti.explicitRes1_eq_zero_iff_exists_kummerMap (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (hp : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n) (c : ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n)) : (ContCohomology.explicitRes1 (AbsoluteGaloisGroup K) (KummerCoeff K n) (Subgroup.map (absoluteGaloisGroupRestrictEquiv K).toMonoidHom (inertiaSubgroup K))) c = 0 ↔ ∃ u ∈ unitFiltration K 0, Multiplicative.toAdd ((kummerMap K n hn) u) = c

The unramified classes of H¹(G_K, μₙ) are the Kummer classes of units. For n prime to the residue characteristic of K, a class restricts to zero on the inertia subgroup exactly when it is the Kummer class of a unit of the valuation ring.