Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.CohomologicalDimension.RightExact

Right exactness of Hⁿ on finite discrete G-modules killed by p kills Hⁿ⁺¹ #

Let G be a profinite group, p a natural number and n a degree. Suppose that the functor Hⁿ(G, -) is right exact on the finite discrete G-modules killed by p: for every short exact sequence 0 → A → B → C → 0 of such modules the map Hⁿ(G, B) → Hⁿ(G, C) is surjective. Then Hⁿ⁺¹(G, M) vanishes for every finite discrete G-module M killed by p.

The argument is the standard effaceability argument. A class x of Hⁿ⁺¹(G, M) restricts to zero on some open subgroup V of G (TauCeti.ContinuousCohomology.exists_openSubgroup_res_eq_zero). The unit M → Coind_V^G M of coinduction embeds M into a module which is again finite and killed by p, with a finite quotient Q killed by p, and under Shapiro's lemma the image of x in Hⁿ⁺¹(G, Coind_V^G M) ≅ Hⁿ⁺¹(V, M) is its restriction to V (TauCeti.ContinuousCohomology.coeffMap_unit_comp_shapiroMap), which is zero. So x is the image under the connecting map of a class of Hⁿ(G, Q), and right exactness lifts that class to Hⁿ(G, Coind_V^G M), where the connecting map kills it. Hence x = 0.

For a pro-p group this bounds the p-cohomological dimension: cd_p G ≤ n (TauCeti.IsProP.cohomologicalDimensionAt_le_of_forall_coeffMap_proj_surjective, in TauCeti.Topology.Algebra.Group.Profinite.ProP.CohomologicalDimension). This is the final step of Tate's proof that an infinite Demushkin group has cohomological dimension 2, recorded in Serre's Bourbaki exposé, §9.1: the duality pairings make H²(G, -) right exact on the finite 𝔽_p[G]-modules, and right exactness kills H³.

Main results #

References #

theorem TauCeti.subsingleton_continuousCohomology_succ_of_forall_coeffMap_proj_surjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {n : ℕ} (h : ∀ (A B C : Type u) [inst : AddCommGroup A] [inst_1 : TopologicalSpace A] [inst_2 : DiscreteTopology A] [inst_3 : DistribMulAction G A] [ContinuousSMul G A] [Finite A] [inst_6 : AddCommGroup B] [inst_7 : TopologicalSpace B] [inst_8 : DiscreteTopology B] [inst_9 : DistribMulAction G B] [ContinuousSMul G B] [Finite B] [inst_12 : AddCommGroup C] [inst_13 : TopologicalSpace C] [inst_14 : DiscreteTopology C] [inst_15 : DistribMulAction G C] [ContinuousSMul G C] [Finite C] (S : ContCohomology.DiscreteShortExact G A B C), (∀ (a : A), p • a = 0) → (∀ (b : B), p • b = 0) → (∀ (c : C), p • c = 0) → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleMap S.proj.toIntLinearMap ⋯) n))) (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] (hM : ∀ (m : M), p • m = 0) :

Right exactness of Hⁿ on finite discrete G-modules killed by p kills Hⁿ⁺¹. Let G be a profinite group and p a natural number. If for every short exact sequence 0 → A → B → C → 0 of finite discrete G-modules killed by p the map Hⁿ(G, B) → Hⁿ(G, C) is surjective, then Hⁿ⁺¹(G, M) vanishes for every finite discrete G-module M killed by p.