Cohomology of modules coinduced from the trivial subgroup

By Shapiro's lemma, the representation Coind_⊥^G X coinduced from the trivial subgroup has vanishing cohomology in positive degrees (Milne, Class Field Theory, II 1.11–1.12), and so does its restriction to any subgroup S, since that restriction is again coinduced from the trivial subgroup (Rep.resCoindBotIso). For a normal subgroup S, the same holds for its S-invariants as a representation of G ⧸ S, which are coinduced from the trivial subgroup of G ⧸ S (Rep.quotientToInvariantsCoindBotIso).

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

Main statements

• groupCohomology.isZero_coindBot_succ: Hⁿ⁺¹(G, Coind_⊥^G X) = 0.
• groupCohomology.isZero_res_coindBot_succ: Hⁿ⁺¹(S, Coind_⊥^G X) = 0 for every subgroup S ≤ G.
• TauCeti.groupCohomology.isZero_quotientToInvariants_coindBot_succ: Hⁿ⁺¹(G ⧸ S, (Coind_⊥^G X)^S) = 0 for every normal subgroup S ≤ G.

References

• J. S. Milne, Class Field Theory, Chapter II, §1.
• K. S. Brown, Cohomology of Groups, Chapter III, §6.

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

Positive-degree cohomology of a representation coinduced from the trivial subgroup vanishes (Milne II 1.12). Unlike the Tate analogue TauCeti.TateCohomology.isZero_coindBot, no finiteness is needed.

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

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

theorem TauCeti.groupCohomology.isZero_quotientToInvariants_coindBot_succ {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] (X : Type u) [AddCommGroup X] [Module k X] (n : ℕ) : CategoryTheory.Limits.IsZero (groupCohomology ((Rep.coindBot k G X).quotientToInvariants S) (n + 1))

The S-invariants of Coind_⊥^G X have no cohomology over G ⧸ S in positive degrees: they are coinduced from the trivial subgroup of G ⧸ S.