Cohomology maps with projective kernels

For a finite group G, a short exact sequence 0 → P → M → N → 0 with P projective over k[G] induces an isomorphism Hⁿ(G, M) ≅ Hⁿ(G, N) in every positive degree. No finiteness or projectivity assumption is needed on M or N.

In particular, a surjection from a relation module onto a completed multiplicative module with kernel ℤ_p[G] induces an isomorphism on H². This comparison preserves the coefficient map itself, which is essential when comparing the classes of group extensions.

Main results

• TauCeti.groupCohomology.isZero_succ_of_projective: projective representations of finite groups have vanishing positive-degree cohomology.
• TauCeti.groupCohomology.isIso_map_of_surjective_of_projective_ker: a surjective coefficient map with projective kernel induces an isomorphism in every positive degree.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, proof of (7.4.1).
• K. S. Brown, Cohomology of Groups, Chapter III, §6.

theorem TauCeti.groupCohomology.isZero_succ_of_projective {k G : Type u} [CommRing k] [Group G] [Finite G] (A : Rep.{u, u, u} k G) [CategoryTheory.Projective A] (n : ℕ) : CategoryTheory.Limits.IsZero (groupCohomology A (n + 1))

A projective representation of a finite group has vanishing cohomology in every positive degree.

theorem TauCeti.groupCohomology.isIso_map_of_surjective_of_projective_ker {k G : Type u} [CommRing k] [Group G] [Finite G] {M N : Type u} [AddCommGroup M] [Module (MonoidAlgebra k G) M] [AddCommGroup N] [Module (MonoidAlgebra k G) N] (f : M →ₗ[MonoidAlgebra k G] N) (hf : Function.Surjective ⇑f) [Module.Projective (MonoidAlgebra k G) ↥f.ker] (n : ℕ) : CategoryTheory.IsIso ((groupCohomology.functor k G (n + 1)).map (Rep.ofModuleMonoidAlgebra.map (ModuleCat.ofHom f)))

A surjective k[G]-linear map with projective kernel induces an isomorphism in every positive degree of group cohomology. The coefficient representations are the canonical ones attached to the two k[G]-modules.