Connecting maps and the comparison from group cohomology to Tate cohomology

The identity on nonnegative cochains gives a natural map from ordinary group cohomology to Tate cohomology. It is the quotient of invariants by norms in degree zero and the canonical comparison isomorphism in positive degrees, and it intertwines the connecting maps. These properties allow ordinary cohomological functoriality to be transported across degree zero.

The intermediate cochain complex is extended by zero in negative degrees; its map to the Tate complex is the identity in every nonnegative degree.

Main results

• Rep.cochainsExtToTate_app_f_ofNat: the comparison is the identity on nonnegative cochains.
• Rep.cochainsExtToTate_app_f_negSucc: the comparison is zero in negative degrees.
• Rep.fromGroupCohomology: the comparison from ordinary cohomology to Tate cohomology in every nonnegative degree.
• Rep.fromGroupCohomology_zero: the degree-zero comparison is the quotient of invariants by norms.
• Rep.fromGroupCohomology_succ: the positive comparison is inverse to Mathlib's canonical Tate-to-ordinary comparison.
• TauCeti.TateCohomology.δ_comp_fromGroupCohomology: the comparison intertwines the connecting maps, including the map from degree zero to degree one.

References

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

noncomputable def Rep.cochainsConnectData {R G : Type u} [CommRing R] [Group G] (M : Rep R G) : CochainComplex.ConnectData HomologicalComplex.zero (groupCohomology.inhomogeneousCochains M)

The complex of inhomogeneous cochains of M, connected to the zero chain complex by the zero map: the complex of inhomogeneous cochains extended by zero to negative degrees.

@[simp]

theorem Rep.cochainsConnectData_d₀ {R G : Type u} [CommRing R] [Group G] (M : Rep R G) : M.cochainsConnectData.d₀ = 0

noncomputable def TauCeti.TateCohomology.cochainsExtFunctor (R G : Type u) [CommRing R] [Group G] : CategoryTheory.Functor (Rep R G) (CochainComplex (ModuleCat R) ℤ)

The complex of inhomogeneous cochains extended by zero to negative degrees, as a functor.

@[simp]

theorem Rep.cochainsExtFunctor_obj_X_ofNat {R G : Type u} [CommRing R] [Group G] (M : Rep R G) (n : ℕ) : ((TauCeti.TateCohomology.cochainsExtFunctor R G).obj M).X ↑n = (groupCohomology.inhomogeneousCochains M).X n

The zero extension has the original cochain carrier in each nonnegative degree.

@[simp]

theorem Rep.cochainsExtFunctor_obj_X_negSucc {R G : Type u} [CommRing R] [Group G] (M : Rep R G) (n : ℕ) : ((TauCeti.TateCohomology.cochainsExtFunctor R G).obj M).X (Int.negSucc n) = HomologicalComplex.zero.X n

The zero extension has zero carrier in each negative degree.

@[simp]

theorem TauCeti.TateCohomology.cochainsExtFunctor_map_f_ofNat {R G : Type u} [CommRing R] [Group G] {M N : Rep R G} (f : M ⟶ N) (n : ℕ) : ((cochainsExtFunctor R G).map f).f ↑n = (groupCohomology.cochainsMap (MonoidHom.id G) f).f n

The extended coefficient map agrees with the cochain map in nonnegative degrees.

@[simp]

theorem TauCeti.TateCohomology.cochainsExtFunctor_map_f_negSucc {R G : Type u} [CommRing R] [Group G] {M N : Rep R G} (f : M ⟶ N) (n : ℕ) : ((cochainsExtFunctor R G).map f).f (Int.negSucc n) = 0

The extended coefficient map is zero in negative degrees.

instance TauCeti.TateCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatIntCochainsExtFunctor {R G : Type u} [CommRing R] [Group G] : (cochainsExtFunctor R G).PreservesZeroMorphisms

theorem TauCeti.TateCohomology.map_cochainsExtFunctor_shortExact {R G : Type u} [CommRing R] [Group G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) : (S.map (cochainsExtFunctor R G)).ShortExact

The extended complexes of a short exact sequence form a short exact sequence.

noncomputable def Rep.cochainsExtIso {R G : Type u} [CommRing R] [Group G] (M : Rep R G) (n : ℕ) : HomologicalComplex.homology M.cochainsConnectData.cochainComplex ↑n ≅ groupCohomology M n

The cohomology of the zero extension of cochains is ordinary group cohomology.

theorem TauCeti.TateCohomology.δ_comp_cochainsExtIso_hom {R G : Type u} [CommRing R] [Group G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) (n : ℕ) : CategoryTheory.CategoryStruct.comp (⋯.δ ↑n ↑(n + 1) ⋯) (S.X₁.cochainsExtIso (n + 1)).hom = CategoryTheory.CategoryStruct.comp (S.X₃.cochainsExtIso n).hom (groupCohomology.δ hS n (n + 1) ⋯)

The identification of extended cochains with ordinary cohomology commutes with connecting maps, including the map from degree zero to degree one.

