Local Tate duality for the named evaluation pairing

Let F be a nonarchimedean local field, n a natural number invertible in F, and A a finite smooth discrete ZMod n-representation of G_F, with Tate dual A' = Hom(A, μₙ) (TauCeti.ClassFieldTheory.tateDual). For i + j = 2, the local Tate-duality pairing

Hⁱ(G_F, A') × Hʲ(G_F, A) → H²(G_F, μₙ) ≃ ZMod n

(TauCeti.ClassFieldTheory.tateDualityPairing, the cup product along the evaluation pairing followed by an identification tr of H²(G_F, μₙ) with ZMod n) induces bijections Hʲ(G_F, A) ≃ Hom(Hⁱ(G_F, A'), ZMod n): it separates the points of Hʲ(G_F, A), and every homomorphism Hⁱ(G_F, A') → ZMod n is pairing with a class of Hʲ(G_F, A) (TauCeti.ClassFieldTheory.tateDualityPairing_flip_perfect).

Finiteness of the complementary cohomology group makes the converse adjoint perfect as well: TauCeti.ClassFieldTheory.tateDualityPairing_perfect separates the classes of Hⁱ(G_F, A') and represents every character of Hʲ(G_F, A). Its mixed-characteristic specialization is TauCeti.ClassFieldTheory.tateDualityPairing_perfect_mixed.

These are Tate's duality maps αⱼ : Hʲ(G_F, A) → Hom(Hⁱ(G_F, A'), H²(G_F, μₙ)) on explicit cocycles, which are bijective (TauCeti.ClassFieldTheory.dualityMap0_kummerCoeff_bijective and its companions), read through the identification of the pairing with the explicit evaluation cup (TauCeti.ClassFieldTheory.tateDualityPairing_eq_explicitDualityPairing02 and its companions).

Main results

• TauCeti.ClassFieldTheory.tateDualityPairing_flip_perfect: for n invertible in F, the Tate-duality pairing identifies Hʲ(G_F, A) with the ZMod n-dual of Hⁱ(G_F, A').
• TauCeti.ClassFieldTheory.tateDualityPairing_perfect and tateDualityPairing_perfect_mixed: the converse adjoint is perfect, generally when n is invertible and in particular for every nonzero n in mixed characteristic.

References

• J.-P. Serre, Galois Cohomology, Chapter II, §5.2, Theorem 2.
• 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.

theorem TauCeti.ClassFieldTheory.tateDualityPairing_flip_perfect {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (hn : IsUnit ↑n) (A : GalRep n F) [DiscreteTopology ↑A] [Finite ↑A] [Fact (IsSmoothDiscrete (ZMod n) A)] (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (i j : ℕ) (hij : i + j = 2) : (∀ (y : ↑(continuousCohomology j A).toModuleCat), (∀ (x : ↑(continuousCohomology i (tateDual A)).toModuleCat), tateDualityPairing A tr i j hij x y = 0) → y = 0) ∧ ∀ (ψ : ↑(continuousCohomology i (tateDual A)).toModuleCat →+ ZMod n), ∃ (y : ↑(continuousCohomology j A).toModuleCat), ∀ (x : ↑(continuousCohomology i (tateDual A)).toModuleCat), tateDualityPairing A tr i j hij x y = ψ x

Local Tate duality for the named evaluation pairing. Let F be a nonarchimedean local field, n invertible in F, and A a finite smooth discrete ZMod n-representation of G_F, with Tate dual A' = Hom(A, μₙ). For complementary degrees i + j = 2, the Tate-duality pairing Hⁱ(G_F, A') × Hʲ(G_F, A) → ZMod n, formed with the evaluation pairing and an identification tr of H²(G_F, μₙ) with ZMod n, identifies Hʲ(G_F, A) with Hom(Hⁱ(G_F, A'), ZMod n): it separates the points of Hʲ(G_F, A), and every homomorphism Hⁱ(G_F, A') → ZMod n is pairing with some class of Hʲ(G_F, A).

theorem TauCeti.ClassFieldTheory.tateDualityPairing_perfect {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (hn : IsUnit ↑n) (A : GalRep n F) [DiscreteTopology ↑A] [Finite ↑A] [Fact (IsSmoothDiscrete (ZMod n) A)] (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (i j : ℕ) (hij : i + j = 2) : (∀ (x : ↑(continuousCohomology i (tateDual A)).toModuleCat), (∀ (y : ↑(continuousCohomology j A).toModuleCat), tateDualityPairing A tr i j hij x y = 0) → x = 0) ∧ ∀ (φ : ↑(continuousCohomology j A).toModuleCat →+ ZMod n), ∃ (x : ↑(continuousCohomology i (tateDual A)).toModuleCat), ∀ (y : ↑(continuousCohomology j A).toModuleCat), tateDualityPairing A tr i j hij x y = φ y

Perfect local Tate duality for the named evaluation pairing. Let F be a nonarchimedean local field, n invertible in F, and A a finite smooth discrete ZMod n-representation of G_F. In complementary degrees, the Tate-duality pairing separates the classes of the Tate dual and represents every ZMod n-valued character of the cohomology of A.

theorem TauCeti.ClassFieldTheory.tateDualityPairing_perfect_mixed (F : Type) [Field F] [CharZero F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (n : ℕ) (hn : n ≠ 0) (A : GalRep n F) (tr : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n) (hA : Finite ↑A) [DiscreteTopology ↑A] [Fact (IsSmoothDiscrete (ZMod n) A)] (i j : ℕ) (hij : i + j = 2) : (∀ (x : ↑(continuousCohomology i (tateDual A)).toModuleCat), (∀ (y : ↑(continuousCohomology j A).toModuleCat), tateDualityPairing A tr i j hij x y = 0) → x = 0) ∧ ∀ (φ : ↑(continuousCohomology j A).toModuleCat →+ ZMod n), ∃ (x : ↑(continuousCohomology i (tateDual A)).toModuleCat), ∀ (y : ↑(continuousCohomology j A).toModuleCat), tateDualityPairing A tr i j hij x y = φ y

Perfect local Tate duality in mixed characteristic. For a characteristic-zero nonarchimedean local field F, every finite smooth discrete ZMod n-representation has a perfect local Tate-duality pairing in complementary degrees.