Right exactness of local second cohomology

For finite smooth discrete coefficients of exponent invertible in a nonarchimedean local field, H² carries surjections to surjections. Consequently the long exact sequence of a short exact sequence of such coefficients terminates at H². This is the endpoint needed for multiplicativity of the three-term local Euler characteristic.

The proof uses local Tate duality for the named evaluation pairing (tateDualityPairing_flip_perfect). The dual coefficient map is injective on invariants, and characters of these invariants extend because ZMod n is self-injective. Naturality of the pairing then transports the extended character back to a second cohomology class.

Main results

• TauCeti.ClassFieldTheory.coeffMap_two_surjective: a surjective coefficient morphism induces a surjection on local H².
• TauCeti.ClassFieldTheory.explicitCoeff2_surjective: the corresponding surjectivity statement for the explicit degree-two model.

References

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

theorem TauCeti.ClassFieldTheory.coeffMap_two_surjective {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (hn : IsUnit ↑n) {B C : GalRep n F} [DiscreteTopology ↑C] [Finite ↑B] [Fact (IsSmoothDiscrete (ZMod n) B)] (f : B ⟶ C) (hf : Function.Surjective ⇑(TopRep.Hom.hom f)) : Function.Surjective ⇑(TopModuleCat.Hom.hom (ContinuousCohomology.coeffMap f 2))

A surjection from a finite smooth discrete Galois representation to a discrete representation induces a surjection on second continuous cohomology when the coefficient exponent is invertible in the local field. The target is automatically finite and smooth.

theorem TauCeti.ClassFieldTheory.explicitCoeff2_surjective {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (hn : IsUnit ↑n) {B C : GalRep n F} [Finite ↑B] [Fact (IsSmoothDiscrete (ZMod n) B)] [DiscreteTopology ↑C] (g : B ⟶ C) (hg : Function.Surjective ⇑(TopRep.Hom.hom g)) (φ : ↑B →+[Field.absoluteGaloisGroup F] ↑C) (hφ : ∀ (b : ↑B), φ b = (TopRep.Hom.hom g) b) : Function.Surjective ⇑(ContCohomology.explicitCoeff2 (Field.absoluteGaloisGroup F) (↑B) φ ⋯)

A surjection from a finite smooth discrete Galois representation to a discrete one induces a surjection on explicit H², through any equivariant additive map φ with the same underlying function. This is coeffMap_two_surjective read through the explicit degree-two comparison.