Tate Cohomology

This file defines the Tate cohomology of finite groups by taking homology of the Tate complex. We define the Tate complex by connecting the inhomogeneous chain complex with the inhomogeneous cochain complex using the norm map.

Key definitions

• Rep.tateNorm: the map induced by the norm map from the zeroth term of the inhomogeneous chain complex to the zeroth term of the inhomogeneous cochain complex.

• tateComplex: the Tate complex defined by connecting the inhomogeneous chain complex and cochain complex using the Tate norm.

• tateComplexFunctor: the functor taking a representation of G to its Tate complex.

• tateCohomologyFunctor: the functor taking a representation of G to its n-th Tate cohomology group.

• isoGroupCohomology: the isomorphism between the n-th Tate cohomology and n-th group cohomology for n : ℕ non-zero.

• isoGroupHomology: the isomorphism between the -n-1-th Tate cohomology and n-th group homology for n : ℕ non-zero.

Main Results

• δ_naturality: the naturality of the connecting homomorphism in the long exact sequence of Tate cohomology.

Tags

Tate cohomology, homological algebra

This file comes from a collaborative work in 2025 ClassFieldTheory workshop, see https://github.com/kbuzzard/ClassFieldTheory/ for more information.

noncomputable def Rep.tateNorm {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : (groupHomology.inhomogeneousChains M).X 0 ⟶ (groupCohomology.inhomogeneousCochains M).X 0

This is the map from the coinvariants of M : Rep R G to the invariants, induced by the map m ↦ ∑ g : G, M.ρ g m.

Equations

• M.tateNorm = CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₀ M).hom (CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom M.norm) (groupCohomology.cochainsIso₀ M).inv)

