Corestriction and connecting maps in every Tate degree

For a subgroup H of a finite group G, Tate corestriction commutes with the connecting map of every short exact sequence of representations, from degree r to degree r + 1 for every integer r. This includes the norm boundary from degree minus one to degree zero. When both degrees are at most -2, the compatibility holds along any homomorphism of finite groups.

In negative degrees, the canonical comparison with group homology intertwines corestriction with the map induced by subgroup inclusion. At the norm boundary, the compatibility relates the norm-kernel inclusion in degree minus one to the relative norm on invariants in degree zero.

In nonnegative degrees, the canonical map from ordinary cohomology to Tate cohomology intertwines corestriction: in degree zero this is the relative norm on invariants, and in positive degrees it is ordinary cohomological corestriction. Since this comparison is surjective, the compatibility with ordinary connecting maps determines the Tate square.

These squares allow dimension shifting across the entire Tate complex and its norm boundary, in particular when proving the projection formula for cup products.

Main results

• TauCeti.TateCohomology.cor_comp_toGroupHomology: negative corestriction is the covariant map on group homology through the canonical comparison.
• TauCeti.TateCohomology.δ_comp_negSuccCor: corestriction along any homomorphism of finite groups commutes with connecting maps whose source and target degrees are at most -2.
• TauCeti.TateCohomology.δ_comp_cor_neg_one: corestriction commutes with the norm-boundary connecting map.
• Rep.fromGroupCohomology_comp_cor: the comparison from ordinary cohomology intertwines corestriction in every nonnegative degree.
• TauCeti.TateCohomology.δ_comp_cor: corestriction commutes with connecting maps in every integer degree.

References

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

theorem TauCeti.TateCohomology.cor_comp_toGroupHomology {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 (Int.negSucc n)) (toGroupHomology M n) = CategoryTheory.CategoryStruct.comp (toGroupHomology (Rep.res H.subtype M) n) (groupHomology.map H.subtype (CategoryTheory.CategoryStruct.id (Rep.res H.subtype M)) n)

Through the canonical comparison with group homology, negative Tate corestriction is induced by the inclusion of the subgroup. This also holds in degree minus one, where the comparison is an injection rather than an isomorphism.

theorem TauCeti.TateCohomology.cor_comp_toGroupHomology_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 : groupHomology M n ⟶ Z) : CategoryTheory.CategoryStruct.comp (cor M H (Int.negSucc n)) (CategoryTheory.CategoryStruct.comp (toGroupHomology M n) h) = CategoryTheory.CategoryStruct.comp (toGroupHomology (Rep.res H.subtype M) n) (CategoryTheory.CategoryStruct.comp (groupHomology.map H.subtype (CategoryTheory.CategoryStruct.id (Rep.res H.subtype M)) n) h)

Through the canonical comparison with group homology, negative Tate corestriction is induced by the inclusion of the subgroup. This also holds in degree minus one, where the comparison is an injection rather than an isomorphism.

@[simp]

