The Tate dimension shift along the augmentation sequence

For a group G, the augmentation sequence 0 ⟶ I_G ⟶ k[G] ⟶ k ⟶ 0 (built in TauCeti.RepresentationTheory.Homological.Augmentation.Basic) has a middle term whose Tate cohomology vanishes for every finite subgroup, because the left regular representation is Tate-acyclic. Its connecting homomorphisms are therefore isomorphisms Ĥⁿ(S, k) ≅ Ĥⁿ⁺¹(S, I_G) in every degree, for every finite subgroup S ≤ G. The ambient group need not be finite; only S need be, since only its Tate cohomology is formed. This is the first of the two dimension shifts behind Tate's theorem; the second is the splitting module of a two-dimensional class.

Main definitions

• TauCeti.TateCohomology.augmentationδIso: Ĥⁿ(S, k) ≅ Ĥⁿ⁺¹(S, I_G) for every finite subgroup S of a group G and every n : ℤ.

Main statements

• TauCeti.TateCohomology.augmentationδIso_hom: the shift is the connecting homomorphism.
• TauCeti.groupCohomology.isZero_H2_augmentationIdeal_res: H²(S, I_G) = 0 for a finite subgroup S when k has no additive torsion, since it is H¹(S, k) = Hom(S, k).

References

• J. S. Milne, Class Field Theory, Chapter II, proof of Theorem 3.11.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (3.1.4).
• The same dimension shift appears in ClassFieldTheory/Cohomology/AugmentationModule.lean in kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0); it is reimplemented here on Mathlib's Tate long-exact-sequence API rather than copied.

noncomputable def TauCeti.TateCohomology.augmentationδIso (k : Type u) {G : Type u} [CommRing k] [Group G] (S : Subgroup G) [Fintype ↥S] (n : ℤ) : tateCohomology (Rep.res S.subtype (Rep.trivial k G k)) n ≅ tateCohomology (Rep.res S.subtype (Rep.augmentationIdeal k G)) (n + 1)

The augmentation dimension shift: Ĥⁿ(S, k) ≅ Ĥⁿ⁺¹(S, I_G) for every finite subgroup S of a group G and every n : ℤ, given by the connecting homomorphism of the augmentation sequence.

@[simp]

theorem TauCeti.TateCohomology.augmentationδIso_hom {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [Fintype ↥S] (n : ℤ) : (augmentationδIso k S n).hom = TateCohomology.δ ⋯ n

The augmentation dimension shift is the connecting homomorphism.

theorem TauCeti.groupCohomology.isZero_H2_augmentationIdeal_res {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [Finite ↥S] [IsAddTorsionFree k] : CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype (Rep.augmentationIdeal k G)) 2)

H²(S, I_G) = 0 for a finite subgroup S of a group G and a coefficient ring k without additive torsion.