Injectivity of inflation on H² when H¹ of the kernel vanishes
ProvedgroupCohomology.map_two_injective_of_injective_of_isZero_H1_kerLet and be finite groups, let be a surjective group homomorphism, let be a -linear representation of and one of , and let be a morphism of representations of , where is with acting through ; thus the underlying -linear map satisfies for all , . Assume that is injective on underlying modules; that every fixed by every element of lies in the image of ; and that the degree-one group cohomology of the restriction of along the inclusion , i.e. , is a zero object. The conclusion is that the underlying map of the morphism induced by the pair , namely groupCohomology.map π j 2, is injective.
This is the injectivity (inflation) half of the inflation–restriction exact sequence in degree two, in the form in which the coefficient module upstairs has its -invariants captured by and of the kernel vanishes. It is used in the computation of fundamental classes of -idèle class groups, via M4aHerbrand.exists_fundamentalClass_ideleClassGroup_map_eq_finrank_smul_of_ne_two.
import Mathlib import Definitions.Def_GroupCohomology_RelationModule import Definitions.Def_GroupCohomology_RelationModuleRes set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false set_option autoImplicit false open CategoryTheory
theorem groupCohomology.map_two_injective_of_injective_of_isZero_H1_ker {G G' : Type} [Group G] [Group G'] [Fintype G] [Fintype G']
(π : G' →* G) (hπ : Function.Surjective π)
(C : Rep ℤ G) (C' : Rep ℤ G') (j : Rep.res π C ⟶ C') (hj : Function.Injective j.hom)
(hjN : ∀ c' : C', (∀ g' : G', g' ∈ π.ker → C'.ρ g' c' = c') → c' ∈ Set.range j.hom)
(h1 : CategoryTheory.Limits.IsZero (groupCohomology (Rep.res π.ker.subtype C') 1)) :
Function.Injective (groupCohomology.map π j 2).hom := by sorry