The order of H² by local duality

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, μₙ). The (0, 2) case of local Tate duality (TauCeti.ClassFieldTheory.tateDualityPairing_perfect) identifies H⁰(F, A') with the ZMod n-dual of H²(F, A), and a finite group killed by n has as many characters with values in ZMod n as elements. So #H²(F, A) = #H⁰(F, A').

The invariants of A' are the G_F-equivariant homomorphisms A → μₙ (TauCeti.ClassFieldTheory.tateDualInvariantsEquivHom), so H⁰(F, A') = Hom_{G_F}(A, μₙ), and #H²(F, A) = #Hom_{G_F}(A, μₙ). This is how the Euler characteristic computes H² from equivariant homomorphisms into the roots of unity.

Main results

• TauCeti.ClassFieldTheory.natCard_continuousCohomology_two_eq_zero_tateDual: #H²(F, A) = #H⁰(F, Hom(A, μₙ)).
• TauCeti.ClassFieldTheory.natCard_continuousCohomology_zero_tateDual: #H⁰(F, Hom(A, μₙ)) = #Hom_{G_F}(A, μₙ), for every discrete A and every field F.
• TauCeti.ClassFieldTheory.natCard_continuousCohomology_two_eq_natCard_hom: #H²(F, A) = #Hom_{G_F}(A, μₙ).

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.3.1).
• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I, proof of Theorem 2.8.

theorem TauCeti.ClassFieldTheory.natCard_continuousCohomology_zero_tateDual {n : ℕ} {F : Type u} [Field F] (A : GalRep n F) [DiscreteTopology ↑A] : Nat.card ↑(continuousCohomology 0 (tateDual A)).toModuleCat = Nat.card (A ⟶ muNRep n F)

#H⁰(F, Hom(A, μₙ)) = #Hom_{G_F}(A, μₙ) for a discrete Galois module A: Mathlib's ContinuousCohomology.zeroIso identifies H⁰ with the invariants, and those are the equivariant homomorphisms (tateDualInvariantsEquivHom).

theorem TauCeti.ClassFieldTheory.natCard_continuousCohomology_two_eq_zero_tateDual {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)] : Nat.card ↑(continuousCohomology 2 A).toModuleCat = Nat.card ↑(continuousCohomology 0 (tateDual A)).toModuleCat

The order of H² by duality: for n invertible in the local field F and A finite smooth discrete, #H²(F, A) = #H⁰(F, Hom(A, μₙ)). The (0, 2) case of tateDualityPairing_perfect identifies H⁰(F, Hom(A, μₙ)) with the characters H²(F, A) → ZMod n, which are as many as the elements of the finite group H²(F, A), killed by n (natCard_addMonoidHom_zmod).

theorem TauCeti.ClassFieldTheory.natCard_continuousCohomology_two_eq_natCard_hom {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)] : Nat.card ↑(continuousCohomology 2 A).toModuleCat = Nat.card (A ⟶ muNRep n F)

#H²(F, A) = #Hom_{G_F}(A, μₙ) for n invertible in the local field F and A finite smooth discrete: duality in degrees (0, 2) (natCard_continuousCohomology_two_eq_zero_tateDual) and the invariants of the Tate dual (natCard_continuousCohomology_zero_tateDual).