Restriction in negative Tate degrees and maps in the two low degrees

Let G be a finite group, H ≤ G a subgroup and M a G-representation. In every Tate degree there are a restriction map tateCohomology M n ⟶ tateCohomology (Rep.res H.subtype M) n and a corestriction map back, and the composite of the two is multiplication by the index [G : H]. In the degrees where the Tate complex is the complex of inhomogeneous cochains — that is, in degrees ≥ 1 — restriction is the ordinary restriction of group cohomology, and in the degrees where it is the complex of inhomogeneous chains — degrees ≤ -2 — corestriction is the ordinary change-of-group map of group homology, both of which Mathlib already provides. Degrees 0 and -1 are the two degrees where the Tate complex is neither, being glued there by the norm map: degree 0 is Mᴳ / N_G M and degree -1 is ker N_G / I_G M.

This file supplies restriction in degrees at most -2 by transporting the homological transfer through Mathlib's comparison with group homology. It also supplies all four maps in degrees 0 and -1, using the identifications of TauCeti.RepresentationTheory.Homological.TateCohomology.LowDegree. Restriction in degree 0 and corestriction in degree -1 are induced by inclusions of representatives, Mᴳ ⊆ Mᴴ and ker N_G ⊇ ker N_H. The other two are induced by the relative norm and the relative transfer of H in G of TauCeti.RepresentationTheory.RelativeNorm: corestriction in degree 0 is the relative norm N_{G/H} : Mᴴ → Mᴳ, and restriction in degree -1 is the relative transfer, which carries ker N_G into ker N_H and I_G M into I_H M.

In both degrees the composite of restriction and corestriction is multiplication by [G : H], because the relative norm is [G : H] • · on Mᴳ and the relative transfer is [G : H] • · modulo I_G M. In degrees at most -2 the same identity is corestriction after transfer in group homology, TauCeti.groupHomology.transfer_comp_map_subtype_id, with corestriction taken from TauCeti.RepresentationTheory.Homological.TateCohomology.NegativeCorestriction.

With trivial integral coefficients, the restriction of Rep.trivial ℤ G ℤ to H is the trivial representation of H, and the identity of ℤ is a compatible pair between the two; the resulting comparison trivialResIso reads the order of degree-zero and the vanishing of degree-one Tate cohomology of Rep.trivial ℤ H ℤ on the restricted representation.

Main definitions

• TauCeti.TateCohomology.H0Res, TauCeti.TateCohomology.H0Cor: restriction and corestriction in degree 0.
• TauCeti.TateCohomology.HNegOneRes, TauCeti.TateCohomology.HNegOneCor: restriction and corestriction in degree -1.
• TauCeti.TateCohomology.negSuccRes: restriction in degree -(n+1) for n > 0.
• TauCeti.TateCohomology.HNegTwoRes: the degree--2 specialization.
• TauCeti.TateCohomology.trivialResIso: Tate cohomology of the trivial integral representation of a subgroup, as Tate cohomology of the restricted trivial representation.
• TauCeti.TateCohomology.resTrivialTateHZeroOne: the class of 1 in degree-zero Tate cohomology of the restricted trivial integral representation; it generates, and is killed by the order of the subgroup.

Main results

• TauCeti.TateCohomology.negSuccRes_comp_negSuccIso_hom: negative restriction agrees with homological transfer through TauCeti.TateCohomology.negSuccIso.
• TauCeti.TateCohomology.H0π_comp_H0Res, TauCeti.TateCohomology.H0π_comp_H0Cor, TauCeti.TateCohomology.HNegOneπ_comp_HNegOneRes, TauCeti.TateCohomology.HNegOneπ_comp_HNegOneCor: the effect of each map on the class of a representative.
• TauCeti.TateCohomology.HNegTwoRes_def: restriction in degree -2 is the transfer in first group homology, transported through Mathlib's comparison with group homology.
• TauCeti.TateCohomology.HNegTwoRes_comp_isoGroupHomology_hom: this comparison commutes with restriction and homological transfer.
• TauCeti.TateCohomology.H0Res_comp_H0Cor, TauCeti.TateCohomology.HNegOneRes_comp_HNegOneCor and TauCeti.TateCohomology.negSuccRes_comp_negSuccCor: corestriction after restriction is multiplication by the index.
• TauCeti.TateCohomology.natCard_tateCohomology_zero_res_trivial_int_eq_card, TauCeti.TateCohomology.isZero_tateCohomology_one_res_trivial_int: degree-zero Tate cohomology of the restricted trivial integral representation has the order of the subgroup, and its degree-one Tate cohomology vanishes.

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.
• J. S. Milne, Class Field Theory, v4.03, Chapter II, §1.

