Homology of modules induced from the trivial subgroup

By Shapiro's lemma, the representation Ind_⊥^G X induced from the trivial subgroup has vanishing homology in positive degrees, and so does its restriction to any subgroup S, since that restriction is again induced from the trivial subgroup (Rep.resIndBotIso).

The statements follow ClassFieldTheory/Cohomology/IndCoind/TrivialCohomology.lean in kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509.

Main statements

• groupHomology.isZero_indBot_succ: Hₙ₊₁(G, Ind_⊥^G X) = 0.
• groupHomology.isZero_res_indBot_succ: Hₙ₊₁(S, Ind_⊥^G X) = 0 for every subgroup S ≤ G.
• TauCeti.groupHomology.isZero_res_leftRegular_succ: Hₙ₊₁(S, k[G]) = 0 for every subgroup.

References

• K. S. Brown, Cohomology of Groups, Chapter III, §6.
• Charles A. Weibel, An Introduction to Homological Algebra, Section 6.3.

theorem groupHomology.isZero_indBot_succ {k G : Type u} [CommRing k] [Group G] (X : Type u) [AddCommGroup X] [Module k X] (n : ℕ) : CategoryTheory.Limits.IsZero (groupHomology (Rep.indBot k G X) (n + 1))

Positive-degree homology of a representation induced from the trivial subgroup vanishes (Weibel 6.3.3). Unlike the Tate analogue TauCeti.TateCohomology.isZero_indBot, no finiteness is needed.

theorem groupHomology.isZero_res_indBot_succ {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) (X : Type u) [AddCommGroup X] [Module k X] (n : ℕ) : CategoryTheory.Limits.IsZero (groupHomology (Rep.res S.subtype (Rep.indBot k G X)) (n + 1))

Positive-degree homology of the restriction to a subgroup of a representation induced from the trivial subgroup vanishes. Unlike the Tate analogue TauCeti.TateCohomology.isZero_res_indBot, no finiteness is needed.

theorem TauCeti.groupHomology.isZero_res_leftRegular_succ {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) (n : ℕ) : CategoryTheory.Limits.IsZero (groupHomology (Rep.res S.subtype (Rep.leftRegular k G)) (n + 1))

Positive-degree homology of a subgroup with coefficients in the restricted left regular representation vanishes, without any finiteness assumption.