Tate's isomorphism criterion for a morphism of representations

Let G be a finite group and f : A ⟶ B a morphism of representations of G. Suppose that for every subgroup S of G of prime-power order the map induced by f on the Tate cohomology of S is surjective in degree q - 1, bijective in degree q and injective in degree q + 1. Then f induces isomorphisms Ĥⁿ(S, A) ≃ Ĥⁿ(S, B) in every integer degree n, for every subgroup S of G (TauCeti.TateCohomology.map_res_bijective_of_forall_isPGroup), and in particular for G itself (TauCeti.TateCohomology.map_bijective_of_forall_isPGroup).

This is the heart of Tate's theorem in the form given by Artin and Tate (Class Field Theory, Preliminaries, §2, Theorem A): once the cohomology class is moved to degree zero by dimension shifting, their cup-product criterion is the case of this statement in which f is the morphism ℤ ⟶ A, 1 ↦ a, attached to an invariant a. The proof is the standard one. Replace f by the monomorphism A ⟶ B ⊞ Coind_⊥^G A with components f and the coinduction unit; the second summand has no Tate cohomology on any subgroup, so this changes nothing on cohomology. The long exact sequence of the cokernel C then shows that the Tate cohomology of C vanishes in the two consecutive degrees q - 1 and q on every subgroup of prime-power order, so C is cohomologically trivial by Tate's triviality criterion (TauCeti.TateCohomology.isZero_of_forall_isPGroup), and the long exact sequence gives the conclusion in every degree.

The other classical route to Tate's theorem, through the splitting module of a degree-two class (Serre, Local Fields, Chapter IX, §8; ClassFieldTheory/Cohomology/SplittingModule.lean in kbuzzard/ClassFieldTheory), is not taken here: the criterion below applies to any morphism and any triple of consecutive degrees, which is what the cup-product formulation of Tate's theorem consumes.

Main statements

• TauCeti.TateCohomology.map_res_bijective_of_forall_isPGroup: the criterion, with the conclusion on every subgroup of G.
• TauCeti.TateCohomology.map_bijective_of_forall_isPGroup: the criterion, with the conclusion on G itself.

References

• E. Artin and J. Tate, Class Field Theory, Preliminaries, §2, Theorem A.
• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter IV (Atiyah–Wall), §10.
• J.-P. Serre, Local Fields, Chapter IX, §8.

theorem TauCeti.TateCohomology.map_res_bijective_of_forall_isPGroup {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) [Finite G] {q : ℤ} (hsurj : ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S], IsPGroup p ↥S → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor (q - 1)).map ((Rep.resFunctor S.subtype).map f)))) (hbij : ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S], IsPGroup p ↥S → Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor q).map ((Rep.resFunctor S.subtype).map f)))) (hinj : ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S], IsPGroup p ↥S → Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor (q + 1)).map ((Rep.resFunctor S.subtype).map f)))) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map ((Rep.resFunctor S.subtype).map f)))

Tate's isomorphism criterion, on every subgroup. Let G be a finite group and f : A ⟶ B a morphism of representations of G. If, for every subgroup S of G of prime-power order, the map induced by f on the Tate cohomology of S is surjective in degree q - 1, bijective in degree q and injective in degree q + 1, then it is bijective in every degree n for every subgroup S of G.

theorem TauCeti.TateCohomology.map_bijective_of_forall_isPGroup {k G : Type u} [CommRing k] [Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) [Fintype G] {q : ℤ} (hsurj : ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S], IsPGroup p ↥S → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor (q - 1)).map ((Rep.resFunctor S.subtype).map f)))) (hbij : ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S], IsPGroup p ↥S → Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor q).map ((Rep.resFunctor S.subtype).map f)))) (hinj : ∀ (p : ℕ) [Fact (Nat.Prime p)] (S : Subgroup G) [inst : Fintype ↥S], IsPGroup p ↥S → Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor (q + 1)).map ((Rep.resFunctor S.subtype).map f)))) (n : ℤ) : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map f))

Tate's isomorphism criterion. Let G be a finite group and f : A ⟶ B a morphism of representations of G. If, for every subgroup S of G of prime-power order, the map induced by f on the Tate cohomology of S is surjective in degree q - 1, bijective in degree q and injective in degree q + 1, then f induces a bijection Ĥⁿ(G, A) → Ĥⁿ(G, B) in every degree n.