Corestriction in group cohomology

Let S be a subgroup of finite index in a group G and A a G-representation. The corestriction (or transfer) is the map

cor : Hⁿ(S, Res_S A) ⟶ Hⁿ(G, A)

in every degree n, going the opposite way to restriction. It is defined through Shapiro's lemma as the composite

Hⁿ(S, Res_S A) ≅ Hⁿ(G, Coind_S^G Res_S A) ⟶ Hⁿ(G, A)

of the inverse of Mathlib's Shapiro isomorphism groupCohomology.coindIso and the map induced by the trace Coind_S^G Res_S A ⟶ A, f ↦ ∑ g⁻¹ • f g over representatives of the right cosets of S, which is the counit of the finite-index adjunction Rep.coindResAdjunction. The finiteness of the index is used only for the trace.

The basic properties are proved here in every degree: corestriction is natural in the coefficients, and corestriction after restriction is multiplication by the index, cor ∘ res = [G : S]. The latter is obtained by identifying Shapiro's isomorphism with restriction followed by evaluation at 1 (TauCeti.groupCohomology.coindIso_hom): restriction then becomes the map induced by the unit A ⟶ Coind_S^G Res_S A, and the unit followed by the trace is [G : S]. Finally, corestriction is transitive along a tower A ↪ B ↪ C of embeddings with images of finite index.

Corestriction is the map along which cohomological invariants are pushed from a subgroup to the whole group; in class field theory it is the cohomological counterpart of the norm, and the normalization cor ∘ res = [G : S] is what relates the invariants of a layer to those of its restrictions.

Main definitions

• TauCeti.groupCohomology.corestrictionNatTrans k S n: corestriction, as a natural transformation from A ↦ Hⁿ(S, Res_S A) to A ↦ Hⁿ(G, A).
• TauCeti.groupCohomology.corestriction S A n: its component at A.

Main results

• TauCeti.groupCohomology.coindIso_hom_comp_corestriction: read through Shapiro's isomorphism, corestriction is the map induced by the trace.

• TauCeti.groupCohomology.map_comp_corestriction: corestriction is natural in the coefficients.

• TauCeti.groupCohomology.map_subtype_id_comp_corestriction: corestriction after restriction is multiplication by [G : S].

• TauCeti.groupCohomology.index_nsmul_eq_zero_of_map_eq_zero: a class whose restriction to S vanishes is killed by [G : S].

• groupCohomology.natCard_nsmul_eq_zero: positive-degree cohomology of a finite group is killed by the order of the group.

• TauCeti.groupCohomology.corestriction_trans: corestriction from A to B followed by corestriction from B to C is corestriction from A to C.

• TauCeti.groupCohomology.δ_comp_corestriction: corestriction commutes with the connecting maps in every ordinary cohomological degree.

• Rep.H0Iso_inv_comp_corestriction_comp_H0Iso_hom: degree-zero corestriction is the relative norm on invariants under the canonical ordinary degree-zero comparison.

References

• K. S. Brown, Cohomology of Groups, Graduate Texts in Mathematics 87, Springer (1982), Chapter III, §9.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., Grundlehren der mathematischen Wissenschaften 323, Springer (2008), Chapter I, §5.

noncomputable def TauCeti.groupCohomology.corestrictionNatTrans (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (n : ℕ) : (Rep.resFunctor S.subtype).comp (groupCohomology.functor k (↥S) n) ⟶ groupCohomology.functor k G n

Corestriction in group cohomology, natural in the coefficients: for a finite-index subgroup S ≤ G, the map Hⁿ(S, Res_S A) ⟶ Hⁿ(G, A) obtained from Shapiro's isomorphism Hⁿ(S, Res_S A) ≅ Hⁿ(G, Coind_S^G Res_S A) and the trace Coind_S^G Res_S A ⟶ A.

Equations

• TauCeti.groupCohomology.corestrictionNatTrans k S n = { app := fun (A : Rep.{?u.1, ?u.1, ?u.1} k G) => TauCeti.groupCohomology.corestrictionApp✝ k S A n, naturality := ⋯ }

noncomputable def TauCeti.groupCohomology.corestriction {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) (n : ℕ) : groupCohomology (Rep.res S.subtype A) n ⟶ groupCohomology A n

Corestriction Hⁿ(S, Res_S A) ⟶ Hⁿ(G, A) along a finite-index subgroup S ≤ G.

Equations

• TauCeti.groupCohomology.corestriction S A n = (TauCeti.groupCohomology.corestrictionNatTrans k S n).app A

@[simp]

theorem TauCeti.groupCohomology.corestrictionNatTrans_app {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) (n : ℕ) : (corestrictionNatTrans k S n).app A = corestriction S A n

The component at A of the corestriction natural transformation is corestriction S A n.

theorem TauCeti.groupCohomology.coindIso_hom_comp_corestriction {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupCohomology.coindIso (Rep.res S.subtype A) n).hom (corestriction S A n) = groupCohomology.map (MonoidHom.id G) ((Rep.coindResAdjunction k S).counit.app A) n

Corestriction through Shapiro's lemma. Precomposed with Shapiro's isomorphism Hⁿ(G, Coind_S^G Res_S A) ≅ Hⁿ(S, Res_S A), corestriction is the map induced by the trace Coind_S^G Res_S A ⟶ A, the counit of Rep.coindResAdjunction.

theorem TauCeti.groupCohomology.map_comp_corestriction {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] {A B : Rep.{u, u, u} k G} (φ : A ⟶ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id ↥S) ((Rep.resFunctor S.subtype).map φ) n) (corestriction S B n) = CategoryTheory.CategoryStruct.comp (corestriction S A n) (groupCohomology.map (MonoidHom.id G) φ n)

