Connecting maps of Tate cohomology in negative degrees

Let G be a finite group and S a short exact sequence of representations of G. In degrees at most -2 Tate cohomology is group homology, \hat{H}^{-(n+1)}(G, M) ≅ Hₙ(G, M) for n > 0 (TauCeti.TateCohomology.negSuccIso), and in degree -1 it is the kernel of the norm modulo the augmentation submodule, a submodule of H₀(G, M) = M_G. This file compares the connecting maps of the long exact sequence of Tate cohomology of S below degree -1 with those of group homology.

The comparison TauCeti.TateCohomology.toGroupHomology : \hat{H}^{-(n+1)}(G, M) ⟶ Hₙ(G, M) is negSuccIso for n > 0 and the inclusion of \hat{H}^{-1}(G, M) into H₀(G, M) for n = 0. It is induced by the identity in negative degrees, from the Tate complex to the complex of inhomogeneous chains reindexed by n ↦ -(n + 1) and extended by zero, so it is injective, natural in M, and commutes with the connecting maps. These properties allow Tate restriction, which is the transfer of group homology in negative degrees, to be compared with the connecting maps there.

Main definitions

• TauCeti.TateCohomology.toGroupHomology: the comparison \hat{H}^{-(n+1)}(G, M) ⟶ Hₙ(G, M).

Main results

• TauCeti.TateCohomology.tateCohomologyFunctor_map_comp_toGroupHomology: the comparison is natural in the coefficient representation.
• TauCeti.TateCohomology.δ_comp_toGroupHomology: the comparison commutes with the connecting maps.
• TauCeti.TateCohomology.toGroupHomology_eq_negSuccIso_hom, TauCeti.TateCohomology.HNegOneπ_comp_toGroupHomology: the comparison is negSuccIso for n > 0, and sends the class of a norm-zero element to its class in H₀(G, M) for n = 0.
• TauCeti.TateCohomology.δ_comp_negSuccIso_hom: through negSuccIso, the Tate connecting map \hat{H}^{-(n+2)}(G, X₃) ⟶ \hat{H}^{-(n+1)}(G, X₁) is the connecting map H_{n+1}(G, X₃) ⟶ Hₙ(G, X₁) of group homology, for n > 0.

References

• K. S. Brown, Cohomology of Groups, Chapter VI.
• J. S. Milne, Class Field Theory, v4.03, Chapter II, §1.

Attribution

This file is adapted from the unmerged TauCetiProject/TauCeti#10141.

noncomputable def TauCeti.TateCohomology.toGroupHomology {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) : tateCohomology M (Int.negSucc n) ⟶ groupHomology M n

The comparison \hat{H}^{-(n+1)}(G, M) ⟶ Hₙ(G, M) induced on homology by the identity in negative degrees. It is negSuccIso for n > 0 (toGroupHomology_eq_negSuccIso_hom), and the inclusion of \hat{H}^{-1}(G, M) into H₀(G, M) for n = 0 (HNegOneπ_comp_toGroupHomology).

theorem TauCeti.TateCohomology.δ_comp_toGroupHomology {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) (n : ℕ) : CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS (Int.negSucc (n + 1))) (toGroupHomology S.X₁ n) = CategoryTheory.CategoryStruct.comp (toGroupHomology S.X₃ (n + 1)) (groupHomology.δ hS (n + 1) n ⋯)

The comparison with group homology commutes with the connecting maps: through toGroupHomology, the Tate connecting map \hat{H}^{-(n+2)}(G, X₃) ⟶ \hat{H}^{-(n+1)}(G, X₁) is the connecting map H_{n+1}(G, X₃) ⟶ Hₙ(G, X₁) of group homology, for every n : ℕ.

theorem TauCeti.TateCohomology.δ_comp_toGroupHomology_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) (n : ℕ) {Z : ModuleCat R} (h : groupHomology S.X₁ n ⟶ Z) : CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS (Int.negSucc (n + 1))) (CategoryTheory.CategoryStruct.comp (toGroupHomology S.X₁ n) h) = CategoryTheory.CategoryStruct.comp (toGroupHomology S.X₃ (n + 1)) (CategoryTheory.CategoryStruct.comp (groupHomology.δ hS (n + 1) n ⋯) h)