theorem Rep.tateNorm_eq {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : M.tateNorm = ModuleCat.ofHom ((Finsupp.lsum R) fun (x : Fin 0 → G) => LinearMap.pi fun (x : Fin 0 → G) => M.ρ.norm)

@[simp]

theorem Rep.norm_comp_d_eq_zero {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp (Hom.toModuleCatHom M.norm) (groupCohomology.d₀₁ M) = 0

@[simp]

theorem Rep.norm_comp_d_eq_zero_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) {Z : ModuleCat R} (h : ModuleCat.of R (G → ↑M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.toModuleCatHom M.norm) (CategoryTheory.CategoryStruct.comp (groupCohomology.d₀₁ M) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem Rep.norm_comp_d_eq_zero_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (x : ↑M) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₀₁ M)) (M.ρ.norm x) = 0

theorem Rep.tateNorm_comp_d {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp M.tateNorm ((groupCohomology.inhomogeneousCochains M).d 0 1) = 0

@[simp]

theorem Rep.comp_eq_zero {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp (groupHomology.d₁₀ M) (Hom.toModuleCatHom M.norm) = 0

theorem Rep.d_comp_tateNorm {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CategoryTheory.CategoryStruct.comp ((groupHomology.inhomogeneousChains M).d 1 0) M.tateNorm = 0

noncomputable def tateComplexConnectData {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CochainComplex.ConnectData (groupHomology.inhomogeneousChains M) (groupCohomology.inhomogeneousCochains M)

The Tate norm connecting complexes of inhomogeneous chains and cochains.

Equations

• tateComplexConnectData M = { d₀ := M.tateNorm, comp_d₀ := ⋯, d₀_comp := ⋯ }

@[simp]

theorem tateComplexConnectData_d₀ {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : (tateComplexConnectData M).d₀ = M.tateNorm

@[reducible, inline]

noncomputable abbrev tateComplex {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : CochainComplex (ModuleCat R) ℤ

The Tate complex defined by connecting inhomogeneous chains and cochains with the Tate norm.

Equations

• tateComplex M = (tateComplexConnectData M).cochainComplex

theorem tateComplex_d_neg_one {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) : (tateComplex M).d (-1) 0 = M.tateNorm

theorem tateComplex_d_ofNat {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) : (tateComplex M).d (↑n) (↑n + 1) = (groupCohomology.inhomogeneousCochains M).d n (n + 1)

theorem tateComplex_d_neg {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℕ) : (tateComplex M).d (-(↑n + 2)) (-(↑n + 1)) = (groupHomology.inhomogeneousChains M).d (n + 1) n

@[reducible]

noncomputable def tateComplex.map {R G : Type u} [CommRing R] [Group G] [Fintype G] {X Y : Rep R G} (φ : X ⟶ Y) : tateComplex X ⟶ tateComplex Y

The chain map on the Tate complex induced by a morphism of representations.

Equations

• tateComplex.map φ = (tateComplexConnectData X).map (tateComplexConnectData Y) (groupHomology.chainsMap (MonoidHom.id G) φ) (groupCohomology.cochainsMap (MonoidHom.id G) φ) ⋯

@[simp]

theorem tateComplex.map_zero {R G : Type u} [CommRing R] [Group G] [Fintype G] {X Y : Rep R G} : map 0 = 0

theorem tateComplex.map_add {R G : Type u} [CommRing R] [Group G] [Fintype G] {X Y : Rep R G} (f g : X ⟶ Y) : map (f + g) = map f + map g

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

The functor taking a representation of G to its Tate complex.

Equations

• tateComplexFunctor R G = { obj := fun (M : Rep R G) => tateComplex M, map := fun {X Y : Rep R G} => tateComplex.map, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem tateComplexFunctor_obj (R G : Type u) [CommRing R] [Group G] [Fintype G] (M : Rep R G) : (tateComplexFunctor R G).obj M = tateComplex M

@[simp]

theorem tateComplexFunctor_map (R G : Type u) [CommRing R] [Group G] [Fintype G] {X✝ Y✝ : Rep R G} (φ : X✝ ⟶ Y✝) : (tateComplexFunctor R G).map φ = tateComplex.map φ

noncomputable def tateCohomologyFunctor {R G : Type u} [CommRing R] [Group G] [Fintype G] (n : ℤ) : CategoryTheory.Functor (Rep R G) (ModuleCat R)

The functor taking a representation of G to its n-th Tate cohomology group.

Equations

• tateCohomologyFunctor n = (tateComplexFunctor R G).comp (HomologicalComplex.homologyFunctor (ModuleCat R) (ComplexShape.up ℤ) n)

@[reducible, inline]

noncomputable abbrev tateCohomology {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep R G) (n : ℤ) : ModuleCat R

The shortcut path of taking Tate cohomology which aligns with groupCohomology and groupHomology.

Equations

• tateCohomology M n = (tateCohomologyFunctor n).obj M

instance TateCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor {R G : Type u} [CommRing R] [Group G] [Fintype G] : (tateComplexFunctor R G).PreservesZeroMorphisms

noncomputable def TateCohomology.tateComplex.evalNonneg {R G : Type u} [CommRing R] [Group G] [Fintype G] (n : ℕ) : (tateComplexFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) ↑n) ≅ (groupCohomology.cochainsFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℕ) n)

The natural isomorphism between the n-th index of the Tate complex and inhomogeneous n-cochains for 0 ≤ n.

Equations

• TateCohomology.tateComplex.evalNonneg n = CategoryTheory.Iso.refl ((tateComplexFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) ↑n))

noncomputable def TateCohomology.tateComplex.evalNeg {R G : Type u} [CommRing R] [Group G] [Fintype G] (n : ℕ) : (tateComplexFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.negSucc n)) ≅ (groupHomology.chainsFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.down ℕ) n)

The natural isomorphism between the n-th index of the Tate complex and inhomogeneous n-chains for n < 0.

Equations

• TateCohomology.tateComplex.evalNeg n = CategoryTheory.Iso.refl ((tateComplexFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) (Int.negSucc n)))

instance TateCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatIntTateComplexFunctor_1 {R G : Type u} [CommRing R] [Group G] [Fintype G] : (tateComplexFunctor R G).PreservesZeroMorphisms

theorem TateCohomology.map_tateComplexFunctor_shortExact {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) : (S.map (tateComplexFunctor R G)).ShortExact

instance TateCohomology.instAdditiveRepCochainComplexModuleCatIntTateComplexFunctor {R G : Type u} [CommRing R] [Group G] [Fintype G] : (tateComplexFunctor R G).Additive

instance TateCohomology.preservesFiniteLimits_tateComplexFunctor {R G : Type u} [CommRing R] [Group G] [Fintype G] : CategoryTheory.Limits.PreservesFiniteLimits (tateComplexFunctor R G)

The next two statements say that tateComplexFunctor is an exact functor from Rep R G to CochainComplex (ModuleCat R) ℤ.

instance TateCohomology.preservesFiniteColimits_tateComplexFunctor {R G : Type u} [CommRing R] [Group G] [Fintype G] : CategoryTheory.Limits.PreservesFiniteColimits (tateComplexFunctor R G)

@[reducible, inline]

noncomputable abbrev TateCohomology.δ {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) (n : ℤ) : tateCohomology S.X₃ n ⟶ tateCohomology S.X₁ (n + 1)

The connecting homomorphism in group cohomology induced by a short exact sequence of G-modules.

Equations

• TateCohomology.δ hS n = ⋯.δ n (n + 1) ⋯

theorem TateCohomology.map_δ {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) (n : ℤ) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor n).map S.g) (δ hS n) = 0

