Dimension shifting in Tate cohomology

For a finite group G, the connecting maps of the canonical sequences

0 ⟶ A ⟶ Coind_⊥^G A ⟶ dimensionShiftUp A ⟶ 0 and 0 ⟶ dimensionShiftDown A ⟶ Ind_⊥^G A ⟶ A ⟶ 0

are isomorphisms in every integer Tate degree. The same is true after restriction to any finite subgroup of G, even when G itself is infinite. These subgroupwise shifts allow a vanishing condition in consecutive degrees to be moved to other degrees simultaneously on all subgroups, as required in Tate's cohomological triviality and cup-product criteria.

The two sequences stay short exact after tensoring on the left with any representation M, and the middle terms M ⊗ Coind_⊥^G A and M ⊗ Ind_⊥^G A still have vanishing Tate cohomology, so their connecting maps are isomorphisms as well (tensorDimensionShiftUpIso, tensorDimensionShiftDownIso). These tensored shifts take the target degree as a parameter, so that a construction proceeding by recursion on the degree, such as the cup product in all bidegrees, needs no transport along equalities of degrees between its recursive steps; the cup product transports its result once, at the end, to the requested target degree.

The composites of two consecutive upward shifts, on the group (dimensionShiftUpTwoIso, from degree 0 to degree 2) and on a finite subgroup (dimensionShiftUpTwoResIso), present a degree-two class as the double shift of a degree-zero class.

Each isomorphism below has Mathlib's connecting homomorphism TateCohomology.δ as its forward map. Thus its naturality in a morphism of the short exact sequences is the existing theorem TateCohomology.δ_naturality; no choices of abstract isomorphisms enter the construction. The naturality statements here apply both to a shift and to its tensor with a fixed representation, so they transport cup products along coefficient maps.

The unrestricted constructions adapt δUpIsoTate and δDownIsoTate from ClassFieldTheory/Cohomology/Functors/UpDown.lean in kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509. The restricted constructions use the vanishing of restricted induced and coinduced representations proved in TateCohomology.Coinduced. All four reuse Mathlib's CategoryTheory.ShortComplex.ShortExact.δIso.

References

• J. S. Milne, Class Field Theory, Chapter II, §3 (dimension shifting and Theorem 3.10).

noncomputable def TauCeti.TateCohomology.dimensionShiftUpIso {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] (n : ℤ) : tateCohomology A.dimensionShiftUp n ≅ tateCohomology A (n + 1)

The upward dimension-shifting sequence identifies Tate cohomology of dimensionShiftUp A in degree n with Tate cohomology of A in degree n + 1.

Equations

• TauCeti.TateCohomology.dimensionShiftUpIso A n = ⋯.δIso n (n + 1) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.TateCohomology.dimensionShiftUpIso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] (n : ℤ) : (dimensionShiftUpIso A n).hom = TateCohomology.δ ⋯ n

The upward dimension shift is the connecting map of the coinduced short exact sequence.

noncomputable def TauCeti.TateCohomology.dimensionShiftDownIso {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] (n : ℤ) : tateCohomology A n ≅ tateCohomology A.dimensionShiftDown (n + 1)

The downward dimension-shifting sequence identifies Tate cohomology of A in degree n with Tate cohomology of dimensionShiftDown A in degree n + 1.

Equations

• TauCeti.TateCohomology.dimensionShiftDownIso A n = ⋯.δIso n (n + 1) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.TateCohomology.dimensionShiftDownIso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] (n : ℤ) : (dimensionShiftDownIso A n).hom = TateCohomology.δ ⋯ n

The downward dimension shift is the connecting map of the induced short exact sequence.

noncomputable def TauCeti.TateCohomology.dimensionShiftUpTwoIso {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] : tateCohomology A.dimensionShiftUp.dimensionShiftUp 0 ≅ tateCohomology A 2

Two upward dimension shifts identify degree-zero Tate cohomology of the twice-shifted representation with degree-two Tate cohomology of the representation itself.

Equations

• TauCeti.TateCohomology.dimensionShiftUpTwoIso A = TauCeti.TateCohomology.dimensionShiftUpIso A.dimensionShiftUp 0 ≪≫ TauCeti.TateCohomology.dimensionShiftUpIso A 1

@[simp]

