Consequences of the long exact sequence in Tate cohomology

Let G be a finite group and 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 a short exact sequence of representations of G. Mathlib provides the connecting homomorphism TateCohomology.δ and the exactness of the long exact sequence at the terms Ĥⁿ(G, X₁) (TateCohomology.exact₁) and Ĥⁿ(G, X₃) (TateCohomology.exact₃). This file adds the exactness at Ĥⁿ(G, X₂) (TateCohomology.exact₂, in the same namespace as its two Mathlib siblings) and records how the vanishing of the Tate cohomology of X₃ controls the map induced by X₁ ⟶ X₂: if Ĥⁿ(G, X₃) vanishes the induced map is surjective in degree n and injective in degree n + 1, and conversely surjectivity in degree n together with injectivity in degree n + 1 forces Ĥⁿ(G, X₃) to vanish. These are the two halves of the argument that a morphism of representations inducing isomorphisms in three consecutive degrees on every subgroup induces isomorphisms in every degree. Likewise, vanishing of the Tate cohomology of two of the three terms, in the degrees the long exact sequence connects, forces it for the third, and vanishing of the Tate cohomology of X₂ in two consecutive degrees makes the connecting map bijective.

Finally, for a 3 × 3 diagram of representations with short exact rows and columns, the two composites of connecting maps between opposite corners differ by a sign. This is the sign rule relating the compatibility of the cup product with connecting maps in its two variables.

Main statements

• TateCohomology.exact₂: exactness of Ĥⁿ(G, X₁) ⟶ Ĥⁿ(G, X₂) ⟶ Ĥⁿ(G, X₃).
• TauCeti.TateCohomology.map_f_surjective_of_isZero_X₃, TauCeti.TateCohomology.map_f_injective_of_isZero_X₃: vanishing of the Tate cohomology of X₃ makes the map induced by X₁ ⟶ X₂ surjective in that degree and injective in the next.
• TauCeti.TateCohomology.isZero_X₃_of_surjective_of_injective: the converse, from two consecutive degrees.
• TauCeti.TateCohomology.isZero_X₁_of_surjective_of_injective: surjectivity in degree n - 1 and injectivity in degree n of the map induced by X₂ ⟶ X₃ force H-hat^n(G, X₁) to vanish.
• TauCeti.TateCohomology.isZero_X₂_of_isZero_X₁_of_isZero_X₃, TauCeti.TateCohomology.isZero_X₃_of_isZero_X₂_of_isZero_X₁, TauCeti.TateCohomology.isZero_X₁_of_isZero_X₃_of_isZero_X₂: two-out-of-three for the vanishing of Tate cohomology along a short exact sequence.
• TauCeti.TateCohomology.natCard_tateCohomology_dvd_of_shortExact: the order of the middle Tate group divides the product of the orders of the outer ones.
• TauCeti.TateCohomology.isIso_map_τ₁_of_isIso_δ: a morphism of short exact sequences inducing isomorphisms on the third terms in degree n and on the connecting maps induces an isomorphism on the first terms in degree n + 1.
• TauCeti.TateCohomology.δ_comp_δ_eq_neg: the connecting maps of a 3 × 3 diagram of representations with short exact rows and columns anticommute.

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

Exactness of Ĥⁿ(G, X₁) ⟶ Ĥⁿ(G, X₂) ⟶ Ĥⁿ(G, X₃), the middle term of the long exact sequence in Tate cohomology of a short exact sequence of representations.

theorem TauCeti.TateCohomology.map_f_surjective_of_isZero_X₃ {k G : Type u} [CommRing k] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) (n : ℤ) (h : CategoryTheory.Limits.IsZero (tateCohomology S.X₃ n)) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map S.f))

If Ĥⁿ(G, X₃) = 0, the map Ĥⁿ(G, X₁) ⟶ Ĥⁿ(G, X₂) induced by X₁ ⟶ X₂ is surjective.

theorem TauCeti.TateCohomology.map_f_injective_of_isZero_X₃ {k G : Type u} [CommRing k] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) (m n : ℤ) (hmn : m + 1 = n) (h : CategoryTheory.Limits.IsZero (tateCohomology S.X₃ m)) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map S.f))

If Ĥᵐ(G, X₃) = 0, the map Ĥⁿ(G, X₁) ⟶ Ĥⁿ(G, X₂) induced by X₁ ⟶ X₂ is injective in the next degree n = m + 1.

theorem TauCeti.TateCohomology.isZero_X₃_of_surjective_of_injective {k G : Type u} [CommRing k] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) (m n : ℤ) (hmn : m + 1 = n) (hsurj : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor m).map S.f))) (hinj : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map S.f))) : CategoryTheory.Limits.IsZero (tateCohomology S.X₃ m)

If the map induced by X₁ ⟶ X₂ on Tate cohomology is surjective in degree m and injective in degree n = m + 1, then Ĥᵐ(G, X₃) = 0.

theorem TauCeti.TateCohomology.isZero_X₁_of_surjective_of_injective {k G : Type u} [CommRing k] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) (m n : ℤ) (hmn : m + 1 = n) (hsurj : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor m).map S.g))) (hinj : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map S.g))) : CategoryTheory.Limits.IsZero (tateCohomology S.X₁ n)

If the map induced by X₂ ⟶ X₃ on Tate cohomology is surjective in degree m and injective in degree n = m + 1, then H-hat^n(G, X₁) = 0.

