Restriction in positive Tate degrees

TauCeti.RepresentationTheory.Homological.TateCohomology.Restriction.Basic supplies restriction in degree 0, in degree -1, and in every degree at most -2. This file supplies the positive degrees, so that a restriction map

tateCohomology M r ⟶ tateCohomology (Rep.res H.subtype M) r

is now available in every integer degree r.

In degrees ≥ 1 the Tate complex is the complex of inhomogeneous cochains, so restriction is the ordinary restriction of group cohomology, transported through Mathlib's comparison TateCohomology.isoGroupCohomology. On a cochain this is the formula already used by TauCeti.groupCohomology.map: a cochain c on G is pulled back to H along the subgroup inclusion, (h₁ ⋯ hₙ) ↦ c (h₁ ⋯ hₙ), and composed with the identity on the restricted coefficient module.

Main definitions

• TauCeti.TateCohomology.posRes: restriction in Tate degree n + 1, for n : ℕ.

Main results

• TauCeti.TateCohomology.posRes_comp_isoGroupCohomology_hom: positive-degree Tate restriction is the ordinary cohomological restriction TauCeti.groupCohomology.map along H.subtype, read through Mathlib's comparison TateCohomology.isoGroupCohomology.
• TauCeti.TateCohomology.posRes_natural: positive-degree Tate restriction is natural in the coefficient module, the discrete counterpart of TauCeti.ContinuousCohomology.coeffMap_comp_res.
• TauCeti.TateCohomology.posRes_trans: positive-degree Tate restriction is transitive along a tower of subgroups, the counterpart of TauCeti.TateCohomology.negSuccRes_trans, read off TauCeti.groupCohomology.map_subgroupOf_trans.

One structural observation is worth recording, because it is not obvious from the statement of posRes_trans. Mathlib's Rep.res does not compose: for K ≤ H ≤ G the composite Rep.res (K.subgroupOf H).subtype (Rep.res H.subtype M) is not definitionally Rep.res K.subtype M, and the two have different carrier types (↥(K.subgroupOf H) versus ↥K), so that equality cannot even be stated as an equation of Reps. The composite is therefore related to the single restriction only through the map along Subgroup.subgroupOfEquivOfLe hKH built from TauCeti.Subgroup.subtype_comp_subgroupOfEquivOfLe and TauCeti.Rep.isIntertwiningMap_res_res, which is why the statement of posRes_trans carries that middle term.

References

• E. Artin and J. Tate, Class Field Theory, Chapter IV, §6 and Chapter XIV, §4.
• K. S. Brown, Cohomology of Groups, Chapter III, §9 and Chapter VI, §5.

noncomputable def TauCeti.TateCohomology.posRes {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) : tateCohomology M ↑(n + 1) ⟶ tateCohomology (Rep.res H.subtype M) ↑(n + 1)

Restriction to a subgroup in Tate degree n + 1, for n : ℕ. In positive degrees the Tate complex is the complex of inhomogeneous cochains, so this is the ordinary restriction of group cohomology TauCeti.groupCohomology.map along H.subtype, transported through Mathlib's comparison TateCohomology.isoGroupCohomology.

@[simp]

theorem TauCeti.TateCohomology.posRes_comp_isoGroupCohomology_hom {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (posRes M H n) ((TateCohomology.isoGroupCohomology (n + 1)).hom.app (Rep.res H.subtype M)) = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology (n + 1)).hom.app M) (groupCohomology.map H.subtype (CategoryTheory.CategoryStruct.id (Rep.res H.subtype M)) (n + 1))

In positive degrees Tate restriction is the ordinary cohomological restriction along H.subtype, read through Mathlib's comparison TateCohomology.isoGroupCohomology.

@[simp]

theorem TauCeti.TateCohomology.posRes_comp_isoGroupCohomology_hom_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) {Z : ModuleCat R} (h : (groupCohomology.functor R (↥H) (n + 1)).obj (Rep.res H.subtype M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (posRes M H n) (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology (n + 1)).hom.app (Rep.res H.subtype M)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupCohomology (n + 1)).hom.app M) (groupCohomology.map H.subtype (CategoryTheory.CategoryStruct.id (Rep.res H.subtype M)) (n + 1))) h

In positive degrees Tate restriction is the ordinary cohomological restriction along H.subtype, read through Mathlib's comparison TateCohomology.isoGroupCohomology.

theorem TauCeti.TateCohomology.posRes_natural {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) {N : Rep.{u, u, u} R G} (f : M ⟶ N) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor ↑(n + 1)).map f) (posRes N H n) = CategoryTheory.CategoryStruct.comp (posRes M H n) ((tateCohomologyFunctor ↑(n + 1)).map ((Rep.resFunctor H.subtype).map f))

Positive-degree Tate restriction is natural in the coefficient module: restricting along H.subtype after a map of G-representations is restriction along the restricted map, in Tate degree n + 1. The discrete counterpart of TauCeti.ContinuousCohomology.coeffMap_comp_res.

theorem TauCeti.TateCohomology.posRes_natural_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) {N : Rep.{u, u, u} R G} (f : M ⟶ N) (n : ℕ) {Z : ModuleCat R} (h : tateCohomology (Rep.res H.subtype N) ↑(n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor ↑(n + 1)).map f) (CategoryTheory.CategoryStruct.comp (posRes N H n) h) = CategoryTheory.CategoryStruct.comp (posRes M H n) (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor ↑(n + 1)).map (Rep.resMap H.subtype f)) h)

Positive-degree Tate restriction is natural in the coefficient module: restricting along H.subtype after a map of G-representations is restriction along the restricted map, in Tate degree n + 1. The discrete counterpart of TauCeti.ContinuousCohomology.coeffMap_comp_res.

theorem TauCeti.TateCohomology.posRes_trans {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) {K H : Subgroup G} (hKH : K ≤ H) (n : ℕ) : CategoryTheory.CategoryStruct.comp (posRes M H n) (CategoryTheory.CategoryStruct.comp (posRes (Rep.res H.subtype M) (K.subgroupOf H) n) (map ⋯ ↑(n + 1))) = posRes M K n

Tate restriction in positive degrees is transitive along a tower of subgroups K ≤ H ≤ G: restricting from G to H and then from H to K is restriction from G to K, once K.subgroupOf H is identified with K by the Tate map along Subgroup.subgroupOfEquivOfLe hKH. This is the positive-degree counterpart of TauCeti.TateCohomology.negSuccRes_trans.

theorem TauCeti.TateCohomology.posRes_trans_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) {K H : Subgroup G} (hKH : K ≤ H) (n : ℕ) {Z : ModuleCat R} (h : tateCohomology (Rep.res K.subtype M) ↑(n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (posRes M H n) (CategoryTheory.CategoryStruct.comp (posRes (Rep.res H.subtype M) (K.subgroupOf H) n) (CategoryTheory.CategoryStruct.comp (map ⋯ ↑(n + 1)) h)) = CategoryTheory.CategoryStruct.comp (posRes M K n) h

Tate restriction in positive degrees is transitive along a tower of subgroups K ≤ H ≤ G: restricting from G to H and then from H to K is restriction from G to K, once K.subgroupOf H is identified with K by the Tate map along Subgroup.subgroupOfEquivOfLe hKH. This is the positive-degree counterpart of TauCeti.TateCohomology.negSuccRes_trans.