Shapiro's isomorphism is restriction followed by evaluation

For a subgroup S ≤ G and an S-representation A, Mathlib's Shapiro isomorphism groupCohomology.coindIso A n : Hⁿ(G, Coind_S^G A) ≅ Hⁿ(S, A) is constructed through Ext: it compares the bar resolution of S with the restriction to S of the bar resolution of G. This file identifies it with an explicit map. It is the change-of-group map

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

restriction to S followed by the counit Res_S Coind_S^G A ⟶ A of restriction–coinduction, which evaluates a function G → A at 1. On inhomogeneous cochains it sends c : Gⁿ → Coind_S^G A to (s₁, …, sₙ) ↦ c (s₁, …, sₙ) 1.

The explicit form is what makes Shapiro's isomorphism usable against the rest of Mathlib's functoriality: it is a groupCohomology.map, so it composes with restriction and coefficient maps by groupCohomology.map_comp. In particular it is what identifies restriction with the unit of the adjunction under Shapiro's lemma, the step that turns the counit of the finite-index adjunction into a corestriction satisfying cor ∘ res = [G : S].

Main results

• TauCeti.groupCohomology.coindIso_hom: (coindIso A n).hom is groupCohomology.map S.subtype ((resCoindAdjunction k S.subtype).counit.app A) n.

• TauCeti.groupCohomology.coindIso_hom_naturality: consequently, Shapiro's isomorphism is natural in the coefficients.

• TauCeti.groupCohomology.map_unit_comp_coindIso_hom: read through Shapiro's isomorphism, restriction to S is the map induced by the unit B ⟶ Coind_S^G Res_S B.

• TauCeti.groupCohomology.δ_comp_coindIso_hom: Shapiro's isomorphism intertwines the connecting maps of a short exact sequence and its coinduction.

References

• K. S. Brown, Cohomology of Groups, Graduate Texts in Mathematics 87, Springer (1982), Chapter III, §6 (Shapiro's lemma) and Chapter III, §8.

theorem TauCeti.groupCohomology.coindIso_hom {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) (A : Rep.{u, u, u} k ↥S) (n : ℕ) : (groupCohomology.coindIso A n).hom = groupCohomology.map S.subtype ((Rep.resCoindAdjunction k S.subtype).counit.app A) n

Shapiro's isomorphism is restriction followed by evaluation at 1. The isomorphism Hⁿ(G, Coind_S^G A) ≅ Hⁿ(S, A) of groupCohomology.coindIso is the change-of-group map along S ≤ G induced by the counit Res_S Coind_S^G A ⟶ A of restriction–coinduction.

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

Shapiro's isomorphism is natural in the coefficients: for a morphism φ : A ⟶ B of S-representations, it intertwines the maps induced by Coind_S^G φ and by φ.

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

Shapiro's isomorphism is natural in the coefficients: for a morphism φ : A ⟶ B of S-representations, it intertwines the maps induced by Coind_S^G φ and by φ.

theorem TauCeti.groupCohomology.map_unit_comp_coindIso_hom {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) (B : Rep.{u, u, u} k G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id G) ((Rep.resCoindAdjunction k S.subtype).unit.app B) n) (groupCohomology.coindIso (Rep.res S.subtype B) n).hom = groupCohomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype B)) n

Restriction through Shapiro's lemma. For a G-representation B, the map induced by the unit B ⟶ Coind_S^G Res_S B of restriction–coinduction, followed by Shapiro's isomorphism, is restriction Hⁿ(G, B) ⟶ Hⁿ(S, Res_S B).

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

Shapiro's isomorphism intertwines the connecting maps of a short exact sequence and its coinduction to the ambient group.

theorem TauCeti.groupCohomology.δ_comp_coindIso_hom_assoc {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k ↥S)} (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 (groupCohomology.coindIso X.X₁ j).hom h) = CategoryTheory.CategoryStruct.comp (groupCohomology.coindIso X.X₃ i).hom (CategoryTheory.CategoryStruct.comp (groupCohomology.δ hX i j hij) h)

Shapiro's isomorphism intertwines the connecting maps of a short exact sequence and its coinduction to the ambient group.