The comparison with group homology commutes with the connecting maps: through toGroupHomology, the Tate connecting map \hat{H}^{-(n+2)}(G, X₃) ⟶ \hat{H}^{-(n+1)}(G, X₁) is the connecting map H_{n+1}(G, X₃) ⟶ Hₙ(G, X₁) of group homology, for every n : ℕ.

@[simp]

theorem TauCeti.TateCohomology.toGroupHomology_eq_negSuccIso_hom {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) [NeZero n] : toGroupHomology M n = (negSuccIso M n).hom

For n > 0 the comparison with group homology is negSuccIso.

theorem TauCeti.TateCohomology.δ_comp_negSuccIso_hom {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) (n : ℕ) [NeZero n] : CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS (Int.negSucc (n + 1))) (negSuccIso S.X₁ n).hom = CategoryTheory.CategoryStruct.comp (negSuccIso S.X₃ (n + 1)).hom (groupHomology.δ hS (n + 1) n ⋯)

The connecting maps of Tate cohomology below degree -1 are those of group homology: through negSuccIso, the Tate connecting map \hat{H}^{-(n+2)}(G, X₃) ⟶ \hat{H}^{-(n+1)}(G, X₁) is the connecting map H_{n+1}(G, X₃) ⟶ Hₙ(G, X₁) of group homology, for n > 0.

theorem TauCeti.TateCohomology.δ_comp_negSuccIso_hom_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) (n : ℕ) [NeZero n] {Z : ModuleCat R} (h : groupHomology S.X₁ n ⟶ Z) : CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS (Int.negSucc (n + 1))) (CategoryTheory.CategoryStruct.comp (negSuccIso S.X₁ n).hom h) = CategoryTheory.CategoryStruct.comp (negSuccIso S.X₃ (n + 1)).hom (CategoryTheory.CategoryStruct.comp (groupHomology.δ hS (n + 1) n ⋯) h)

The connecting maps of Tate cohomology below degree -1 are those of group homology: through negSuccIso, the Tate connecting map \hat{H}^{-(n+2)}(G, X₃) ⟶ \hat{H}^{-(n+1)}(G, X₁) is the connecting map H_{n+1}(G, X₃) ⟶ Hₙ(G, X₁) of group homology, for n > 0.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_comp_toGroupHomology {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp (HNegOneπ M) (toGroupHomology M 0) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.ker M.ρ.norm).subtype) (groupHomology.H0π M)

In degree -1 the comparison with group homology sends the class of a norm-zero element to its class in H₀(G, M).

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_comp_toGroupHomology_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) {Z : ModuleCat R} (h : groupHomology M 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (HNegOneπ M) (CategoryTheory.CategoryStruct.comp (toGroupHomology M 0) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.ker M.ρ.norm).subtype) (CategoryTheory.CategoryStruct.comp (groupHomology.H0π M) h)

In degree -1 the comparison with group homology sends the class of a norm-zero element to its class in H₀(G, M).

theorem TauCeti.TateCohomology.tateCohomologyFunctor_map_comp_toGroupHomology {R G : Type u} [CommRing R] [Group G] [Fintype G] {M N : Rep R G} (f : M ⟶ N) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (Int.negSucc n)).map f) (toGroupHomology N n) = CategoryTheory.CategoryStruct.comp (toGroupHomology M n) (groupHomology.map (MonoidHom.id G) f n)

The comparison with group homology is natural in the coefficient representation.

theorem TauCeti.TateCohomology.tateCohomologyFunctor_map_comp_toGroupHomology_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] {M N : Rep R G} (f : M ⟶ N) (n : ℕ) {Z : ModuleCat R} (h : groupHomology N n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (Int.negSucc n)).map f) (CategoryTheory.CategoryStruct.comp (toGroupHomology N n) h) = CategoryTheory.CategoryStruct.comp (toGroupHomology M n) (CategoryTheory.CategoryStruct.comp (groupHomology.map (MonoidHom.id G) f n) h)

The comparison with group homology is natural in the coefficient representation.

instance TauCeti.TateCohomology.instMonoModuleCatToGroupHomology {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) : CategoryTheory.Mono (toGroupHomology M n)

The comparison with group homology is injective.