noncomputable def TauCeti.TateCohomology.negSuccRes {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) [NeZero n] : tateCohomology M (Int.negSucc n) ⟶ tateCohomology (Rep.res H.subtype M) (Int.negSucc n)

Restriction to a subgroup in Tate degree -(n+1), for n > 0. Through Mathlib's negative-degree comparison, this is the transfer in nth group homology.

@[simp]

theorem TauCeti.TateCohomology.negSuccRes_comp_negSuccIso_hom {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) [NeZero n] : CategoryTheory.CategoryStruct.comp (negSuccRes M H n) (negSuccIso (Rep.res H.subtype M) n).hom = CategoryTheory.CategoryStruct.comp (negSuccIso M n).hom (groupHomology.transfer M H n)

Negative-degree Tate restriction is the homological transfer through TauCeti.TateCohomology.negSuccIso.

@[simp]

theorem TauCeti.TateCohomology.negSuccRes_comp_negSuccIso_hom_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) [NeZero n] {Z : ModuleCat R} (h : groupHomology (Rep.res H.subtype M) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (negSuccRes M H n) (CategoryTheory.CategoryStruct.comp (negSuccIso (Rep.res H.subtype M) n).hom h) = CategoryTheory.CategoryStruct.comp (negSuccIso M n).hom (CategoryTheory.CategoryStruct.comp (groupHomology.transfer M H n) h)

Negative-degree Tate restriction is the homological transfer through TauCeti.TateCohomology.negSuccIso.

noncomputable def TauCeti.TateCohomology.HNegTwoRes {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : tateCohomology M (-2) ⟶ tateCohomology (Rep.res H.subtype M) (-2)

Restriction to a subgroup in degree -2 Tate cohomology. Under the comparison with first group homology, this is the homological transfer.

theorem TauCeti.TateCohomology.HNegTwoRes_eq_negSuccRes {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : HNegTwoRes M H = negSuccRes M H 1

Degree--2 restriction is the degree-one instance of negative restriction.

theorem TauCeti.TateCohomology.HNegTwoRes_def {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : HNegTwoRes M H = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 HNegTwoRes_def._proof_1).hom.app M) (CategoryTheory.CategoryStruct.comp (groupHomology.transfer M H 1) ((TateCohomology.isoGroupHomology (-2) 1 HNegTwoRes_def._proof_1).inv.app (Rep.res H.subtype M)))

Restriction in Tate degree -2 is the transfer in first group homology, transported through Mathlib's negative-degree comparison TateCohomology.isoGroupHomology.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoRes_comp_isoGroupHomology_hom {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : CategoryTheory.CategoryStruct.comp (HNegTwoRes M H) ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.res H.subtype M)) = CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app M) (groupHomology.transfer M H 1)

Restriction in degree -2 commutes with the comparison to first group homology.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoRes_comp_isoGroupHomology_hom_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) {Z : ModuleCat R} (h : (groupHomology.functor R (↥H) 1).obj (Rep.res H.subtype M) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HNegTwoRes M H) (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.res H.subtype M)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app M) (groupHomology.transfer M H 1)) h

Restriction in degree -2 commutes with the comparison to first group homology.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoRes_comp_isoGroupHomology_hom_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (x : ↑(tateCohomology M (-2))) : (CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app (Rep.res H.subtype M))) ((CategoryTheory.ConcreteCategory.hom (HNegTwoRes M H)) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp ((TateCohomology.isoGroupHomology (-2) 1 ⋯).hom.app M) (groupHomology.transfer M H 1))) x

Restriction in degree -2 commutes with the comparison to first group homology.

theorem TauCeti.TateCohomology.negSuccRes_comp_negSuccCor {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) [NeZero n] : CategoryTheory.CategoryStruct.comp (negSuccRes M H n) (negSuccCor M H.subtype n) = H.index • CategoryTheory.CategoryStruct.id (tateCohomology M (Int.negSucc n))

Restriction followed by corestriction is multiplication by the index, in every Tate degree -(n+1) with n > 0.