Corestriction is natural in the coefficients.

theorem TauCeti.groupCohomology.map_comp_corestriction_assoc {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] {A B : Rep.{u, u, u} k G} (φ : A ⟶ B) (n : ℕ) {Z : ModuleCat k} (h : groupCohomology B n ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id ↥S) (Rep.resMap S.subtype φ) n) (CategoryTheory.CategoryStruct.comp (corestriction S B n) h) = CategoryTheory.CategoryStruct.comp (corestriction S A n) (CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id G) φ n) h)

Corestriction is natural in the coefficients.

theorem TauCeti.groupCohomology.map_comp_corestriction_apply {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] {A B : Rep.{u, u, u} k G} (φ : A ⟶ B) (n : ℕ) (x : ↑(groupCohomology (Rep.res S.subtype A) n)) : (CategoryTheory.ConcreteCategory.hom (corestriction S B n)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id ↥S) (Rep.resMap S.subtype φ) n)) x) = (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id G) φ n)) ((CategoryTheory.ConcreteCategory.hom (corestriction S A n)) x)

Corestriction is natural in the coefficients.

theorem TauCeti.groupCohomology.map_subtype_id_comp_corestriction {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupCohomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A)) n) (corestriction S A n) = S.index • CategoryTheory.CategoryStruct.id (groupCohomology A n)

Corestriction after restriction is multiplication by the index: for a finite-index subgroup S ≤ G, the composite Hⁿ(G, A) ⟶ Hⁿ(S, Res_S A) ⟶ Hⁿ(G, A) of restriction and corestriction is [G : S] times the identity, in every degree n.

theorem TauCeti.groupCohomology.map_subtype_id_comp_corestriction_assoc {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) (n : ℕ) {Z : ModuleCat k} (h : groupCohomology A n ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupCohomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A)) n) (CategoryTheory.CategoryStruct.comp (corestriction S A n) h) = CategoryTheory.CategoryStruct.comp (S.index • CategoryTheory.CategoryStruct.id (groupCohomology A n)) h

Corestriction after restriction is multiplication by the index: for a finite-index subgroup S ≤ G, the composite Hⁿ(G, A) ⟶ Hⁿ(S, Res_S A) ⟶ Hⁿ(G, A) of restriction and corestriction is [G : S] times the identity, in every degree n.

theorem TauCeti.groupCohomology.map_subtype_id_comp_corestriction_apply {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] (A : Rep.{u, u, u} k G) (n : ℕ) (x : ↑(groupCohomology A n)) : (CategoryTheory.ConcreteCategory.hom (corestriction S A n)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A)) n)) x) = S.index • x

Corestriction after restriction is multiplication by the index: for a finite-index subgroup S ≤ G, the composite Hⁿ(G, A) ⟶ Hⁿ(S, Res_S A) ⟶ Hⁿ(G, A) of restriction and corestriction is [G : S] times the identity, in every degree n.

theorem TauCeti.groupCohomology.index_nsmul_eq_zero_of_map_eq_zero {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] {A : Rep.{u, u, u} k G} {n : ℕ} {x : ↑(groupCohomology A n)} (h : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A)) n)) x = 0) : S.index • x = 0

A class in Hⁿ(G, A) whose restriction to the finite-index subgroup S vanishes is killed by the index of S.

