The inverse of Shapiro's isomorphism in homology is the corestriction of the unit

For a subgroup S ≤ G and an S-representation A, Mathlib's homological Shapiro isomorphism groupHomology.indIso A n : Hₙ(G, Ind_S^G A) ≅ Hₙ(S, A) is constructed through Tor: it compares the bar resolution of S with the restriction to S of the bar resolution of G. This file identifies its inverse with an explicit map. It is the change-of-group map

Hₙ(S, A) ⟶ Hₙ(G, Ind_S^G A)

along S ≤ G, induced by the unit A ⟶ Res_S Ind_S^G A, a ↦ 1 ⊗ a, of induction–restriction. On inhomogeneous chains it sends a · (s₁, …, sₙ) to (1 ⊗ a) · (s₁, …, sₙ).

The explicit form is what makes Shapiro's isomorphism usable against the rest of Mathlib's functoriality: its inverse is a groupHomology.map, so it composes with corestriction and coefficient maps by groupHomology.map_comp. In particular, corestriction from S to G becomes the map induced by the counit Ind_S^G Res_S B ⟶ B, which is what gives the homological transfer the normalization cor ∘ res = [G : S].

This is the homological counterpart of TauCeti.groupCohomology.coindIso_hom.

Main results

• TauCeti.groupHomology.indIso_inv: (indIso A n).inv is groupHomology.map S.subtype ((indResAdjunction k S.subtype).unit.app A) n.
• TauCeti.groupHomology.indIso_inv_comp_map_counit: read through Shapiro's isomorphism, corestriction from S to G is the map induced by the counit Ind_S^G Res_S B ⟶ B.
• TauCeti.groupHomology.indIso_inv_naturality, TauCeti.groupHomology.indIso_hom_naturality: Shapiro's isomorphism is natural in the coefficients.

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.groupHomology.indIso_inv {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (S : Subgroup G) (A : Rep.{u, u, u} k ↥S) (n : ℕ) : (groupHomology.indIso S A n).inv = groupHomology.map S.subtype ((Rep.indResAdjunction k S.subtype).unit.app A) n

The inverse of Shapiro's isomorphism in homology is corestriction of the unit. The inverse of the isomorphism Hₙ(G, Ind_S^G A) ≅ Hₙ(S, A) of groupHomology.indIso is the change-of-group map along S ≤ G induced by the unit A ⟶ Res_S Ind_S^G A, a ↦ 1 ⊗ a, of induction–restriction. The DecidableEq G instance is the one used by Mathlib's indIso; keeping it caller-supplied ensures that this equality rewrites the caller's isomorphism.

theorem TauCeti.groupHomology.indIso_inv_comp_map_counit {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (S : Subgroup G) (B : Rep.{u, u, u} k G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupHomology.indIso S (Rep.res S.subtype B) n).inv (groupHomology.map (MonoidHom.id G) ((Rep.indResAdjunction k S.subtype).counit.app B) n) = groupHomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype B)) n

Corestriction through Shapiro's lemma. For a G-representation B, the inverse of Shapiro's isomorphism Hₙ(G, Ind_S^G Res_S B) ≅ Hₙ(S, Res_S B) followed by the map induced by the counit Ind_S^G Res_S B ⟶ B of induction–restriction is corestriction Hₙ(S, Res_S B) ⟶ Hₙ(G, B).

theorem TauCeti.groupHomology.indIso_inv_comp_map_counit_assoc {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (S : Subgroup G) (B : Rep.{u, u, u} k G) (n : ℕ) {Z : ModuleCat k} (h : groupHomology B n ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.indIso S (Rep.res S.subtype B) n).inv (CategoryTheory.CategoryStruct.comp (groupHomology.map (MonoidHom.id G) ((Rep.indResAdjunction k S.subtype).counit.app B) n) h) = CategoryTheory.CategoryStruct.comp (groupHomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype B)) n) h

Corestriction through Shapiro's lemma. For a G-representation B, the inverse of Shapiro's isomorphism Hₙ(G, Ind_S^G Res_S B) ≅ Hₙ(S, Res_S B) followed by the map induced by the counit Ind_S^G Res_S B ⟶ B of induction–restriction is corestriction Hₙ(S, Res_S B) ⟶ Hₙ(G, B).

theorem TauCeti.groupHomology.indIso_inv_naturality {k G : Type u} [CommRing k] [Group G] [DecidableEq G] (S : Subgroup G) (A : Rep.{u, u, u} k ↥S) {B : Rep.{u, u, u} k ↥S} (φ : A ⟶ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (groupHomology.map (MonoidHom.id ↥S) φ n) (groupHomology.indIso S B n).inv = CategoryTheory.CategoryStruct.comp (groupHomology.indIso S A n).inv (groupHomology.map (MonoidHom.id G) ((Rep.indFunctor k S.subtype).map φ) n)

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

theorem TauCeti.groupHomology.indIso_inv_naturality_assoc {k G : Type u} [CommRing k] [Group G] [DecidableEq 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 : groupHomology (Rep.ind S.subtype B) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.map (MonoidHom.id ↥S) φ n) (CategoryTheory.CategoryStruct.comp (groupHomology.indIso S B n).inv h) = CategoryTheory.CategoryStruct.comp (groupHomology.indIso S A n).inv (CategoryTheory.CategoryStruct.comp (groupHomology.map (MonoidHom.id G) ((Rep.indFunctor k S.subtype).map φ) n) h)

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

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

Shapiro's isomorphism is natural in the coefficients: indIso_inv_naturality for (indIso S A n).hom.

theorem TauCeti.groupHomology.indIso_hom_naturality_assoc {k G : Type u} [CommRing k] [Group G] [DecidableEq 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 : groupHomology B n ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.map (MonoidHom.id G) ((Rep.indFunctor k S.subtype).map φ) n) (CategoryTheory.CategoryStruct.comp (groupHomology.indIso S B n).hom h) = CategoryTheory.CategoryStruct.comp (groupHomology.indIso S A n).hom (CategoryTheory.CategoryStruct.comp (groupHomology.map (MonoidHom.id ↥S) φ n) h)

Shapiro's isomorphism is natural in the coefficients: indIso_inv_naturality for (indIso S A n).hom.