theorem TauCeti.TateCohomology.dimensionShiftUpTwoIso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] : (dimensionShiftUpTwoIso A).hom = CategoryTheory.CategoryStruct.comp (dimensionShiftUpIso A.dimensionShiftUp 0).hom (dimensionShiftUpIso A 1).hom

The double shift is the composite of the two upward dimension shifts.

theorem TauCeti.TateCohomology.dimensionShiftUpIso_hom_naturality {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (n : ℤ) {B : Rep.{u, u, u} k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor n).map (Rep.dimensionShiftUpMap f)) (dimensionShiftUpIso B n).hom = CategoryTheory.CategoryStruct.comp (dimensionShiftUpIso A n).hom ((tateCohomologyFunctor (n + 1)).map f)

Upward dimension shifting commutes with a morphism of coefficient representations.

theorem TauCeti.TateCohomology.dimensionShiftUpIso_hom_naturality_assoc {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (n : ℤ) {B : Rep.{u, u, u} k G} (f : A ⟶ B) {Z : ModuleCat k} (h : tateCohomology B (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor n).map (Rep.dimensionShiftUpMap f)) (CategoryTheory.CategoryStruct.comp (dimensionShiftUpIso B n).hom h) = CategoryTheory.CategoryStruct.comp (dimensionShiftUpIso A n).hom (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (n + 1)).map f) h)

Upward dimension shifting commutes with a morphism of coefficient representations.

theorem TauCeti.TateCohomology.dimensionShiftUpIso_inv_naturality {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (n : ℤ) {B : Rep.{u, u, u} k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (n + 1)).map f) (dimensionShiftUpIso B n).inv = CategoryTheory.CategoryStruct.comp (dimensionShiftUpIso A n).inv ((tateCohomologyFunctor n).map (Rep.dimensionShiftUpMap f))

The inverse upward shift commutes with a coefficient morphism.

theorem TauCeti.TateCohomology.dimensionShiftUpIso_inv_naturality_assoc {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (n : ℤ) {B : Rep.{u, u, u} k G} (f : A ⟶ B) {Z : ModuleCat k} (h : tateCohomology B.dimensionShiftUp n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (n + 1)).map f) (CategoryTheory.CategoryStruct.comp (dimensionShiftUpIso B n).inv h) = CategoryTheory.CategoryStruct.comp (dimensionShiftUpIso A n).inv (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor n).map (Rep.dimensionShiftUpMap f)) h)

The inverse upward shift commutes with a coefficient morphism.

theorem TauCeti.TateCohomology.dimensionShiftDownIso_hom_naturality {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (n : ℤ) {B : Rep.{u, u, u} k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor n).map f) (dimensionShiftDownIso B n).hom = CategoryTheory.CategoryStruct.comp (dimensionShiftDownIso A n).hom ((tateCohomologyFunctor (n + 1)).map (Rep.dimensionShiftDownMap f))

Downward dimension shifting commutes with a morphism of coefficient representations.

theorem TauCeti.TateCohomology.dimensionShiftDownIso_hom_naturality_assoc {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (n : ℤ) {B : Rep.{u, u, u} k G} (f : A ⟶ B) {Z : ModuleCat k} (h : tateCohomology B.dimensionShiftDown (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor n).map f) (CategoryTheory.CategoryStruct.comp (dimensionShiftDownIso B n).hom h) = CategoryTheory.CategoryStruct.comp (dimensionShiftDownIso A n).hom (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (n + 1)).map (Rep.dimensionShiftDownMap f)) h)

Downward dimension shifting commutes with a morphism of coefficient representations.

theorem TauCeti.TateCohomology.dimensionShiftDownIso_inv_naturality {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (n : ℤ) {B : Rep.{u, u, u} k G} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (n + 1)).map (Rep.dimensionShiftDownMap f)) (dimensionShiftDownIso B n).inv = CategoryTheory.CategoryStruct.comp (dimensionShiftDownIso A n).inv ((tateCohomologyFunctor n).map f)

The inverse downward shift commutes with a coefficient morphism.

theorem TauCeti.TateCohomology.dimensionShiftDownIso_inv_naturality_assoc {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (n : ℤ) {B : Rep.{u, u, u} k G} (f : A ⟶ B) {Z : ModuleCat k} (h : tateCohomology B n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (n + 1)).map (Rep.dimensionShiftDownMap f)) (CategoryTheory.CategoryStruct.comp (dimensionShiftDownIso B n).inv h) = CategoryTheory.CategoryStruct.comp (dimensionShiftDownIso A n).inv (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor n).map f) h)

