Local Tate duality for finite Galois modules

Let K be a nonarchimedean local field, n a natural number invertible in K, and μₙ the nth roots of unity of a separable closure Kˢ, the G_K-module TauCeti.KummerCoeff K n. For a finite discrete G_K-module A killed by n, write A' = Hom(A, μₙ) for its dual (the internal hom TauCeti.InternalHom) and

αᵢ : Hⁱ(G_K, A) → Hom(H²⁻ⁱ(G_K, A'), H²(G_K, μₙ)),   i = 0, 1, 2,

for Tate's duality maps (TauCeti.ContCohomology.dualityMap0, dualityMap1, dualityMap2). This file proves Tate's local duality theorem in this form: the three maps αᵢ are bijective for every such A (TauCeti.ClassFieldTheory.dualityMap0_kummerCoeff_bijective and its companions in degrees 1 and 2). No filtration of A by modules with trivial action is used, and none need exist: over ℚ₂, the unramified action of order two on ℤ/3 has none.

The proof goes up from the trivial-action case in three steps.

• Open subgroups. An open subgroup V of G_K acting trivially on μₙ is the absolute Galois group of its fixed field E, a finite extension of K containing a primitive nth root of unity ζ. Through ζ, the V-modules μₙ and ℤ/n with trivial action are isomorphic, and Tate's duality for finite modules with trivial action over E (TauCeti.ClassFieldTheory.dualityMap0_bijective_of_isPrimitiveRoot and its companions) gives the bijectivity of the three duality maps of V on every finite V-module with trivial action killed by n (TauCeti.ClassFieldTheory.dualityMap_bijective_of_smul_kummerCoeff_eq_self).
• Shapiro's lemma. Corestriction H²(V, μₙ) → H²(G_K, μₙ) is bijective (TauCeti.ClassFieldTheory.explicitCor2_kummerCoeff_bijective), so Shapiro's lemma carries this duality to the G_K-module Coind_V^{G_K} A (TauCeti.ContCohomology.dualityMap0_bijective_discreteCoind_of_bijective and its companions), which is TauCeti.ClassFieldTheory.dualityMap_bijective_discreteCoind_kummerCoeff.
• Dimension shifting. For a general finite A killed by n, choose an open normal subgroup V acting trivially on A and on μₙ. Along 0 → A → Coind_V^{G_K} A → C → 0, the four lemma and a count of orders pass from the coinduced modules to A (TauCeti.ContCohomology.dualityMap0_bijective_of_bijective_discreteCoind and its companions), using H²(G_K, μₙ) ≃ ℤ/n (TauCeti.ClassFieldTheory.h2MuEquivZMod) and the finiteness of H¹(G_K, A'), which reduces in the same way to the finiteness of H¹(V, ℤ/ℓ) = Eˣ/(Eˣ)ˡ.

The statements are made on the explicit low-degree cochain model with the single ambient coefficient module μₙ = KummerCoeff K n, which is the model of the generic duality, Shapiro and corestriction API they are assembled from.

Main results

• TauCeti.ClassFieldTheory.dualityMap_bijective_of_smul_kummerCoeff_eq_self: Tate's duality for an open subgroup of G_K acting trivially on μₙ, on its finite modules with trivial action.
• TauCeti.ClassFieldTheory.dualityMap_bijective_discreteCoind_kummerCoeff: Tate's duality for the modules coinduced from such a subgroup.
• TauCeti.ClassFieldTheory.dualityMap0_kummerCoeff_bijective, dualityMap1_kummerCoeff_bijective and dualityMap2_kummerCoeff_bijective: local Tate duality for every finite discrete G_K-module killed by n.

References

• J.-P. Serre, Galois Cohomology, Chapter II, §5.2, Theorem 2 and its proof.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (7.2.6).
• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I, Theorem 2.1 and its proof.

theorem TauCeti.ClassFieldTheory.dualityMap_bijective_of_smul_kummerCoeff_eq_self {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (V : Subgroup (AbsoluteGaloisGroup K)) (hV : IsOpen ↑V) (hVN : ∀ v ∈ V, ∀ (y : KummerCoeff K n), v • y = y) (A : Type) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥V) A] [ContinuousSMul (↥V) A] [Finite A] (hA : ∀ (a : A), n • a = 0) (hAV : ∀ (v : ↥V) (a : A), v • a = a) : Function.Bijective ⇑(ContCohomology.dualityMap0 (↥V) A (KummerCoeff K n)) ∧ Function.Bijective ⇑(ContCohomology.dualityMap1 (↥V) A (KummerCoeff K n)) ∧ Function.Bijective ⇑(ContCohomology.dualityMap2 (↥V) A (KummerCoeff K n))

Tate's duality on an open subgroup acting trivially on μₙ. Let V be an open subgroup of G_K acting trivially on μₙ, for n invertible in the local field K. For every finite discrete V-module A killed by n on which V acts trivially, the three duality maps Hⁱ(V, A) → Hom(H²⁻ⁱ(V, Hom(A, μₙ)), H²(V, μₙ)) are bijective.

theorem TauCeti.ClassFieldTheory.dualityMap_bijective_discreteCoind_kummerCoeff {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (V : Subgroup (AbsoluteGaloisGroup K)) (hV : IsOpen ↑V) (hVN : ∀ v ∈ V, ∀ (y : KummerCoeff K n), v • y = y) (A : Type) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (↥V) A] [ContinuousSMul (↥V) A] [Finite A] (hA : ∀ (a : A), n • a = 0) (hAV : ∀ (v : ↥V) (a : A), v • a = a) [V.FiniteIndex] : Function.Bijective ⇑(ContCohomology.dualityMap0 (AbsoluteGaloisGroup K) (DiscreteCoind (AbsoluteGaloisGroup K) V A) (KummerCoeff K n)) ∧ Function.Bijective ⇑(ContCohomology.dualityMap1 (AbsoluteGaloisGroup K) (DiscreteCoind (AbsoluteGaloisGroup K) V A) (KummerCoeff K n)) ∧ Function.Bijective ⇑(ContCohomology.dualityMap2 (AbsoluteGaloisGroup K) (DiscreteCoind (AbsoluteGaloisGroup K) V A) (KummerCoeff K n))

Tate's duality on a module coinduced from an open subgroup acting trivially on μₙ. Let V be an open subgroup of G_K acting trivially on μₙ, for n invertible in the local field K, and A a finite discrete V-module killed by n on which V acts trivially. Then the three duality maps of G_K are bijective on Coind_V^{G_K} A: by Shapiro's lemma they are those of V on A, followed by corestriction on H²(-, μₙ), which is bijective.

theorem TauCeti.ClassFieldTheory.dualityMap0_kummerCoeff_bijective {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (A : Type) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (AbsoluteGaloisGroup K) A] [ContinuousSMul (AbsoluteGaloisGroup K) A] [Finite A] (hA : ∀ (a : A), n • a = 0) : Function.Bijective ⇑(ContCohomology.dualityMap0 (AbsoluteGaloisGroup K) A (KummerCoeff K n))

Local Tate duality in degree zero. Let K be a nonarchimedean local field and n a natural number invertible in K. For every finite discrete G_K-module A killed by n, Tate's duality map H⁰(G_K, A) → Hom(H²(G_K, Hom(A, μₙ)), H²(G_K, μₙ)) is bijective.

theorem TauCeti.ClassFieldTheory.dualityMap1_kummerCoeff_bijective {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (A : Type) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (AbsoluteGaloisGroup K) A] [ContinuousSMul (AbsoluteGaloisGroup K) A] [Finite A] (hA : ∀ (a : A), n • a = 0) : Function.Bijective ⇑(ContCohomology.dualityMap1 (AbsoluteGaloisGroup K) A (KummerCoeff K n))

Local Tate duality in degree one. Let K be a nonarchimedean local field and n a natural number invertible in K. For every finite discrete G_K-module A killed by n, Tate's duality map H¹(G_K, A) → Hom(H¹(G_K, Hom(A, μₙ)), H²(G_K, μₙ)) is bijective.

theorem TauCeti.ClassFieldTheory.dualityMap2_kummerCoeff_bijective {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (A : Type) [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction (AbsoluteGaloisGroup K) A] [ContinuousSMul (AbsoluteGaloisGroup K) A] [Finite A] (hA : ∀ (a : A), n • a = 0) : Function.Bijective ⇑(ContCohomology.dualityMap2 (AbsoluteGaloisGroup K) A (KummerCoeff K n))

Local Tate duality in degree two. Let K be a nonarchimedean local field and n a natural number invertible in K. For every finite discrete G_K-module A killed by n, Tate's duality map H²(G_K, A) → Hom(H⁰(G_K, Hom(A, μₙ)), H²(G_K, μₙ)) is bijective.