theorem TauCeti.TateCohomology.negSuccRes_comp_negSuccCor_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) [NeZero n] {Z : ModuleCat R} (h : tateCohomology M (Int.negSucc n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (negSuccRes M H n) (CategoryTheory.CategoryStruct.comp (negSuccCor M H.subtype n) h) = CategoryTheory.CategoryStruct.comp (H.index • CategoryTheory.CategoryStruct.id (tateCohomology M (Int.negSucc n))) h

Restriction followed by corestriction is multiplication by the index, in every Tate degree -(n+1) with n > 0.

theorem TauCeti.TateCohomology.negSuccRes_comp_negSuccCor_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (n : ℕ) [NeZero n] (x : ↑(tateCohomology M (Int.negSucc n))) : (CategoryTheory.ConcreteCategory.hom (negSuccCor M H.subtype n)) ((CategoryTheory.ConcreteCategory.hom (negSuccRes M H n)) x) = H.index • x

Restriction followed by corestriction is multiplication by the index, in every Tate degree -(n+1) with n > 0.

noncomputable def TauCeti.TateCohomology.H0Res {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : tateCohomology M 0 ⟶ tateCohomology (Rep.res H.subtype M) 0

Restriction to a subgroup in degree zero Tate cohomology, induced by the inclusion of the invariants Mᴳ ⊆ Mᴴ.

noncomputable def TauCeti.TateCohomology.H0Cor {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : tateCohomology (Rep.res H.subtype M) 0 ⟶ tateCohomology M 0

Corestriction from a subgroup in degree zero Tate cohomology, induced by the relative norm Mᴴ → Mᴳ.

@[simp]

theorem TauCeti.TateCohomology.H0π_comp_H0Res {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : CategoryTheory.CategoryStruct.comp (H0π M) (H0Res M H) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Submodule.inclusion ⋯)) (H0π (Rep.res H.subtype M))

Restriction in degree zero sends the class of a G-invariant element to the class of the same element, viewed as an H-invariant element.

@[simp]

theorem TauCeti.TateCohomology.H0π_comp_H0Res_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) {Z : ModuleCat R} (h : tateCohomology (Rep.res H.subtype M) 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (H0π M) (CategoryTheory.CategoryStruct.comp (H0Res M H) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Submodule.inclusion ⋯)) (CategoryTheory.CategoryStruct.comp (H0π (Rep.res H.subtype M)) h)

Restriction in degree zero sends the class of a G-invariant element to the class of the same element, viewed as an H-invariant element.

@[simp]

theorem TauCeti.TateCohomology.H0π_comp_H0Res_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (x : ↥M.ρ.invariants) : (CategoryTheory.ConcreteCategory.hom (H0Res M H)) ((CategoryTheory.ConcreteCategory.hom (H0π M)) x) = (CategoryTheory.ConcreteCategory.hom (H0π (Rep.res H.subtype M))) ((Submodule.inclusion ⋯) x)

Restriction in degree zero sends the class of a G-invariant element to the class of the same element, viewed as an H-invariant element.

@[simp]

theorem TauCeti.TateCohomology.H0π_comp_H0Cor {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : CategoryTheory.CategoryStruct.comp (H0π (Rep.res H.subtype M)) (H0Cor M H) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (M.ρ.relNormInvariants H)) (H0π M)

Corestriction in degree zero sends the class of an H-invariant element to the class of its relative norm.

@[simp]

theorem TauCeti.TateCohomology.H0π_comp_H0Cor_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) {Z : ModuleCat R} (h : tateCohomology M 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (H0π (Rep.res H.subtype M)) (CategoryTheory.CategoryStruct.comp (H0Cor M H) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (M.ρ.relNormInvariants H)) (CategoryTheory.CategoryStruct.comp (H0π M) h)

Corestriction in degree zero sends the class of an H-invariant element to the class of its relative norm.

@[simp]

theorem TauCeti.TateCohomology.H0π_comp_H0Cor_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (x : ↥(Representation.invariants (MonoidHom.comp M.ρ H.subtype))) : (CategoryTheory.ConcreteCategory.hom (H0Cor M H)) ((CategoryTheory.ConcreteCategory.hom (H0π (Rep.res H.subtype M))) x) = (CategoryTheory.ConcreteCategory.hom (H0π M)) ((M.ρ.relNormInvariants H) x)

Corestriction in degree zero sends the class of an H-invariant element to the class of its relative norm.

theorem TauCeti.TateCohomology.H0Cor_comp_H0Res_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (x : ↑(tateCohomology M 0)) : (CategoryTheory.ConcreteCategory.hom (H0Cor M H)) ((CategoryTheory.ConcreteCategory.hom (H0Res M H)) x) = H.index • x

Corestriction of the restriction of a degree-zero class is the index multiple of it.

theorem TauCeti.TateCohomology.H0Res_comp_H0Cor {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : CategoryTheory.CategoryStruct.comp (H0Res M H) (H0Cor M H) = H.index • CategoryTheory.CategoryStruct.id (tateCohomology M 0)

Restriction followed by corestriction is multiplication by the index, in degree zero.

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

Restriction to a subgroup in degree -1 Tate cohomology, induced by the relative transfer.

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

Corestriction from a subgroup in degree -1 Tate cohomology, induced by the inclusion of the kernel of the norm of H in the kernel of the norm of G.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_comp_HNegOneRes {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : CategoryTheory.CategoryStruct.comp (HNegOneπ M) (HNegOneRes M H) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (M.ρ.relTransferKerNorm H)) (HNegOneπ (Rep.res H.subtype M))

Restriction in degree -1 sends the class of a norm-zero element to the class of its relative transfer.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_comp_HNegOneRes_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) {Z : ModuleCat R} (h : tateCohomology (Rep.res H.subtype M) (-1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HNegOneπ M) (CategoryTheory.CategoryStruct.comp (HNegOneRes M H) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (M.ρ.relTransferKerNorm H)) (CategoryTheory.CategoryStruct.comp (HNegOneπ (Rep.res H.subtype M)) h)

Restriction in degree -1 sends the class of a norm-zero element to the class of its relative transfer.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_comp_HNegOneRes_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (x : ↥(LinearMap.ker M.ρ.norm)) : (CategoryTheory.ConcreteCategory.hom (HNegOneRes M H)) ((CategoryTheory.ConcreteCategory.hom (HNegOneπ M)) x) = (CategoryTheory.ConcreteCategory.hom (HNegOneπ (Rep.res H.subtype M))) ((M.ρ.relTransferKerNorm H) x)

Restriction in degree -1 sends the class of a norm-zero element to the class of its relative transfer.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_comp_HNegOneCor {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : CategoryTheory.CategoryStruct.comp (HNegOneπ (Rep.res H.subtype M)) (HNegOneCor M H) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Submodule.inclusion ⋯)) (HNegOneπ M)

Corestriction in degree -1 sends the class of a norm-zero element to the class of the same element.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_comp_HNegOneCor_assoc {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) {Z : ModuleCat R} (h : tateCohomology M (-1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HNegOneπ (Rep.res H.subtype M)) (CategoryTheory.CategoryStruct.comp (HNegOneCor M H) h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Submodule.inclusion ⋯)) (CategoryTheory.CategoryStruct.comp (HNegOneπ M) h)

Corestriction in degree -1 sends the class of a norm-zero element to the class of the same element.

@[simp]

theorem TauCeti.TateCohomology.HNegOneπ_comp_HNegOneCor_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (x : ↥(LinearMap.ker (Representation.norm (MonoidHom.comp M.ρ H.subtype)))) : (CategoryTheory.ConcreteCategory.hom (HNegOneCor M H)) ((CategoryTheory.ConcreteCategory.hom (HNegOneπ (Rep.res H.subtype M))) x) = (CategoryTheory.ConcreteCategory.hom (HNegOneπ M)) ((Submodule.inclusion ⋯) x)

Corestriction in degree -1 sends the class of a norm-zero element to the class of the same element.

theorem TauCeti.TateCohomology.HNegOneCor_comp_HNegOneRes_apply {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) (x : ↑(tateCohomology M (-1))) : (CategoryTheory.ConcreteCategory.hom (HNegOneCor M H)) ((CategoryTheory.ConcreteCategory.hom (HNegOneRes M H)) x) = H.index • x

Corestriction of the restriction of a degree -1 class is the index multiple of it.

theorem TauCeti.TateCohomology.HNegOneRes_comp_HNegOneCor {R G : Type u} [CommRing R] [Group G] [Fintype G] (M : Rep.{u, u, u} R G) (H : Subgroup G) : CategoryTheory.CategoryStruct.comp (HNegOneRes M H) (HNegOneCor M H) = H.index • CategoryTheory.CategoryStruct.id (tateCohomology M (-1))

Restriction followed by corestriction is multiplication by the index, in degree -1.

theorem TauCeti.TateCohomology.HNegOneRes_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) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (-1)).map f) (HNegOneRes N H) = CategoryTheory.CategoryStruct.comp (HNegOneRes M H) ((tateCohomologyFunctor (-1)).map ((Rep.resFunctor H.subtype).map f))

