Tate cohomology of a directed union of subrepresentations

Let G be a finite group and M a representation of G that is the directed union of subrepresentations A i, in the sense that the maps f i : A i ⟶ M are injective and every finite subset of M lies in the image of one of them. This file shows that every Tate cohomology class of M, in every integer degree, comes from one of the A i (TauCeti.TateCohomology.exists_tateCohomologyFunctor_map_eq).

In degree n ≥ 0 the Tate complex of M consists of the functions Gⁿ → M, and in degree n < 0 of the finitely supported functions G^(-n-1) → M. Either way an element has finitely many values, since G is finite, so it comes from some A i (exists_tateComplex_map_f_eq). The maps of Tate complexes induced by the f i are injective in every degree (tateComplex_map_f_injective), so a lift of a cocycle is a cocycle, and the statement follows from its counterpart for complexes of modules, HomologicalComplex.exists_homologyMap_eq_of_injective.

This is how the Tate cohomology of the ideles of a number field, the union of the S-ideles over the finite sets S of places, is computed from that of the S-ideles.

Main results

• TauCeti.TateCohomology.exists_tateCohomologyFunctor_map_eq: a Tate cohomology class of a directed union of subrepresentations comes from one of them.

References

• J. S. Milne, Class Field Theory, Chapter VII, §2.

theorem TauCeti.TateCohomology.tateComplex_map_f_injective {k G : Type u} [CommRing k] [Group G] [Fintype G] {M N : Rep k G} (f : M ⟶ N) (hf : Function.Injective ⇑(Rep.Hom.hom f)) (n : ℤ) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((tateComplex.map f).f n))

An injective morphism of representations induces injective maps on the Tate complexes, in every degree.

theorem TauCeti.TateCohomology.exists_tateComplex_map_f_eq {k G : Type u} [CommRing k] [Group G] [Fintype G] {κ : Type u_1} {M : Rep k G} {A : κ → Rep k G} (f : (i : κ) → A i ⟶ M) (hf : ∀ (i : κ), Function.Injective ⇑(Rep.Hom.hom (f i))) (h : ∀ (s : Finset ↑M), ∃ (i : κ), ∀ m ∈ s, m ∈ Set.range ⇑(Rep.Hom.hom (f i))) (n : ℤ) (z : ↑((tateComplex M).X n)) : ∃ (i : κ) (y : ↑((tateComplex (A i)).X n)), (CategoryTheory.ConcreteCategory.hom ((tateComplex.map (f i)).f n)) y = z

If every finite subset of M lies in the image of one of the maps f i : A i ⟶ M, then every element of the Tate complex of M, in every degree, comes from the Tate complex of one of the A i.

theorem TauCeti.TateCohomology.exists_tateCohomologyFunctor_map_eq {k G : Type u} [CommRing k] [Group G] [Fintype G] {κ : Type u_1} {M : Rep k G} {A : κ → Rep k G} (f : (i : κ) → A i ⟶ M) (hf : ∀ (i : κ), Function.Injective ⇑(Rep.Hom.hom (f i))) (h : ∀ (s : Finset ↑M), ∃ (i : κ), ∀ m ∈ s, m ∈ Set.range ⇑(Rep.Hom.hom (f i))) (n : ℤ) (x : ↑(tateCohomology M n)) : ∃ (i : κ) (y : ↑((tateCohomologyFunctor n).obj (A i))), (ModuleCat.Hom.hom ((tateCohomologyFunctor n).map (f i))) y = x

Tate cohomology of a directed union. Let f i : A i ⟶ M be injective morphisms of representations of a finite group such that every finite subset of M lies in the image of one of them. Then every class of H-hat^n(G, M), for every n : ℤ, is the image of a class of H-hat^n(G, A i) for some i.