The inverse downward shift commutes with a coefficient morphism.

@[simp]

theorem TauCeti.TateCohomology.isZero_dimensionShiftUp_iff {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology A.dimensionShiftUp n) ↔ CategoryTheory.Limits.IsZero (tateCohomology A (n + 1))

Vanishing in degree n of an upward shift is vanishing in degree n + 1 of the original module.

@[simp]

theorem TauCeti.TateCohomology.isZero_dimensionShiftDown_iff {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology A.dimensionShiftDown (n + 1)) ↔ CategoryTheory.Limits.IsZero (tateCohomology A n)

Vanishing in degree n + 1 of a downward shift is vanishing in degree n of the original module.

noncomputable def TauCeti.TateCohomology.tensorDimensionShiftUpIso {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] (M : Rep.{u, u, u} k G) (i j : ℤ) (hij : i + 1 = j) : tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M A.dimensionShiftUp) i ≅ tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M A) j

Tensoring the upward dimension-shifting sequence of A on the left with M identifies Tate cohomology of M ⊗ dimensionShiftUp A in degree i with Tate cohomology of M ⊗ A in degree j = i + 1.

Equations

• TauCeti.TateCohomology.tensorDimensionShiftUpIso A M i j hij = ⋯.δIso i j hij ⋯ ⋯

@[simp]

theorem TauCeti.TateCohomology.tensorDimensionShiftUpIso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] (M : Rep.{u, u, u} k G) (i j : ℤ) (hij : i + 1 = j) : (tensorDimensionShiftUpIso A M i j hij).hom = ⋯.δ i j hij

The tensored upward dimension shift is the connecting map of the tensored coinduced short exact sequence.

noncomputable def TauCeti.TateCohomology.tensorDimensionShiftDownIso {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] (M : Rep.{u, u, u} k G) (i j : ℤ) (hij : i + 1 = j) : tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M A) i ≅ tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M A.dimensionShiftDown) j

Tensoring the downward dimension-shifting sequence of A on the left with M identifies Tate cohomology of M ⊗ A in degree i with Tate cohomology of M ⊗ dimensionShiftDown A in degree j = i + 1.

Equations

• TauCeti.TateCohomology.tensorDimensionShiftDownIso A M i j hij = ⋯.δIso i j hij ⋯ ⋯

@[simp]

theorem TauCeti.TateCohomology.tensorDimensionShiftDownIso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] (M : Rep.{u, u, u} k G) (i j : ℤ) (hij : i + 1 = j) : (tensorDimensionShiftDownIso A M i j hij).hom = ⋯.δ i j hij

The tensored downward dimension shift is the connecting map of the tensored induced short exact sequence.

theorem TauCeti.TateCohomology.tensorDimensionShiftUpIso_hom_naturality_right {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (M : Rep.{u, u, u} k G) {B : Rep.{u, u, u} k G} (f : A ⟶ B) (i j : ℤ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (Rep.dimensionShiftUpMap f))) (tensorDimensionShiftUpIso B M i j hij).hom = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso A M i j hij).hom ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f))

The tensored upward dimension shift is natural in its shifting representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftUpIso_hom_naturality_right_assoc {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (M : Rep.{u, u, u} k G) {B : Rep.{u, u, u} k G} (f : A ⟶ B) (i j : ℤ) (hij : i + 1 = j) {Z : ModuleCat k} (h : tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M B) j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (Rep.dimensionShiftUpMap f))) (CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso B M i j hij).hom h) = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso A M i j hij).hom (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f)) h)

The tensored upward dimension shift is natural in its shifting representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftUpIso_inv_naturality_right {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (M : Rep.{u, u, u} k G) {B : Rep.{u, u, u} k G} (f : A ⟶ B) (i j : ℤ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f)) (tensorDimensionShiftUpIso B M i j hij).inv = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso A M i j hij).inv ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (Rep.dimensionShiftUpMap f)))