theorem TauCeti.groupCohomology.δ_comp_corestriction {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hX : X.ShortExact) (i j : ℕ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp (groupCohomology.δ ⋯ i j hij) (corestriction S X.X₁ j) = CategoryTheory.CategoryStruct.comp (corestriction S X.X₃ i) (groupCohomology.δ hX i j hij)

Corestriction from a finite-index subgroup commutes with the connecting maps of any short exact sequence of representations, in every ordinary cohomological degree.

theorem TauCeti.groupCohomology.δ_comp_corestriction_assoc {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hX : X.ShortExact) (i j : ℕ) (hij : i + 1 = j) {Z : ModuleCat k} (h : groupCohomology X.X₁ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupCohomology.δ ⋯ i j hij) (CategoryTheory.CategoryStruct.comp (corestriction S X.X₁ j) h) = CategoryTheory.CategoryStruct.comp (corestriction S X.X₃ i) (CategoryTheory.CategoryStruct.comp (groupCohomology.δ hX i j hij) h)

Corestriction from a finite-index subgroup commutes with the connecting maps of any short exact sequence of representations, in every ordinary cohomological degree.

Transitivity

theorem TauCeti.groupCohomology.corestriction_trans {k : Type u} [CommRing k] {A B C : Type u} [Group A] [Group B] [Group C] {φ₁ : A →* B} {φ₂ : B →* C} {φ₃ : A →* C} (h₁ : Function.Injective ⇑φ₁) (h₂ : Function.Injective ⇑φ₂) (h : φ₂.comp φ₁ = φ₃) [φ₁.range.FiniteIndex] [φ₂.range.FiniteIndex] (M : Rep.{u, u, u} k C) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupCohomology.mapIso (MonoidHom.ofInjective h₁) (LinearEquiv.refl k ↑M) ⋯ n).hom (CategoryTheory.CategoryStruct.comp (corestriction φ₁.range (Rep.res φ₂ M) n) (CategoryTheory.CategoryStruct.comp (groupCohomology.mapIso (MonoidHom.ofInjective h₂) (LinearEquiv.refl k ↑M) ⋯ n).hom (corestriction φ₂.range M n))) = CategoryTheory.CategoryStruct.comp (groupCohomology.mapIso (MonoidHom.ofInjective ⋯) (LinearEquiv.refl k ↑M) ⋯ n).hom (corestriction φ₃.range M n)

Transitivity of corestriction. Let φ₁ : A →* B and φ₂ : B →* C be injective with images of finite index, and let φ₃ = φ₂.comp φ₁. Identify each group with its image through MonoidHom.ofInjective. Then corestriction from A to B, followed by corestriction from B to C, is corestriction from A to C:

Hⁿ(A, M) ⟶ Hⁿ(B, M) ⟶ Hⁿ(C, M) equals Hⁿ(A, M) ⟶ Hⁿ(C, M).

The composite φ₃ is a separate argument, related to φ₂.comp φ₁ by the equation h, so the statement applies when the composite is only propositionally equal to a given homomorphism. This is the transitivity result described in Brown, Chapter III, §9, and Neukirch--Schmidt--Wingberg, Chapter I, §5.

theorem groupCohomology.natCard_nsmul_eq_zero {k G : Type u} [CommRing k] [Group G] [Finite G] {A : Rep.{u, u, u} k G} {n : ℕ} (x : ↑(groupCohomology A (n + 1))) : Nat.card G • x = 0

Positive-degree cohomology of a finite group is killed by the order of the group (Milne II 1.31).

theorem Rep.H0Iso_inv_comp_corestriction_comp_H0Iso_hom {k G : Type u} [CommRing k] [Group G] (M : Rep.{u, u, u} k G) (H : Subgroup G) [H.FiniteIndex] [Fintype (G ⧸ H)] : CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso (res H.subtype M)).inv (CategoryTheory.CategoryStruct.comp (TauCeti.groupCohomology.corestriction H M 0) (groupCohomology.H0Iso M).hom) = ModuleCat.ofHom (M.ρ.relNormInvariants H)

Under the degree-zero identification with invariants, corestriction is the relative norm. The quotient Fintype is explicit so that the relative norm uses the caller's coset enumeration.

theorem Rep.H0Iso_inv_comp_corestriction_comp_H0Iso_hom_assoc {k G : Type u} [CommRing k] [Group G] (M : Rep.{u, u, u} k G) (H : Subgroup G) [H.FiniteIndex] [Fintype (G ⧸ H)] {Z : ModuleCat k} (h : ↧↥M.ρ.invariants ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso (res H.subtype M)).inv (CategoryTheory.CategoryStruct.comp (TauCeti.groupCohomology.corestriction H M 0) (CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso M).hom h)) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (M.ρ.relNormInvariants H)) h

Under the degree-zero identification with invariants, corestriction is the relative norm. The quotient Fintype is explicit so that the relative norm uses the caller's coset enumeration.