theorem TauCeti.TateCohomology.δ_comp_cochainsExtIso_hom_assoc {R G : Type u} [CommRing R] [Group G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) (n : ℕ) {Z : ModuleCat R} (h : groupCohomology S.X₁ (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (⋯.δ ↑n ↑(n + 1) ⋯) (CategoryTheory.CategoryStruct.comp (S.X₁.cochainsExtIso (n + 1)).hom h) = CategoryTheory.CategoryStruct.comp (S.X₃.cochainsExtIso n).hom (CategoryTheory.CategoryStruct.comp (groupCohomology.δ hS n (n + 1) ⋯) h)

The identification of extended cochains with ordinary cohomology commutes with connecting maps, including the map from degree zero to degree one.

noncomputable def TauCeti.TateCohomology.cochainsExtToTate (R G : Type u) [CommRing R] [Group G] [Fintype G] : cochainsExtFunctor R G ⟶ tateComplexFunctor R G

The identity in nonnegative degrees, from the extended complex of cochains to the Tate complex.

@[simp]

theorem Rep.cochainsExtToTate_app_f_ofNat {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) : ((TauCeti.TateCohomology.cochainsExtToTate R G).app M).f ↑n = CategoryTheory.CategoryStruct.id ((groupCohomology.inhomogeneousCochains M).X n)

The comparison with the Tate complex is the identity on every nonnegative cochain.

@[simp]

theorem Rep.cochainsExtToTate_app_f_negSucc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) : ((TauCeti.TateCohomology.cochainsExtToTate R G).app M).f (Int.negSucc n) = 0

The comparison with the Tate complex is zero in every negative degree.

theorem Rep.homologyMap_cochainsExtToTate {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) : HomologicalComplex.homologyMap ((TauCeti.TateCohomology.cochainsExtToTate R G).app M) ↑(n + 1) = CategoryTheory.CategoryStruct.comp (M.cochainsConnectData.homologyIsoPos (n + 1) ↑(n + 1) ⋯).hom ((tateComplexConnectData M).homologyIsoPos (n + 1) ↑(n + 1) ⋯).inv

In positive degrees, the identity of cochains induces on cohomology the composite of the two comparisons with the cohomology of the complex of inhomogeneous cochains.

theorem Rep.isIso_homologyMap_cochainsExtToTate {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) : CategoryTheory.IsIso (HomologicalComplex.homologyMap ((TauCeti.TateCohomology.cochainsExtToTate R G).app M) ↑(n + 1))

In positive degrees, the identity of cochains induces an isomorphism from the cohomology of the extended complex of cochains to Tate cohomology.

theorem Rep.epi_homologyMap_cochainsExtToTate_zero {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.Epi (HomologicalComplex.homologyMap ((TauCeti.TateCohomology.cochainsExtToTate R G).app M) 0)

In degree zero, the identity of cochains induces an epimorphism from the cohomology of the extended complex of cochains, the invariants, onto Tate cohomology.

theorem Rep.epi_homologyMap_cochainsExtToTate {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) {r : ℤ} (hr : 0 ≤ r) : CategoryTheory.Epi (HomologicalComplex.homologyMap ((TauCeti.TateCohomology.cochainsExtToTate R G).app M) r)

In nonnegative degrees, the identity of cochains induces an epimorphism from the cohomology of the extended complex of cochains onto Tate cohomology.

noncomputable def Rep.fromGroupCohomology {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) : groupCohomology M n ⟶ tateCohomology M ↑n

The canonical map from ordinary group cohomology to Tate cohomology in nonnegative degrees: quotient by norms in degree zero, and inverse to the usual comparison in positive degrees.

@[simp]

theorem Rep.fromGroupCohomology_succ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) : M.fromGroupCohomology (n + 1) = ((TateCohomology.isoGroupCohomology (n + 1)).app M).inv

In positive degrees, the comparison from ordinary cohomology is inverse to Mathlib's canonical Tate-to-ordinary comparison.

@[simp]

theorem Rep.fromGroupCohomology_zero {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : M.fromGroupCohomology 0 = CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso M).hom (TauCeti.TateCohomology.H0π M)

In degree zero, the ordinary-to-Tate comparison is the quotient map on invariants.

instance TauCeti.TateCohomology.instEpiModuleCatFromGroupCohomology {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) : CategoryTheory.Epi (M.fromGroupCohomology n)

The comparison from ordinary cohomology is surjective in every nonnegative degree.

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

Ordinary and Tate connecting maps agree through the canonical comparison, including the connecting map from degree zero to degree one.

theorem TauCeti.TateCohomology.δ_comp_fromGroupCohomology_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 : tateCohomology S.X₁ ↑(n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupCohomology.δ hS n (n + 1) ⋯) (CategoryTheory.CategoryStruct.comp (S.X₁.fromGroupCohomology (n + 1)) h) = CategoryTheory.CategoryStruct.comp (S.X₃.fromGroupCohomology n) (CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS ↑n) h)

Ordinary and Tate connecting maps agree through the canonical comparison, including the connecting map from degree zero to degree one.