The inverse tensored upward shift is natural in its shifting representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftUpIso_inv_naturality_right_assoc {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (M : Rep.{u, u, u} k G) {B : Rep.{u, u, u} k G} (f : A ⟶ B) (i j : ℤ) (hij : i + 1 = j) {Z : ModuleCat k} (h : tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M B.dimensionShiftUp) i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f)) (CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso B M i j hij).inv h) = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso A M i j hij).inv (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (Rep.dimensionShiftUpMap f))) h)

The inverse tensored upward shift is natural in its shifting representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftDownIso_hom_naturality_right {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (M : Rep.{u, u, u} k G) {B : Rep.{u, u, u} k G} (f : A ⟶ B) (i j : ℤ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f)) (tensorDimensionShiftDownIso B M i j hij).hom = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso A M i j hij).hom ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (Rep.dimensionShiftDownMap f)))

The tensored downward dimension shift is natural in its shifting representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftDownIso_hom_naturality_right_assoc {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (M : Rep.{u, u, u} k G) {B : Rep.{u, u, u} k G} (f : A ⟶ B) (i j : ℤ) (hij : i + 1 = j) {Z : ModuleCat k} (h : tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M B.dimensionShiftDown) j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f)) (CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso B M i j hij).hom h) = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso A M i j hij).hom (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (Rep.dimensionShiftDownMap f))) h)

The tensored downward dimension shift is natural in its shifting representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftDownIso_inv_naturality_right {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (M : Rep.{u, u, u} k G) {B : Rep.{u, u, u} k G} (f : A ⟶ B) (i j : ℤ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (Rep.dimensionShiftDownMap f))) (tensorDimensionShiftDownIso B M i j hij).inv = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso A M i j hij).inv ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f))

The inverse tensored downward shift is natural in its shifting representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftDownIso_inv_naturality_right_assoc {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} [Fintype G] (M : Rep.{u, u, u} k G) {B : Rep.{u, u, u} k G} (f : A ⟶ B) (i j : ℤ) (hij : i + 1 = j) {Z : ModuleCat k} (h : tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M B) i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (Rep.dimensionShiftDownMap f))) (CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso B M i j hij).inv h) = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso A M i j hij).inv (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f)) h)

The inverse tensored downward shift is natural in its shifting representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftUpIso_hom_naturality_left {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] {M M' : Rep.{u, u, u} k G} (f : M ⟶ M') (i j : ℤ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A.dimensionShiftUp)) (tensorDimensionShiftUpIso A M' i j hij).hom = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso A M i j hij).hom ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A))

The tensored upward dimension shift is natural in the tensoring representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftUpIso_hom_naturality_left_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] {M M' : Rep.{u, u, u} k G} (f : M ⟶ M') (i j : ℤ) (hij : i + 1 = j) {Z : ModuleCat k} (h : tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M' A) j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A.dimensionShiftUp)) (CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso A M' i j hij).hom h) = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso A M i j hij).hom (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A)) h)

The tensored upward dimension shift is natural in the tensoring representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftUpIso_inv_naturality_left {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] {M M' : Rep.{u, u, u} k G} (f : M ⟶ M') (i j : ℤ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A)) (tensorDimensionShiftUpIso A M' i j hij).inv = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso A M i j hij).inv ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A.dimensionShiftUp))

The inverse tensored upward shift is natural in the tensoring representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftUpIso_inv_naturality_left_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] {M M' : Rep.{u, u, u} k G} (f : M ⟶ M') (i j : ℤ) (hij : i + 1 = j) {Z : ModuleCat k} (h : tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M' A.dimensionShiftUp) i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A)) (CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso A M' i j hij).inv h) = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftUpIso A M i j hij).inv (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A.dimensionShiftUp)) h)

The inverse tensored upward shift is natural in the tensoring representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftDownIso_hom_naturality_left {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] {M M' : Rep.{u, u, u} k G} (f : M ⟶ M') (i j : ℤ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A)) (tensorDimensionShiftDownIso A M' i j hij).hom = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso A M i j hij).hom ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A.dimensionShiftDown))

The tensored downward dimension shift is natural in the tensoring representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftDownIso_hom_naturality_left_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] {M M' : Rep.{u, u, u} k G} (f : M ⟶ M') (i j : ℤ) (hij : i + 1 = j) {Z : ModuleCat k} (h : tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M' A.dimensionShiftDown) j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A)) (CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso A M' i j hij).hom h) = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso A M i j hij).hom (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A.dimensionShiftDown)) h)

