Corestriction in negative Tate degrees

Let f : H → G be a homomorphism of finite groups and let M be a G-representation. In every Tate degree at most -2, Mathlib identifies Tate cohomology with ordinary group homology:

Ĥ⁻ⁿ⁻¹(G, M) ≃ Hₙ(G, M) for n > 0.

Ordinary group homology is covariant in the group, so f gives corestriction

Ĥ⁻ⁿ⁻¹(H, M) ⟶ Ĥ⁻ⁿ⁻¹(G, M).

This file packages that composite in every such degree and proves that transport back through the Tate comparison is exactly Mathlib's group-homology map. The construction is a natural transformation in the coefficient representation. Degree -2, which corresponds to first group homology and hence to the abelianization for trivial integral coefficients, is exported under the separate name HNegTwoCor for the low-degree Artin--Tate applications. Its interaction with the low-degree homology comparison is recorded explicitly.

This construction treats degrees at most -2 via group homology; positive degrees instead require a cohomological corestriction construction.

Main definitions

• TauCeti.TateCohomology.negSuccCorNatTrans: corestriction along a group homomorphism in degree -(n+1), natural in the coefficient representation, for n > 0.
• TauCeti.TateCohomology.negSuccCor: its value on one representation.
• TauCeti.TateCohomology.HNegTwoCor: the degree--2 specialization.

Main results

• TauCeti.TateCohomology.negSuccCor_comp_negSuccIso_hom: negative corestriction agrees with ordinary group-homology corestriction through TauCeti.TateCohomology.negSuccIso.
• TauCeti.TateCohomology.map_comp_negSuccCor: negative corestriction is natural in its coefficients.

References

• E. Artin and J. Tate, Class Field Theory, Chapter IV, §6 and Chapter XIV, §4.
• K. S. Brown, Cohomology of Groups, Chapter III, §9 and Chapter VI, §5.

noncomputable def TauCeti.TateCohomology.negSuccCorNatTrans {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] (f : H →* G) (n : ℕ) [NeZero n] : (Rep.resFunctor f).comp (tateCohomologyFunctor (Int.negSucc n)) ⟶ tateCohomologyFunctor (Int.negSucc n)

Corestriction along a homomorphism in Tate degree -(n+1), natural in the coefficient representation, where n > 0. Through Mathlib's negative-degree Tate comparison this is the ordinary covariant map on nth group homology induced by the homomorphism.

noncomputable def TauCeti.TateCohomology.negSuccCor {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] (M : Rep R G) (f : H →* G) (n : ℕ) [NeZero n] : tateCohomology (Rep.res f M) (Int.negSucc n) ⟶ tateCohomology M (Int.negSucc n)

Corestriction along f : H → G in Tate degree -(n+1), where n > 0.

@[simp]

theorem TauCeti.TateCohomology.negSuccCor_comp_negSuccIso_hom {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] (M : Rep R G) (f : H →* G) (n : ℕ) [NeZero n] : CategoryTheory.CategoryStruct.comp (negSuccCor M f n) (negSuccIso M n).hom = CategoryTheory.CategoryStruct.comp (negSuccIso (Rep.res f M) n).hom (groupHomology.map f (CategoryTheory.CategoryStruct.id (Rep.res f M)) n)

Negative-degree Tate corestriction is the ordinary group-homology map through TauCeti.TateCohomology.negSuccIso.

@[simp]

theorem TauCeti.TateCohomology.negSuccCor_comp_negSuccIso_hom_assoc {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] (M : Rep R G) (f : H →* G) (n : ℕ) [NeZero n] {Z : ModuleCat R} (h : groupHomology M n ⟶ Z) : CategoryTheory.CategoryStruct.comp (negSuccCor M f n) (CategoryTheory.CategoryStruct.comp (negSuccIso M n).hom h) = CategoryTheory.CategoryStruct.comp (negSuccIso (Rep.res f M) n).hom (CategoryTheory.CategoryStruct.comp (groupHomology.map f (CategoryTheory.CategoryStruct.id (Rep.res f M)) n) h)

Negative-degree Tate corestriction is the ordinary group-homology map through TauCeti.TateCohomology.negSuccIso.

