Shapiro's lemma for Tate cohomology

Let G be a finite group, S a subgroup of G and A a representation of S. This file identifies the Tate cohomology of the coinduced representation Coind_S^G A with that of A:

H-hat^n(G, Coind_S^G A) ≅ H-hat^n(S, A).

Mathlib's Shapiro lemma groupCohomology.coindIso gives this for ordinary cohomology, which is Tate cohomology in positive degrees, so the isomorphism holds in every positive degree for every finite group (coindIsoPos). When G is cyclic, so is S, and two-periodicity of Tate cohomology (Rep.FiniteCyclicGroup.periodicIso) carries every degree to a positive one, on both sides at once (coindIso).

This is how the Tate cohomology of a module whose summands are permuted transitively by G is computed from the stabilizer of one summand: for instance the units of a semi-local algebra K_v ⊗[K] L of a cyclic extension of number fields, coinduced from the decomposition group of one place above v.

Main definitions

• TauCeti.TateCohomology.coindIsoPos: H-hat^n(G, Coind_S^G A) ≅ H-hat^n(S, A) for G finite and every positive n : ℕ.
• TauCeti.TateCohomology.coindIso: H-hat^n(G, Coind_S^G A) ≅ H-hat^n(S, A) for G finite cyclic and every n : ℤ.

References

• J. S. Milne, Class Field Theory, Chapter II, Proposition 1.11 (Shapiro's lemma) and §3 (Tate cohomology), and Chapter VII, §2.

noncomputable def TauCeti.TateCohomology.coindIsoPos {R G : Type u} [CommRing R] [Group G] [Fintype G] (S : Subgroup G) [Fintype ↥S] (A : Rep.{u, u, u} R ↥S) (n : ℕ) [NeZero n] : tateCohomology (Rep.coind.{u, u, u, u} S.subtype A) ↑n ≅ tateCohomology A ↑n

Shapiro's lemma for Tate cohomology in positive degrees. For a subgroup S of a finite group G and a representation A of S, the Tate cohomology of the coinduced representation Coind_S^G A is that of A, in every positive degree n.

noncomputable def TauCeti.TateCohomology.coindIso {R G : Type u} [CommRing R] [Group G] [Fintype G] (S : Subgroup G) [Fintype ↥S] (A : Rep.{u, u, u} R ↥S) [IsCyclic G] (n : ℤ) : tateCohomology (Rep.coind.{u, u, u, u} S.subtype A) n ≅ tateCohomology A n

Shapiro's lemma for Tate cohomology of a finite cyclic group. For a subgroup S of a finite cyclic group G and a representation A of S, the Tate cohomology of the coinduced representation Coind_S^G A is that of A, in every degree n : ℤ.