Restriction to a finite-index subgroup is injective on H¹
ProvedgroupCohomology.mem_coboundaries1_of_restrict_of_isUnit_indexLet be a commutative ring and a group (in the same universe), let be a -linear representation of , i.e. an object of Rep k G, and let be a subgroup of finite index whose index , viewed in via the canonical map , is a unit. Let be an element of cocycles₁ A, that is, a -cocycle for the -action on (so ), regarded as a function by coercion. Assume that the restriction of to is a coboundary: there exists with for every . The conclusion is that itself is a coboundary on all of : there exists such that for every . No normality assumption on is made, and the statement is at the level of cochains rather than cohomology classes.
This is the injectivity of the restriction map when the index is invertible in the coefficient ring, stated on representatives. It is used to compare of a decomposition group with that of a subgroup in the local bridge lemmas NumberField.PlaceDecomp.exists_unit_inv_map_delta_res_eq_theta_localBridge and its primary variant, and in groupCohomology.exists_linearEquiv_H1_of_forall_iff_of_isUnit_index.
import Mathlib set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false set_option autoImplicit false universe u open CategoryTheory groupCohomology
theorem groupCohomology.mem_coboundaries1_of_restrict_of_isUnit_index
{k G : Type u} [CommRing k] [Group G] (A : Rep.{u} k G) (S : Subgroup G)
[S.FiniteIndex] (hindex : IsUnit ((S.index : k)))
(c : cocycles₁ A) (hc : ∃ a : A, ∀ s : S, c (s : G) = A.ρ (s : G) a - a) :
∃ a : A, ∀ g : G, c g = A.ρ g a - a := by sorry