Restriction and corestriction in every Tate degree

For a subgroup H of a finite group G, the separate constructions of restriction and corestriction in positive, zero, minus one, and lower negative degrees assemble into maps in every integer degree. Their composite is multiplication by the index [G : H]; for the trivial subgroup, whose Tate cohomology vanishes, this shows that every Tate cohomology group of G is killed by |G| (natCard_nsmul_eq_zero), hence torsion (isAddTorsion_tateCohomology), and zero if |G| is invertible in the coefficient ring (subsingleton_tateCohomology_of_isUnit_natCard). These uniform maps are the group-change operations used in the restriction law for the Tate cup product. Restriction is natural in the coefficient representation in every degree (res_natural). Tower composition for class-field-theory layers is provided by ClassFieldTheory.LayerRestriction.tateRes_trans and ClassFieldTheory.LayerRestriction.tateCor_trans.

In positive degrees the maps use the canonical comparison with ordinary group cohomology; in degrees zero and minus one they use invariants and norm kernels; below minus one they use the comparison with group homology. The normalization follows the usual restriction-corestriction identity (Brown, Cohomology of Groups, Chapter III, §9; Artin and Tate, Class Field Theory, Chapter IV, §6).

noncomputable def TauCeti.TateCohomology.res {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (r : ℤ) : tateCohomology M r ⟶ tateCohomology (Rep.res H.subtype M) r

Restriction of Tate cohomology from a finite group to a subgroup, in every integer degree.

@[simp]

theorem TauCeti.TateCohomology.res_zero {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : res M H 0 = H0Res M H

In degree zero, uniform Tate restriction is induced by inclusion of invariants.

@[simp]

theorem TauCeti.TateCohomology.res_ofNat_succ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) : res M H (↑n + 1) = posRes M H n

In positive degrees, uniform Tate restriction is ordinary cohomological restriction.

@[simp]

theorem TauCeti.TateCohomology.res_neg_one {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : res M H (-1) = HNegOneRes M H

In degree minus one, uniform Tate restriction uses the relative transfer on norm kernels.

@[simp]

theorem TauCeti.TateCohomology.res_negSucc_succ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) : res M H (Int.negSucc (n + 1)) = negSuccRes M H (n + 1)

Below degree minus one, uniform Tate restriction is homological transfer.

theorem TauCeti.TateCohomology.res_natural {R G : Type u} [CommRing R] [Group G] [Fintype G] {M N : Rep.{u, u, u} R G} (f : M ⟶ N) (H : Subgroup G) (r : ℤ) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor r).map f) (res N H r) = CategoryTheory.CategoryStruct.comp (res M H r) ((tateCohomologyFunctor r).map (Rep.resMap H.subtype f))

Tate restriction is natural in the coefficient representation, in every integer degree.

theorem TauCeti.TateCohomology.res_natural_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] {M N : Rep.{u, u, u} R G} (f : M ⟶ N) (H : Subgroup G) (r : ℤ) {Z : ModuleCat R} (h : tateCohomology (Rep.res H.subtype N) r ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor r).map f) (CategoryTheory.CategoryStruct.comp (res N H r) h) = CategoryTheory.CategoryStruct.comp (res M H r) (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor r).map (Rep.resMap H.subtype f)) h)

Tate restriction is natural in the coefficient representation, in every integer degree.

noncomputable def TauCeti.TateCohomology.cor {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (r : ℤ) : tateCohomology (Rep.res H.subtype M) r ⟶ tateCohomology M r

Corestriction of Tate cohomology from a subgroup of a finite group, in every integer degree.

@[simp]

theorem TauCeti.TateCohomology.cor_zero {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : cor M H 0 = H0Cor M H

In degree zero, uniform Tate corestriction is the relative norm.

@[simp]

theorem TauCeti.TateCohomology.cor_ofNat_succ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) : cor M H (↑n + 1) = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology (n + 1)).hom.app (Rep.res H.subtype M)) (CategoryTheory.CategoryStruct.comp (groupCohomology.corestriction H M (n + 1)) ((TateCohomology.isoGroupCohomology (n + 1)).inv.app M))

