Tate's cohomological triviality criterion

Let G be a finite group and A a representation of G. If the cohomology of A vanishes in two consecutive degrees on every subgroup of G of prime-power order, then it vanishes in every degree on every subgroup of G (Milne, Class Field Theory, II 3.10). This file proves the criterion for ordinary cohomology in positive degrees and for Tate cohomology in all integer degrees. It is the step of Tate's theorem that makes the splitting module of a degree-two cohomology class cohomologically trivial.

The proof has three steps.

• For a finite cyclic group, cohomology in positive degrees is two-periodic, so vanishing in two consecutive positive degrees gives vanishing in all of them (isZero_succ_of_isCyclic_of_isZero).
• For a subgroup S of prime-power order, argue by induction on #S. A nontrivial such S has a normal subgroup T of index p with S ⧸ T cyclic. By induction the cohomology of T vanishes in every positive degree, so inflation Hⁿ⁺¹(S ⧸ T, A^T) ⟶ Hⁿ⁺¹(S, A) is an isomorphism in every degree, and the cyclic case applies to S ⧸ T.
• For an arbitrary subgroup, restriction to Sylow subgroups detects vanishing (TauCeti.groupCohomology.isZero_of_isZero_sylow).

Tate cohomology is reduced to the ordinary case by dimension shifting: Tate cohomology of dimensionShiftDown A in degree n + 1 is Tate cohomology of A in degree n, on every subgroup at once, so enough downward shifts move both the hypothesis and the conclusion into positive degrees.

Main statements

• TauCeti.groupCohomology.isZero_succ_of_isCyclic_of_isZero: for a finite cyclic group, vanishing of H^{q+1} and H^{q+2} implies vanishing of Hⁿ⁺¹ for every n.
• TauCeti.groupCohomology.isZero_of_forall_isPGroup: the criterion for ordinary cohomology in positive degrees.
• TauCeti.TateCohomology.isZero_of_forall_isPGroup: the criterion for Tate cohomology in all integer degrees.

References

• J. S. Milne, Class Field Theory, Chapter II, Theorem 3.10.
• J.-P. Serre, Local Fields, Chapter IX, §5 (the criterion for a finite group, via its Sylow subgroups) and §8 (its use in the theorem of Tate and Nakayama).
• ClassFieldTheory/Cohomology/TrivialityCriterion.lean in kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509, proves the same criterion (groupCohomology.trivialCohomology_of_even_of_odd and Rep.tateCohomology_of_trivialCohomology) by the same three steps, for hypotheses on all injective group homomorphisms into G; it is reimplemented here for subgroups of prime-power order, on Tau Ceti's inflation-restriction, Sylow and dimension-shifting API.

theorem TauCeti.groupCohomology.isZero_succ_of_isCyclic_of_isZero {k G : Type u} [CommRing k] [Group G] [Finite G] [IsCyclic G] (A : Rep.{u, u, u} k G) {q : ℕ} (h₁ : CategoryTheory.Limits.IsZero (groupCohomology A (q + 1))) (h₂ : CategoryTheory.Limits.IsZero (groupCohomology A (q + 2))) (n : ℕ) : CategoryTheory.Limits.IsZero (groupCohomology A (n + 1))

Periodicity for a finite cyclic group. If the cohomology of a finite cyclic group vanishes in the two consecutive positive degrees q + 1 and q + 2, it vanishes in every positive degree.

theorem TauCeti.groupCohomology.isZero_of_forall_isPGroup {k G : Type u} [CommRing k] [Group G] [Finite G] (A : Rep.{u, u, u} k G) {q : ℕ} (h₁ : ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G), IsPGroup p ↥S → CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype A) (q + 1))) (h₂ : ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G), IsPGroup p ↥S → CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype A) (q + 2))) (S : Subgroup G) (n : ℕ) : CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype A) (n + 1))

Tate's cohomological triviality criterion for ordinary cohomology (Milne II 3.10). Let G be a finite group and A a representation of G. If H^{q+1}(S, A) and H^{q+2}(S, A) vanish for every subgroup S of G of prime-power order, then Hⁿ⁺¹(S, A) vanishes for every subgroup S of G and every n.

theorem TauCeti.TateCohomology.isZero_of_forall_isPGroup {k G : Type u} [CommRing k] [Group G] [Finite G] (A : Rep.{u, u, u} k G) {q : ℤ} (h₁ : ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S], IsPGroup p ↥S → CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A) q)) (h₂ : ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S], IsPGroup p ↥S → CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A) (q + 1))) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A) n)

Tate's cohomological triviality criterion (Milne II 3.10). Let G be a finite group and A a representation of G. If its Tate cohomology vanishes in degrees q and q + 1 for every subgroup S of G of prime-power order, then it vanishes in degree n for every subgroup S of G and every integer n.