theorem TauCeti.TateCohomology.δ_comp_cor_neg_one {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (H : Subgroup G) : CategoryTheory.CategoryStruct.comp (TateCohomology.δ ⋯ (-1)) (H0Cor S.X₁ H) = CategoryTheory.CategoryStruct.comp (HNegOneCor S.X₃ H) (TateCohomology.δ hS (-1))

Corestriction commutes with the connecting map from degree minus one to degree zero. On representatives this is the relative-norm identity N_{G/H} N_H = N_G.

@[simp]

theorem TauCeti.TateCohomology.δ_comp_cor_neg_one_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (H : Subgroup G) {Z : ModuleCat R} (h : tateCohomology S.X₁ 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (TateCohomology.δ ⋯ (-1)) (CategoryTheory.CategoryStruct.comp (H0Cor S.X₁ H) h) = CategoryTheory.CategoryStruct.comp (HNegOneCor S.X₃ H) (CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS (-1)) h)

Corestriction commutes with the connecting map from degree minus one to degree zero. On representatives this is the relative-norm identity N_{G/H} N_H = N_G.

@[simp]

theorem TauCeti.TateCohomology.δ_comp_negSuccCor {R G : Type u} [CommRing R] [Group G] [Fintype G] {H : Type u} [Group H] [Fintype H] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (f : H →* G) (n : ℕ) [NeZero n] : CategoryTheory.CategoryStruct.comp (TateCohomology.δ ⋯ (Int.negSucc (n + 1))) (negSuccCor S.X₁ f n) = CategoryTheory.CategoryStruct.comp (negSuccCor S.X₃ f (n + 1)) (TateCohomology.δ hS (Int.negSucc (n + 1)))

Corestriction along a homomorphism of finite groups commutes with the connecting map from degree -(n+2) to degree -(n+1) when n > 0, so both degrees are at most -2.

@[simp]

theorem TauCeti.TateCohomology.δ_comp_negSuccCor_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] {H : Type u} [Group H] [Fintype H] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (f : H →* G) (n : ℕ) [NeZero n] {Z : ModuleCat R} (h : tateCohomology S.X₁ (Int.negSucc n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (TateCohomology.δ ⋯ (Int.negSucc (n + 1))) (CategoryTheory.CategoryStruct.comp (negSuccCor S.X₁ f n) h) = CategoryTheory.CategoryStruct.comp (negSuccCor S.X₃ f (n + 1)) (CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS (Int.negSucc (n + 1))) h)

Corestriction along a homomorphism of finite groups commutes with the connecting map from degree -(n+2) to degree -(n+1) when n > 0, so both degrees are at most -2.

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

The canonical comparison from ordinary cohomology to Tate cohomology intertwines corestriction in every nonnegative degree, including the relative norm in degree zero.

As in cor, the subgroup Tate carrier uses Subgroup.fintypeOfFinite H; callers with another Fintype H should select this instance when forming the square. The generic Rep.fromGroupCohomology comparison itself preserves the ambient group instance.

theorem Rep.fromGroupCohomology_comp_cor_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 : tateCohomology M ↑n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((res H.subtype M).fromGroupCohomology n) (CategoryTheory.CategoryStruct.comp (TauCeti.TateCohomology.cor M H ↑n) h) = CategoryTheory.CategoryStruct.comp (TauCeti.groupCohomology.corestriction H M n) (CategoryTheory.CategoryStruct.comp (M.fromGroupCohomology n) h)

The canonical comparison from ordinary cohomology to Tate cohomology intertwines corestriction in every nonnegative degree, including the relative norm in degree zero.

As in cor, the subgroup Tate carrier uses Subgroup.fintypeOfFinite H; callers with another Fintype H should select this instance when forming the square. The generic Rep.fromGroupCohomology comparison itself preserves the ambient group instance.

@[simp]

theorem TauCeti.TateCohomology.δ_comp_cor {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (H : Subgroup G) (r : ℤ) : CategoryTheory.CategoryStruct.comp (TateCohomology.δ ⋯ r) (cor S.X₁ H (r + 1)) = CategoryTheory.CategoryStruct.comp (cor S.X₃ H r) (TateCohomology.δ hS r)

Tate corestriction commutes with the connecting map from degree r to degree r + 1 for every integer degree, including both sides of the norm boundary.

The subgroup Tate carrier uses the Subgroup.fintypeOfFinite H instance fixed by cor.

@[simp]

theorem TauCeti.TateCohomology.δ_comp_cor_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (H : Subgroup G) (r : ℤ) {Z : ModuleCat R} (h : tateCohomology S.X₁ (r + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (TateCohomology.δ ⋯ r) (CategoryTheory.CategoryStruct.comp (cor S.X₁ H (r + 1)) h) = CategoryTheory.CategoryStruct.comp (cor S.X₃ H r) (CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS r) h)

Tate corestriction commutes with the connecting map from degree r to degree r + 1 for every integer degree, including both sides of the norm boundary.

The subgroup Tate carrier uses the Subgroup.fintypeOfFinite H instance fixed by cor.