@[simp]

theorem TauCeti.TateCohomology.map_comp_negSuccCor {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] {M N : Rep R G} (f : H →* G) (n : ℕ) [NeZero n] (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (Int.negSucc n)).map (Rep.resMap f φ)) (negSuccCor N f n) = CategoryTheory.CategoryStruct.comp (negSuccCor M f n) ((tateCohomologyFunctor (Int.negSucc n)).map φ)

Negative-degree Tate corestriction is natural in the coefficient representation.

@[simp]

theorem TauCeti.TateCohomology.map_comp_negSuccCor_assoc {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] {M N : Rep R G} (f : H →* G) (n : ℕ) [NeZero n] (φ : M ⟶ N) {Z : ModuleCat R} (h : tateCohomology N (Int.negSucc n) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (Int.negSucc n)).map (Rep.resMap f φ)) (CategoryTheory.CategoryStruct.comp (negSuccCor N f n) h) = CategoryTheory.CategoryStruct.comp (negSuccCor M f n) (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (Int.negSucc n)).map φ) h)

Negative-degree Tate corestriction is natural in the coefficient representation.

noncomputable def TauCeti.TateCohomology.HNegTwoCor {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] (M : Rep R G) (f : H →* G) : tateCohomology (Rep.res f M) (-2) ⟶ tateCohomology M (-2)

Corestriction along a group homomorphism in degree -2 Tate cohomology. Under the comparison with group homology, this is the induced map on first homology.

theorem TauCeti.TateCohomology.HNegTwoCor_eq_negSuccCor {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] (M : Rep R G) (f : H →* G) : HNegTwoCor M f = negSuccCor M f 1

Degree--2 corestriction is the degree-one instance of negative corestriction.

@[simp]

theorem TauCeti.TateCohomology.map_comp_HNegTwoCor {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] {M N : Rep R G} (f : H →* G) (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (-2)).map (Rep.resMap f φ)) (HNegTwoCor N f) = CategoryTheory.CategoryStruct.comp (HNegTwoCor M f) ((tateCohomologyFunctor (-2)).map φ)

Degree--2 corestriction is natural in the coefficient representation.

@[simp]

theorem TauCeti.TateCohomology.map_comp_HNegTwoCor_assoc {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] {M N : Rep R G} (f : H →* G) (φ : M ⟶ N) {Z : ModuleCat R} (h : tateCohomology N (-2) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (-2)).map (Rep.resMap f φ)) (CategoryTheory.CategoryStruct.comp (HNegTwoCor N f) h) = CategoryTheory.CategoryStruct.comp (HNegTwoCor M f) (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (-2)).map φ) h)

Degree--2 corestriction is natural in the coefficient representation.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoCor_comp_isoGroupHomology_hom {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] (M : Rep R G) (f : H →* G) : CategoryTheory.CategoryStruct.comp (HNegTwoCor M f) ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app M) = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.res f M)) ((groupHomology.coresNatTrans R f 1).app M)

Degree--2 corestriction agrees with the map induced on first group homology.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoCor_comp_isoGroupHomology_hom_assoc {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] (M : Rep R G) (f : H →* G) {Z : ModuleCat R} (h : (groupHomology.functor R G 1).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (HNegTwoCor M f) (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app M) h) = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.res f M)) (CategoryTheory.CategoryStruct.comp ((groupHomology.coresNatTrans R f 1).app M) h)

Degree--2 corestriction agrees with the map induced on first group homology.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoCor_comp_isoGroupHomology_hom_apply {R G H : Type u} [CommRing R] [Group G] [Group H] [Fintype G] [Fintype H] (M : Rep R G) (f : H →* G) (x : ↑(tateCohomology (Rep.res f M) (-2))) : (CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app M)) ((CategoryTheory.ConcreteCategory.hom (HNegTwoCor M f)) x) = (CategoryTheory.ConcreteCategory.hom (groupHomology.map f (CategoryTheory.CategoryStruct.id (Rep.res f M)) 1)) ((CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.res f M))) x)

Degree--2 corestriction agrees with the map induced on first group homology.