Restriction across the boundary of the Tate complex #
Restriction commutes with the connecting map from degree -1 to degree zero. These degrees
straddle the norm differential joining chains to cochains: restriction acts by relative transfer
on the norm kernel and by inclusion on the invariants. Their compatibility follows from
N_H ∘ relTransfer = N_G and the norm description of the connecting map.
This is the boundary case needed to dimension-shift the restriction law for cups with a negative-degree factor.
References #
- K. S. Brown, Cohomology of Groups, Chapter VI, §5.
- E. Artin and J. Tate, Class Field Theory, Chapter IV, §6.
@[simp]
theorem
TauCeti.TateCohomology.δ_comp_res_neg_one
{R G : Type u}
[CommRing R]
[Group G]
[Fintype G]
{S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)}
(hS : S.ShortExact)
(H : Subgroup G)
:
CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS (-1)) (H0Res S.X₁ H) = CategoryTheory.CategoryStruct.comp (HNegOneRes S.X₃ H) (TateCohomology.δ ⋯ (-1))
Tate restriction commutes with the connecting map from degree -1 to degree zero.
@[simp]
theorem
TauCeti.TateCohomology.δ_comp_res_neg_one_assoc
{R G : Type u}
[CommRing R]
[Group G]
[Fintype G]
{S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)}
(hS : S.ShortExact)
(H : Subgroup G)
{Z : ModuleCat R}
(h : tateCohomology (Rep.res H.subtype S.X₁) 0 ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (TateCohomology.δ hS (-1)) (CategoryTheory.CategoryStruct.comp (H0Res S.X₁ H) h) = CategoryTheory.CategoryStruct.comp (HNegOneRes S.X₃ H)
(CategoryTheory.CategoryStruct.comp (TateCohomology.δ ⋯ (-1)) h)
Tate restriction commutes with the connecting map from degree -1 to degree zero.