Tate restriction in degree -1 is natural in the coefficient representation.

theorem TauCeti.TateCohomology.HNegOneRes_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) {Z : ModuleCat R} (h : tateCohomology (Rep.res H.subtype N) (-1) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (-1)).map f) (CategoryTheory.CategoryStruct.comp (HNegOneRes N H) h) = CategoryTheory.CategoryStruct.comp (HNegOneRes M H) (CategoryTheory.CategoryStruct.comp ((tateCohomologyFunctor (-1)).map (Rep.resMap H.subtype f)) h)

Tate restriction in degree -1 is natural in the coefficient representation.

theorem TauCeti.TateCohomology.isIntertwiningMap_trivial_res {G : Type} [Group G] (S : Subgroup G) : (Rep.trivial ℤ ↥S ℤ).ρ.IsIntertwiningMap (MonoidHom.comp (Rep.res S.subtype (Rep.trivial ℤ G ℤ)).ρ ↑(MulEquiv.refl ↥S)) ↑(LinearEquiv.refl ℤ ℤ)

The identity of ℤ intertwines the trivial representation of a subgroup S of G with the restriction to S of the trivial representation of G.

noncomputable def TauCeti.TateCohomology.trivialResIso {G : Type} [Group G] [Finite G] (S : Subgroup G) (n : ℤ) : tateCohomology (Rep.trivial ℤ ↥S ℤ) n ≅ tateCohomology (Rep.res S.subtype (Rep.trivial ℤ G ℤ)) n