The tensored downward dimension shift is natural in the tensoring representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftDownIso_inv_naturality_left {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] {M M' : Rep.{u, u, u} k G} (f : M ⟶ M') (i j : ℤ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A.dimensionShiftDown)) (tensorDimensionShiftDownIso A M' i j hij).inv = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso A M i j hij).inv ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A))

The inverse of the tensored downward dimension shift is natural in the tensoring representation.

theorem TauCeti.TateCohomology.tensorDimensionShiftDownIso_inv_naturality_left_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) [Fintype G] {M M' : Rep.{u, u, u} k G} (f : M ⟶ M') (i j : ℤ) (hij : i + 1 = j) {Z : ModuleCat k} (h : tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M' A) i ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor j).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A.dimensionShiftDown)) (CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso A M' i j hij).inv h) = CategoryTheory.CategoryStruct.comp (tensorDimensionShiftDownIso A M i j hij).inv (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor i).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f A)) h)

The inverse of the tensored downward dimension shift is natural in the tensoring representation.

noncomputable def TauCeti.TateCohomology.dimensionShiftUpResIso {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : tateCohomology (Rep.res S.subtype A.dimensionShiftUp) n ≅ tateCohomology (Rep.res S.subtype A) (n + 1)

Upward dimension shifting after restriction to a finite subgroup. The shift is constructed over G, so the same coefficient representation works for every finite subgroup.

Equations

• TauCeti.TateCohomology.dimensionShiftUpResIso A S n = ⋯.δIso n (n + 1) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.TateCohomology.dimensionShiftUpResIso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : (dimensionShiftUpResIso A S n).hom = TateCohomology.δ ⋯ n

Restricted upward dimension shifting is the connecting map of the restricted sequence.

noncomputable def TauCeti.TateCohomology.dimensionShiftDownResIso {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : tateCohomology (Rep.res S.subtype A) n ≅ tateCohomology (Rep.res S.subtype A.dimensionShiftDown) (n + 1)

Downward dimension shifting after restriction to a finite subgroup. The shift is constructed over G, so the same coefficient representation works for every finite subgroup.

Equations

• TauCeti.TateCohomology.dimensionShiftDownResIso A S n = ⋯.δIso n (n + 1) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.TateCohomology.dimensionShiftDownResIso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : (dimensionShiftDownResIso A S n).hom = TateCohomology.δ ⋯ n

Restricted downward dimension shifting is the connecting map of the restricted sequence.

noncomputable def TauCeti.TateCohomology.dimensionShiftUpTwoResIso {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : tateCohomology (Rep.res S.subtype A.dimensionShiftUp.dimensionShiftUp) n ≅ tateCohomology (Rep.res S.subtype A) (n + 1 + 1)

Two upward dimension shifts after restriction to a finite subgroup identify Tate cohomology of the twice-shifted representation in degree n with Tate cohomology of the representation itself in degree n + 1 + 1.

Equations

• TauCeti.TateCohomology.dimensionShiftUpTwoResIso A S n = TauCeti.TateCohomology.dimensionShiftUpResIso A.dimensionShiftUp S n ≪≫ TauCeti.TateCohomology.dimensionShiftUpResIso A S (n + 1)

@[simp]

theorem TauCeti.TateCohomology.dimensionShiftUpTwoResIso_hom {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : (dimensionShiftUpTwoResIso A S n).hom = CategoryTheory.CategoryStruct.comp (dimensionShiftUpResIso A.dimensionShiftUp S n).hom (dimensionShiftUpResIso A S (n + 1)).hom

The restricted double shift is the composite of the two restricted upward dimension shifts.

@[simp]

theorem TauCeti.TateCohomology.isZero_res_dimensionShiftUp_iff {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A.dimensionShiftUp) n) ↔ CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A) (n + 1))

Vanishing in degree n of an upward shift is vanishing in degree n + 1 of the original module, also on a finite subgroup.

@[simp]

theorem TauCeti.TateCohomology.isZero_res_dimensionShiftDown_iff {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A.dimensionShiftDown) (n + 1)) ↔ CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype A) n)

Vanishing in degree n + 1 of a downward shift is vanishing in degree n of the original module, also on a finite subgroup.