The Tate cup product along an isomorphism of finite groups

A compatible pair (e, φ), a group isomorphism e : G ≃* H together with a linear map φ from a G-representation M to an H-representation N satisfying φ ∘ ρ g = σ (e g) ∘ φ, induces a map TauCeti.TateCohomology.map on Tate cohomology in every degree. This file proves that these maps are compatible with the Tate cup product in all integer bidegrees (TauCeti.TateCohomology.map_cup): for compatible pairs (e, φ₁) and (e, φ₂), the pair (e, φ₁ ⊗ φ₂) carries x ∪ y to the cup product of the images of x and y.

The main application is conjugation of a finite normal layer of a class formation, under which cup product with the fundamental class, and hence the Artin map, is equivariant.

Main statements

• TauCeti.TateCohomology.map_cup: every pair of compatible pairs along the same isomorphism is compatible with the cup product.

References

• K. S. Brown, Cohomology of Groups, Chapter V, §3 and Chapter VI, §5.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, Chapter I, §5.

theorem TauCeti.TateCohomology.map_cup {k G H : Type u} [CommRing k] [Group G] [Group H] [Fintype G] [Fintype H] {e : G ≃* H} {M₁ M₂ : Rep.{u, u, u} k G} {N₁ N₂ : Rep.{u, u, u} k H} {φ₁ : ↑M₁ →ₗ[k] ↑N₁} {φ₂ : ↑M₂ →ₗ[k] ↑N₂} (h₁ : M₁.ρ.IsIntertwiningMap (MonoidHom.comp N₁.ρ ↑e) φ₁) (h₂ : M₂.ρ.IsIntertwiningMap (MonoidHom.comp N₂.ρ ↑e) φ₂) (p q r : ℤ) (h : p + q = r) (x : ↑(tateCohomology M₁ p)) (y : ↑(tateCohomology M₂ q)) : (CategoryTheory.ConcreteCategory.hom (map ⋯ r)) (((cup M₁ M₂ p q r h) x) y) = ((cup N₁ N₂ p q r h) ((CategoryTheory.ConcreteCategory.hom (map h₁ p)) x)) ((CategoryTheory.ConcreteCategory.hom (map h₂ q)) y)

The Tate cup product is natural along compatible pairs. For compatible pairs (e, φ₁) from M₁ to N₁ and (e, φ₂) from M₂ to N₂ along one isomorphism e : G ≃* H of finite groups, the pair (e, φ₁ ⊗ φ₂) carries x ∪ y to the cup product of the images of x and y, in every bidegree.