Tate cohomology of the trivial integral representation of a subgroup S of G, identified with Tate cohomology of the restriction to S of the trivial integral representation of G.

@[simp]

theorem TauCeti.TateCohomology.trivialResIso_hom {G : Type} [Group G] [Finite G] (S : Subgroup G) (n : ℤ) : (trivialResIso S n).hom = map ⋯ n

The comparison trivialResIso is the Tate map attached to the compatible pair isIntertwiningMap_trivial_res.

noncomputable def TauCeti.TateCohomology.resTrivialTateHZeroOne {G : Type} [Group G] [Finite G] (S : Subgroup G) : ↑(tateCohomology (Rep.res S.subtype (Rep.trivial ℤ G ℤ)) 0)

The class of 1 ∈ ℤ in degree-zero Tate cohomology of the restriction to S of the trivial integral representation of G.

theorem TauCeti.TateCohomology.resTrivialTateHZeroOne_def {G : Type} [Group G] [Finite G] (S : Subgroup G) : resTrivialTateHZeroOne S = (CategoryTheory.ConcreteCategory.hom (H0π (Rep.res S.subtype (Rep.trivial ℤ G ℤ)))) ⟨1, ⋯⟩

The class of 1 is the degree-zero projection of the invariant 1.

theorem TauCeti.TateCohomology.exists_zsmul_resTrivialTateHZeroOne_eq {G : Type} [Group G] [Finite G] (S : Subgroup G) (x : ↑(tateCohomology (Rep.res S.subtype (Rep.trivial ℤ G ℤ)) 0)) : ∃ (n : ℤ), n • resTrivialTateHZeroOne S = x

Every degree-zero class of the restricted trivial integral representation is an integer multiple of the class of 1.

theorem TauCeti.TateCohomology.natCard_zsmul_resTrivialTateHZeroOne {G : Type} [Group G] [Finite G] (S : Subgroup G) : ↑(Nat.card ↥S) • resTrivialTateHZeroOne S = 0

The order of the subgroup kills the class of 1.

theorem TauCeti.TateCohomology.natCard_tateCohomology_zero_res_trivial_int_eq_card {G : Type} [Group G] [Finite G] (S : Subgroup G) : Nat.card ↑(tateCohomology (Rep.res S.subtype (Rep.trivial ℤ G ℤ)) 0) = Nat.card ↥S

Degree-zero Tate cohomology of the restricted trivial integral representation has the order of the subgroup.

theorem TauCeti.TateCohomology.isZero_tateCohomology_one_res_trivial_int {G : Type} [Group G] [Finite G] (S : Subgroup G) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype (Rep.trivial ℤ G ℤ)) 1)

Degree-one Tate cohomology of the restricted trivial integral representation vanishes: it is H¹(S, ℤ) = Hom(S, ℤ) = 0.