theorem TauCeti.TateCohomology.isZero_X₂_of_isZero_X₁_of_isZero_X₃ {k G : Type u} [CommRing k] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) (n : ℤ) (h₁ : CategoryTheory.Limits.IsZero (tateCohomology S.X₁ n)) (h₃ : CategoryTheory.Limits.IsZero (tateCohomology S.X₃ n)) : CategoryTheory.Limits.IsZero (tateCohomology S.X₂ n)

If Ĥⁿ(G, X₁) = 0 and Ĥⁿ(G, X₃) = 0, then Ĥⁿ(G, X₂) = 0.

theorem TauCeti.TateCohomology.isZero_X₃_of_isZero_X₂_of_isZero_X₁ {k G : Type u} [CommRing k] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) (m n : ℤ) (hmn : m + 1 = n) (h₂ : CategoryTheory.Limits.IsZero (tateCohomology S.X₂ m)) (h₁ : CategoryTheory.Limits.IsZero (tateCohomology S.X₁ n)) : CategoryTheory.Limits.IsZero (tateCohomology S.X₃ m)

If Ĥᵐ(G, X₂) = 0 and Ĥⁿ(G, X₁) = 0 in the next degree n = m + 1, then Ĥᵐ(G, X₃) = 0.

theorem TauCeti.TateCohomology.isZero_X₁_of_isZero_X₃_of_isZero_X₂ {k G : Type u} [CommRing k] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) (m n : ℤ) (hmn : m + 1 = n) (h₃ : CategoryTheory.Limits.IsZero (tateCohomology S.X₃ m)) (h₂ : CategoryTheory.Limits.IsZero (tateCohomology S.X₂ n)) : CategoryTheory.Limits.IsZero (tateCohomology S.X₁ n)

If Ĥᵐ(G, X₃) = 0 and Ĥⁿ(G, X₂) = 0 in the next degree n = m + 1, then Ĥⁿ(G, X₁) = 0.

theorem TauCeti.TateCohomology.δ_bijective_of_isZero_X₂ {k G : Type u} [CommRing k] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) (n : ℤ) (h₀ : CategoryTheory.Limits.IsZero (tateCohomology S.X₂ n)) (h₁ : CategoryTheory.Limits.IsZero (tateCohomology S.X₂ (n + 1))) : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (TateCohomology.δ hS n))

If Ĥⁿ(G, X₂) = 0 and Ĥⁿ⁺¹(G, X₂) = 0, the connecting map Ĥⁿ(G, X₃) ⟶ Ĥⁿ⁺¹(G, X₁) is bijective.

theorem TauCeti.TateCohomology.δ_comp_δ_eq_neg {k G : Type u} [CommRing k] [Group G] [Fintype G] (D : CategoryTheory.ShortComplex (CategoryTheory.ShortComplex (Rep k G))) (h₁ : D.X₁.ShortExact) (h₂ : D.X₂.ShortExact) (h₃ : D.X₃.ShortExact) (h₁' : (D.map CategoryTheory.ShortComplex.π₁).ShortExact) (h₂' : (D.map CategoryTheory.ShortComplex.π₂).ShortExact) (h₃' : (D.map CategoryTheory.ShortComplex.π₃).ShortExact) (n : ℤ) : CategoryTheory.CategoryStruct.comp (TateCohomology.δ h₃ n) (TateCohomology.δ h₁' (n + 1)) = -CategoryTheory.CategoryStruct.comp (TateCohomology.δ h₃' n) (TateCohomology.δ h₁ (n + 1))

The connecting maps of a 3 × 3 diagram anticommute in Tate cohomology. Let D be a 3 × 3 diagram of representations, presented as a short complex D.X₁ ⟶ D.X₂ ⟶ D.X₃ of short complexes, all of whose rows D.Xᵢ and columns D.map π_j are short exact. Then the two composites of connecting maps Ĥⁿ(G, X₃₃) ⟶ Ĥⁿ⁺²(G, X₁₁), through the third row and the first column, and through the third column and the first row, differ by a sign.

theorem TauCeti.TateCohomology.isIso_map_τ₁_of_isIso_δ {k G : Type u} [CommRing k] [Group G] [Fintype G] {A B : CategoryTheory.ShortComplex (Rep k G)} (hA : A.ShortExact) (hB : B.ShortExact) (Φ : A ⟶ B) (n : ℤ) [CategoryTheory.IsIso (TateCohomology.δ hA n)] [CategoryTheory.IsIso (TateCohomology.δ hB n)] [CategoryTheory.IsIso ((tateCohomologyFunctor n).map Φ.τ₃)] : CategoryTheory.IsIso ((tateCohomologyFunctor (n + 1)).map Φ.τ₁)

Isomorphisms transported along connecting maps. For a morphism Φ : A ⟶ B of short exact sequences of representations whose connecting maps in degree n are isomorphisms and which induces an isomorphism on the third terms in degree n, the induced map on the first terms is an isomorphism in degree n + 1.

theorem TauCeti.TateCohomology.natCard_tateCohomology_dvd_of_shortExact {k G : Type u} [CommRing k] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep k G)} (hS : S.ShortExact) (n : ℤ) : Nat.card ↑(tateCohomology S.X₂ n) ∣ Nat.card ↑(tateCohomology S.X₁ n) * Nat.card ↑(tateCohomology S.X₃ n)

In the long exact sequence of Tate cohomology, the middle Tate group in degree n is squeezed between the two outer ones: its order divides their product. In particular it is finite as soon as they are.