In positive degrees, uniform Tate corestriction is ordinary corestriction transported through the canonical comparison isomorphisms.

@[simp]

theorem TauCeti.TateCohomology.cor_neg_one {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : cor M H (-1) = HNegOneCor M H

In degree minus one, uniform Tate corestriction includes the subgroup norm kernel.

@[simp]

theorem TauCeti.TateCohomology.cor_negSucc_succ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) : cor M H (Int.negSucc (n + 1)) = negSuccCor M H.subtype (n + 1)

Below degree minus one, uniform Tate corestriction is the covariant map on homology.

theorem TauCeti.TateCohomology.cor_pos_comp_isoGroupCohomology_hom {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (cor M H (↑n + 1)) ((TateCohomology.isoGroupCohomology (n + 1)).hom.app M) = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology (n + 1)).hom.app (Rep.res H.subtype M)) (groupCohomology.corestriction H M (n + 1))

In positive degrees, Tate corestriction agrees with ordinary cohomological corestriction through the canonical comparison.

theorem TauCeti.TateCohomology.cor_pos_comp_isoGroupCohomology_hom_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) {Z : ModuleCat R} (h : (groupCohomology.functor R G (n + 1)).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (cor M H (↑n + 1)) (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology (n + 1)).hom.app M) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology (n + 1)).hom.app (Rep.res H.subtype M)) (groupCohomology.corestriction H M (n + 1))) h

In positive degrees, Tate corestriction agrees with ordinary cohomological corestriction through the canonical comparison.

@[simp]

theorem TauCeti.TateCohomology.res_comp_cor {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (r : ℤ) : CategoryTheory.CategoryStruct.comp (res M H r) (cor M H r) = H.index • CategoryTheory.CategoryStruct.id (tateCohomology M r)

Restriction followed by corestriction multiplies every Tate class by the subgroup index, in every integer degree.

@[simp]

theorem TauCeti.TateCohomology.res_comp_cor_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (r : ℤ) {Z : ModuleCat R} (h : tateCohomology M r ⟶ Z) : CategoryTheory.CategoryStruct.comp (res M H r) (CategoryTheory.CategoryStruct.comp (cor M H r) h) = CategoryTheory.CategoryStruct.comp (H.index • CategoryTheory.CategoryStruct.id (tateCohomology M r)) h

Restriction followed by corestriction multiplies every Tate class by the subgroup index, in every integer degree.

@[simp]

theorem TauCeti.TateCohomology.res_comp_cor_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (r : ℤ) (x : ↑(tateCohomology M r)) : (CategoryTheory.ConcreteCategory.hom (cor M H r)) ((CategoryTheory.ConcreteCategory.hom (res M H r)) x) = H.index • x

Restriction followed by corestriction multiplies every Tate class by the subgroup index, in every integer degree.

theorem TauCeti.TateCohomology.natCard_nsmul_eq_zero {R G : Type u} [CommRing R] [Group G] [Fintype G] {A : Rep.{u, u, u} R G} {n : ℤ} (x : ↑(tateCohomology A n)) : Nat.card G • x = 0

Tate cohomology of a finite group is killed by the order of the group: every class in every degree is annihilated by Nat.card G.

theorem TauCeti.TateCohomology.subsingleton_tateCohomology_of_isUnit_natCard {R G : Type u} [CommRing R] [Group G] [Fintype G] {A : Rep.{u, u, u} R G} (h : IsUnit ↑(Nat.card G)) (n : ℤ) : Subsingleton ↑(tateCohomology A n)

Tate cohomology vanishes in every degree if the order of the group is invertible in the coefficient ring, since it is killed by Nat.card G.

theorem TauCeti.TateCohomology.isAddTorsion_tateCohomology {R G : Type u} [CommRing R] [Group G] [Fintype G] (A : Rep.{u, u, u} R G) (n : ℤ) : IsAddTorsion ↑(tateCohomology A n)

Every Tate cohomology group of a finite group is torsion, being killed by Nat.card G.