Torsion of group cohomology and restriction to Sylow subgroups

For a finite group G, the composite Cor ∘ Res : Hⁿ(G, A) ⟶ Hⁿ(S, A) ⟶ Hⁿ(G, A) is multiplication by the index [G : S]. Taking S trivial shows that Hⁿ(G, A) is killed by the order of G for n ≥ 1; taking S a Sylow p-subgroup shows that restriction to S is injective on the p-primary part of Hⁿ(G, A), because [G : S] is prime to p. Consequently Hⁿ(G, A) vanishes for n ≥ 1 as soon as, for every prime p dividing the order of G, Hⁿ(P, A) vanishes for some Sylow p-subgroup P, which is the reduction step of Tate's cohomological triviality criterion.

Main statements

• TauCeti.groupCohomology.eq_zero_of_pow_nsmul_eq_zero_of_map_sylow_eq_zero: an element of Hⁿ(G, A) killed by a power of p and by restriction to a Sylow p-subgroup is zero.
• TauCeti.groupCohomology.eq_zero_of_map_sylow_eq_zero: an element of Hⁿ⁺¹(G, A) whose restriction to a Sylow p-subgroup vanishes for every prime p is zero.
• TauCeti.groupCohomology.isZero_of_isZero_sylow: Hⁿ⁺¹(G, A) = 0 if, for every prime p dividing the order of G, Hⁿ⁺¹(P, A) = 0 for some Sylow p-subgroup P.

References

• J. S. Milne, Class Field Theory, Chapter II, Corollaries 1.31 and 1.33 and Theorem 3.10.
• The same facts appear as torsion_of_finite_of_neZero and groupCohomology_Sylow in ClassFieldTheory/Cohomology/Functors/Corestriction.lean and in the Sylow step of ClassFieldTheory/Cohomology/TrivialityCriterion.lean in kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509; they are reimplemented here on Tau Ceti's corestriction API.

theorem TauCeti.groupCohomology.eq_zero_of_pow_nsmul_eq_zero_of_map_sylow_eq_zero {k G : Type u} [CommRing k] [Group G] [Finite G] (A : Rep.{u, u, u} k G) (n p : ℕ) [Fact (Nat.Prime p)] (P : Sylow p G) {x : ↑(groupCohomology A n)} {j : ℕ} (hx : p ^ j • x = 0) (h : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (↑P).subtype (CategoryTheory.CategoryStruct.id (Rep.res (↑P).subtype A)) n)) x = 0) : x = 0

Restriction to a Sylow p-subgroup is injective on the p-primary part (Milne II 1.33): an element of Hⁿ(G, A) killed by a power of p whose restriction to a Sylow p-subgroup P vanishes is zero.

theorem TauCeti.groupCohomology.eq_zero_of_map_sylow_eq_zero {k G : Type u} [CommRing k] [Group G] [Finite G] (A : Rep.{u, u, u} k G) (n : ℕ) {x : ↑(groupCohomology A (n + 1))} (h : ∀ (p : ℕ) [Fact (Nat.Prime p)], p ∣ Nat.card G → ∃ (P : Sylow p G), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (↑P).subtype (CategoryTheory.CategoryStruct.id (Rep.res (↑P).subtype A)) (n + 1))) x = 0) : x = 0

Restriction to the Sylow subgroups is jointly injective (Milne II 1.33): an element of Hⁿ⁺¹(G, A) whose restriction vanishes, for every prime p dividing the order of G, on some Sylow p-subgroup is zero.

theorem TauCeti.groupCohomology.isZero_of_isZero_sylow {k G : Type u} [CommRing k] [Group G] [Finite G] (A : Rep.{u, u, u} k G) (n : ℕ) (h : ∀ (p : ℕ) [Fact (Nat.Prime p)], p ∣ Nat.card G → ∃ (P : Sylow p G), CategoryTheory.Limits.IsZero (groupCohomology (Rep.res (↑P).subtype A) (n + 1))) : CategoryTheory.Limits.IsZero (groupCohomology A (n + 1))

The Sylow reduction of Tate's triviality criterion (Milne II 3.10, last paragraph): if, for every prime p dividing the order of G, Hⁿ⁺¹(P, A) = 0 for some Sylow p-subgroup P, then Hⁿ⁺¹(G, A) = 0.