Duality in degree two makes H² right exact

Let 0 → A → B → C → 0 be a short exact sequence of discrete G-modules with B killed by a prime p, and let N be a discrete G-module. Tate's duality map in degree two, α₂ : H²(G, M) → Hom(H⁰(G, M'), H²(G, N)) with M' = InternalHom G M N (TauCeti.ContCohomology.dualityMap2), is natural in M: α₂ (f_* b) = α₂ b ∘ f^*, where f^* : H⁰(G, C') → H⁰(G, B') is precomposition with f = proj. If α₂ is surjective on B and injective on C, then H²(G, B) → H²(G, C) is surjective.

The argument is the one of Serre's exposé, §9.1: f^* is injective because f is surjective, and H⁰(G, B') is killed by p, so every functional on H⁰(G, C') extends along f^* to a functional on H⁰(G, B') (AddMonoidHom.exists_comp_eq_of_injective). Given y ∈ H²(G, C), extend α₂ y to ψ, lift ψ to b ∈ H²(G, B) by surjectivity, and compare α₂ (f_* b) = ψ ∘ f^* = α₂ y; injectivity gives f_* b = y.

The statement is made both on the explicit cocycle model (explicitCoeff2) and on the canonical coefficient map TauCeti.ContinuousCohomology.coeffMap in degree two, which is the form consumed by Tate's criterion TauCeti.IsProP.cohomologicalDimensionAt_le_of_forall_coeffMap_proj_surjective: perfect duality in degree two on the finite modules killed by p bounds the cohomological dimension of a pro-p group by 2.

Main results

• TauCeti.ContCohomology.DiscreteShortExact.explicitCoeff2_proj_surjective_of_dualityMap2: if α₂ is surjective on B and injective on C, then H²(G, B) → H²(G, C) is surjective, on the explicit model.
• TauCeti.ContCohomology.DiscreteShortExact.coeffMap_proj_surjective_of_dualityMap2: the same for the canonical coefficient map in degree two.

References

• J.-P. Serre, Structure de certains pro-p-groupes (d'après Demuškin), Séminaire Bourbaki 8 (1962/63), exposé 252, §9.1.

theorem TauCeti.ContCohomology.DiscreteShortExact.explicitCoeff2_proj_surjective_of_dualityMap2 {G : Type uG} [Group G] [TopologicalSpace G] [ContinuousMul G] {A : Type uA} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type uB} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type uC} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] {p : ℕ} [Fact (Nat.Prime p)] (hB : ∀ (b : B), p • b = 0) (hsurj : Function.Surjective ⇑(dualityMap2 G B N)) (hinj : Function.Injective ⇑(dualityMap2 G C N)) : Function.Surjective ⇑(explicitCoeff2 G B S.projDistribMulActionHom ⋯)

Duality in degree two makes H² right exact, on the explicit model. For a short exact sequence 0 → A → B → C → 0 of discrete G-modules with B killed by a prime p, if Tate's duality map α₂ : H²(G, M) → Hom(H⁰(G, InternalHom G M N), H²(G, N)) is surjective for M = B and injective for M = C, then H²(G, B) → H²(G, C) is surjective.

theorem TauCeti.ContCohomology.DiscreteShortExact.coeffMap_proj_surjective_of_dualityMap2 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] {A : Type u} [AddCommGroup A] [TopologicalSpace A] [DiscreteTopology A] [DistribMulAction G A] {B : Type u} [AddCommGroup B] [TopologicalSpace B] [DiscreteTopology B] [DistribMulAction G B] [ContinuousSMul G B] {C : Type u} [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] [DistribMulAction G C] [ContinuousSMul G C] (S : DiscreteShortExact G A B C) (N : Type uN) [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] {p : ℕ} [Fact (Nat.Prime p)] (hB : ∀ (b : B), p • b = 0) (hsurj : Function.Surjective ⇑(dualityMap2 G B N)) (hinj : Function.Injective ⇑(dualityMap2 G C N)) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleMap S.proj.toIntLinearMap ⋯) 2))

Duality in degree two makes H² right exact, for the canonical coefficient map. For a short exact sequence 0 → A → B → C → 0 of discrete G-modules with B killed by a prime p, if Tate's duality map α₂ is surjective for M = B and injective for M = C, then the canonical H²(G, B) → H²(G, C) is surjective. This is the hypothesis of Tate's criterion TauCeti.IsProP.cohomologicalDimensionAt_le_of_forall_coeffMap_proj_surjective in degree 2.