Restriction and corestriction in Tate degree -2 on the abelianization

For a finite group G and trivial coefficients A, degree -2 Tate cohomology is H_Tate⁻²(G, A) ≃ Gᵃᵇ ⊗ A (TauCeti.TateCohomology.HNegTwoAddEquivTensorOfIsTrivial). This file identifies the two change-of-group maps in this degree under that identification:

• restriction to a subgroup S ≤ G, H_Tate⁻²(G, A) ⟶ H_Tate⁻²(S, A), is the group-theoretic transfer (Verlagerung) Gᵃᵇ → Sᵃᵇ, tensored with A;
• corestriction along a homomorphism f : H →* G, H_Tate⁻²(H, A) ⟶ H_Tate⁻²(G, A), is Abelianization.map f, tensored with A.

Together they make the identification H_Tate⁻²(G, A) ≃ Gᵃᵇ ⊗ A natural in the group: a statement about restriction or corestriction in Tate degree -2 can be transported to the corresponding statement about the Verlagerung or Abelianization.map. For A = ℤ, these are the compatibilities of the identification H_Tate⁻²(G, ℤ) ≃ Gᵃᵇ with restriction and corestriction that the reciprocity isomorphism Gᵃᵇ ≃ H_Tate⁰(G, C) inherits.

Main results

• TauCeti.TateCohomology.HNegTwoAddEquivTensorOfIsTrivial_HNegTwoRes: restriction in degree -2 is the Verlagerung.
• TauCeti.TateCohomology.HNegTwoAddEquivTensorOfIsTrivial_HNegTwoCor: corestriction in degree -2 is the map induced on abelianizations.
• TauCeti.TateCohomology.HNegTwoAddEquivAbelianization_map: with integral coefficients, Tate cohomology along an isomorphism of finite groups is, in degree -2, the induced isomorphism of abelianizations.

References

• J.-P. Serre, Local Fields, Chapter VII, §8 and Chapter XI, §3.
• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §4.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoAddEquivTensorOfIsTrivial_HNegTwoRes {k G : Type u} [CommRing k] [Group G] [Fintype G] (S : Subgroup G) (A : Rep.{u, u, u} k G) [A.IsTrivial] (x : ↑(tateCohomology A (-2))) : (HNegTwoAddEquivTensorOfIsTrivial (Rep.res S.subtype A)) ((CategoryTheory.ConcreteCategory.hom (HNegTwoRes A S)) x) = (LinearMap.rTensor (↑A) (MonoidHom.toAdditive (Abelianization.lift Abelianization.of.transfer)).toIntLinearMap) ((HNegTwoAddEquivTensorOfIsTrivial A) x)

Restriction in Tate degree -2 is the Verlagerung. For a subgroup S of a finite group G and trivial coefficients A, restriction H_Tate⁻²(G, A) ⟶ H_Tate⁻²(S, A) becomes V ⊗ id : Gᵃᵇ ⊗ A → Sᵃᵇ ⊗ A under the identifications H_Tate⁻² ≃ (-)ᵃᵇ ⊗ A, where V is the group-theoretic transfer.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoAddEquivTensorOfIsTrivial_HNegTwoCor {k G : Type u} [CommRing k] [Group G] [Fintype G] {H : Type u} [Group H] [Fintype H] (A : Rep.{u, u, u} k G) [A.IsTrivial] (f : H →* G) (y : ↑(tateCohomology (Rep.res f A) (-2))) : (HNegTwoAddEquivTensorOfIsTrivial A) ((CategoryTheory.ConcreteCategory.hom (HNegTwoCor A f)) y) = (LinearMap.rTensor (↑A) (MonoidHom.toAdditive (Abelianization.map f)).toIntLinearMap) ((HNegTwoAddEquivTensorOfIsTrivial (Rep.res f A)) y)

Corestriction in Tate degree -2 is the map induced on abelianizations. For a homomorphism f : H →* G of finite groups and trivial coefficients A, corestriction H_Tate⁻²(H, A) ⟶ H_Tate⁻²(G, A) becomes Abelianization.map f ⊗ id : Hᵃᵇ ⊗ A → Gᵃᵇ ⊗ A under the identifications H_Tate⁻² ≃ (-)ᵃᵇ ⊗ A.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoAddEquivAbelianization_HNegTwoRes {G : Type} [Group G] [Fintype G] (S : Subgroup G) (x : ↑(tateCohomology (Rep.trivial ℤ G ℤ) (-2))) : (TensorProduct.rid ℤ (Additive (Abelianization ↥S))) ((HNegTwoAddEquivTensorOfIsTrivial (Rep.res S.subtype (Rep.trivial ℤ G ℤ))) ((CategoryTheory.ConcreteCategory.hom (HNegTwoRes (Rep.trivial ℤ G ℤ) S)) x)) = (MonoidHom.toAdditive (Abelianization.lift Abelianization.of.transfer)) (HNegTwoAddEquivAbelianization x)

Under the integral degree--2 identification, restriction to a subgroup is the group-theoretic transfer.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoAddEquivAbelianization_HNegTwoCor {G : Type} [Group G] [Fintype G] {H : Type} [Group H] [Fintype H] (f : H →* G) (y : ↑(tateCohomology (Rep.res f (Rep.trivial ℤ G ℤ)) (-2))) : HNegTwoAddEquivAbelianization ((CategoryTheory.ConcreteCategory.hom (HNegTwoCor (Rep.trivial ℤ G ℤ) f)) y) = (MonoidHom.toAdditive (Abelianization.map f)) ((TensorProduct.rid ℤ (Additive (Abelianization H))) ((HNegTwoAddEquivTensorOfIsTrivial (Rep.res f (Rep.trivial ℤ G ℤ))) y))

Under the integral degree--2 identification, corestriction along a homomorphism is the map that it induces on abelianizations.

@[simp]

theorem TauCeti.TateCohomology.HNegTwoAddEquivAbelianization_map {G : Type} [Group G] [Fintype G] {H : Type} [Group H] [Fintype H] (e : G ≃* H) (x : ↑(tateCohomology (Rep.trivial ℤ G ℤ) (-2))) : HNegTwoAddEquivAbelianization ((CategoryTheory.ConcreteCategory.hom (map ⋯ (-2))) x) = (MulEquiv.toAdditive e.abelianizationCongr) (HNegTwoAddEquivAbelianization x)

The integral degree--2 identification is natural along isomorphisms of groups: Tate cohomology along an isomorphism e : G ≃* H of finite groups, with integral coefficients, is the isomorphism Gᵃᵇ ≃ Hᵃᵇ induced by e in degree -2.