This and δ_map are the preliminary results for the long exact sequence in Tate cohomology induced by a short exact sequence of G-reps.

theorem TateCohomology.δ_map {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) (n : ℤ) : CategoryTheory.CategoryStruct.comp (δ hS n) ((tateCohomologyFunctor (n + 1)).map S.f) = 0

theorem TateCohomology.exact₃ {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) (n : ℤ) : { X₁ := (tateCohomologyFunctor n).obj S.X₂, X₂ := (tateCohomologyFunctor n).obj S.X₃, X₃ := tateCohomology S.X₁ (n + 1), f := (tateCohomologyFunctor n).map S.g, g := δ hS n, zero := ⋯ }.Exact

theorem TateCohomology.exact₁ {R G : Type u} [CommRing R] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep R G)} (hS : S.ShortExact) (n : ℤ) : { X₁ := tateCohomology S.X₃ n, X₂ := tateCohomology S.X₁ (n + 1), X₃ := (tateCohomologyFunctor (n + 1)).obj S.X₂, f := δ hS n, g := (tateCohomologyFunctor (n + 1)).map S.f, zero := ⋯ }.Exact

theorem TateCohomology.δ_naturality {R G : Type u} [CommRing R] [Group G] [Fintype G] {X1 X2 : CategoryTheory.ShortComplex (Rep R G)} (hX1 : X1.ShortExact) (hX2 : X2.ShortExact) (F : X1 ⟶ X2) (i : ℤ) : CategoryTheory.CategoryStruct.comp (δ hX1 i) ((tateCohomologyFunctor (i + 1)).map F.τ₁) = CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map F.τ₃) (δ hX2 i)

noncomputable def TateCohomology.isoGroupCohomology {R G : Type u} [CommRing R] [Group G] [Fintype G] (n : ℕ) [NeZero n] : tateCohomologyFunctor ↑n ≅ groupCohomology.functor R G n

The isomorphism between the n-th Tate cohomology and n-th group cohomology for n : ℕ non-zero.

Equations

• TateCohomology.isoGroupCohomology n = CategoryTheory.NatIso.ofComponents (fun (M : Rep R G) => (tateComplexConnectData M).homologyIsoPos n ↑n ⋯) ⋯

noncomputable def TateCohomology.isoGroupHomology {R G : Type u} [CommRing R] [Group G] [Fintype G] (m : ℤ) (n : ℕ) (hmn : m = -(↑n + 1)) [NeZero n] : tateCohomologyFunctor m ≅ groupHomology.functor R G n

The isomorphism between the -n-1-th Tate cohomology and n-th group homology for n : ℕ non-zero.

Equations

• TateCohomology.isoGroupHomology m n hmn = CategoryTheory.NatIso.ofComponents (fun (M : Rep R G) => (tateComplexConnectData M).homologyIsoNeg n m hmn) ⋯