Transport of Hⁿ along an isomorphism of group–module pairs
ProvedgroupCohomology.nonempty_linearEquiv_of_iso_res_mulEquivLet be a commutative ring, let and be groups, let be an isomorphism of groups, let be a -linear representation of and a -linear representation of , and let be an isomorphism in the category of -linear representations of from to Rep.res e.toMonoidHom B, that is, to regarded as a -representation via the monoid homomorphism underlying . Let be a natural number. The assertion is that there exists a -linear equivalence from the -th group cohomology onto whose inverse is given, on every element of , by the underlying map of the functoriality morphism groupCohomology.map attached to the pair consisting of the monoid homomorphism underlying and the morphism of -representations, in degree . Thus the conclusion records not merely that the two cohomology modules are isomorphic as -modules, but that the inverse of the exhibited equivalence is pinned to the canonical map induced by .
This is the standard statement that group cohomology, being contravariant in the group and covariant in the coefficient module, is invariant under an isomorphism of pairs . It serves as a transport lemma: results about proved for one model of a Galois group and its coefficient module (for instance an idèle class group, or coefficients restricted along an identification of Galois groups) are carried over to an isomorphic model, and it is used in this form by the Herbrand-quotient and descent computations of the development.
import Mathlib set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false set_option autoImplicit false open CategoryTheory groupCohomology Rep
theorem groupCohomology.nonempty_linearEquiv_of_iso_res_mulEquiv
{k G H : Type} [CommRing k] [Group G] [Group H]
(e : G ≃* H) (A : Rep k G) (B : Rep k H) (φ : A ≅ Rep.res e.toMonoidHom B) (n : ℕ) :
∃ ψ : groupCohomology A n ≃ₗ[k] groupCohomology B n,
∀ x : groupCohomology B n,
ψ.symm x = (groupCohomology.map e.toMonoidHom (φ.inv : Rep.res e.toMonoidHom B ⟶ A) n).hom x := by sorry