The Tate cup product with a degree-zero class

For a finite group G and representations M, N, this file constructs the Tate cup product

tateCohomology M n × tateCohomology N 0 → tateCohomology (M ⊗ N) n

in every integer degree n. An invariant y ∈ N^G gives a morphism of representations M ⟶ M ⊗ N, m ↦ m ⊗ y, and the cup product of x ∈ tateCohomology M n with the class of y is the image of x under the induced map. The substance is that this depends only on the class of y in tateCohomology N 0 = N^G / N_G N: when y = N_G z is a norm, m ↦ m ⊗ N_G z is the norm m ↦ ∑ g, g • (g⁻¹ • m ⊗ z) of the linear map m ↦ m ⊗ z, so it factors through a coinduced representation and induces zero on Tate cohomology.

This is the bidegree (n, 0) part of the cup product on Tate cohomology. It is compatible with the connecting homomorphisms in the first variable, and the cup product of two degree-zero classes is induced by M^G ⊗ N^G → (M ⊗ N)^G; these are the two properties from which the cup product in all bidegrees is obtained by dimension shifting (Cassels–Fröhlich, Chapter IV, §7).

Main definitions

• TauCeti.TateCohomology.cupH0: the cup product tateCohomology M n × tateCohomology N 0 → tateCohomology (M ⊗ N) n, as a k-bilinear map.

Main statements

• TauCeti.TateCohomology.map_tensorInvariant_eq_zero: m ↦ m ⊗ y induces zero on Tate cohomology when y is a norm.
• TauCeti.TateCohomology.cupH0_H0π: the cup product with the class of an invariant y is the map induced by m ↦ m ⊗ y.
• TauCeti.TateCohomology.cupH0_H0π_H0π: in degree zero, the cup product of the classes of x and y is the class of x ⊗ y.
• TauCeti.TateCohomology.cupH0_map_left, TauCeti.TateCohomology.cupH0_map_right: naturality in both coefficient representations.
• TauCeti.TateCohomology.δ_cupH0: compatibility with the connecting homomorphism of a short exact sequence in the first variable which stays short exact after tensoring with N.

References

• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter IV (Atiyah–Wall), §6 and §7.
• K. S. Brown, Cohomology of Groups, Chapter VI, §5.

theorem TauCeti.TateCohomology.map_tensorInvariant_eq_zero {k G : Type u} [CommRing k] [Group G] [Fintype G] {N : Rep.{u, u, u} k G} (M : Rep.{u, u, u} k G) {y : ↥N.ρ.invariants} (hy : ↑y ∈ LinearMap.range N.ρ.norm) (n : ℤ) : (tateCohomologyFunctor n).map (M.tensorInvariant y) = 0

If y is a norm, then m ↦ m ⊗ y induces zero on Tate cohomology in every degree: for y = N_G z it is the norm m ↦ ∑ g, g • (g⁻¹ • m ⊗ z) of the linear map m ↦ m ⊗ z.

noncomputable def TauCeti.TateCohomology.cupH0 {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) (n : ℤ) : ↑(tateCohomology M n) →ₗ[k] ↑(tateCohomology N 0) →ₗ[k] ↑(tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) n)

The Tate cup product with a degree-zero class, tateCohomology M n × tateCohomology N 0 → tateCohomology (M ⊗ N) n: the cup product of x with the class of an invariant y is the image of x under the map induced by m ↦ m ⊗ y (cupH0_H0π). It is well defined because that map vanishes on Tate cohomology when y is a norm (map_tensorInvariant_eq_zero).

@[simp]

theorem TauCeti.TateCohomology.cupH0_H0π {k G : Type u} [CommRing k] [Group G] [Fintype G] {M N : Rep.{u, u, u} k G} (n : ℤ) (x : ↑(tateCohomology M n)) (y : ↥N.ρ.invariants) : ((cupH0 M N n) x) ((CategoryTheory.ConcreteCategory.hom (H0π N)) y) = (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map (M.tensorInvariant y))) x

The cup product with the class of an invariant y is the map induced by m ↦ m ⊗ y.

@[simp]

theorem TauCeti.TateCohomology.cupH0_H0π_H0π {k G : Type u} [CommRing k] [Group G] [Fintype G] {M N : Rep.{u, u, u} k G} (x : ↥M.ρ.invariants) (y : ↥N.ρ.invariants) : ((cupH0 M N 0) ((CategoryTheory.ConcreteCategory.hom (H0π M)) x)) ((CategoryTheory.ConcreteCategory.hom (H0π N)) y) = (CategoryTheory.ConcreteCategory.hom (H0π (CategoryTheory.MonoidalCategoryStruct.tensorObj M N))) ⟨↑x ⊗ₜ[k] ↑y, ⋯⟩

In degree zero, the cup product of the classes of invariants x and y is the class of the invariant x ⊗ y.

theorem TauCeti.TateCohomology.cupH0_map_left {k G : Type u} [CommRing k] [Group G] [Fintype G] {M N M' : Rep.{u, u, u} k G} (f : M ⟶ M') (n : ℤ) (x : ↑(tateCohomology M n)) (y : ↑(tateCohomology N 0)) : ((cupH0 M' N n) ((CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map f)) x)) y = (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N))) (((cupH0 M N n) x) y)

The cup product with a degree-zero class is natural in the first coefficient representation.

theorem TauCeti.TateCohomology.cupH0_map_right {k G : Type u} [CommRing k] [Group G] [Fintype G] {M N N' : Rep.{u, u, u} k G} (g : N ⟶ N') (n : ℤ) (x : ↑(tateCohomology M n)) (y : ↑(tateCohomology N 0)) : ((cupH0 M N' n) x) ((CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor 0).map g)) y) = (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M g))) (((cupH0 M N n) x) y)

The cup product with a degree-zero class is natural in the second coefficient representation.

theorem TauCeti.TateCohomology.δ_cupH0 {k G : Type u} [CommRing k] [Group G] [Fintype G] {N : Rep.{u, u, u} k G} {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) (hSN : (S.map (CategoryTheory.MonoidalCategory.tensorRight N)).ShortExact) (n : ℤ) (x : ↑(tateCohomology S.X₃ n)) (y : ↑(tateCohomology N 0)) : (CategoryTheory.ConcreteCategory.hom (TateCohomology.δ hSN n)) (((cupH0 S.X₃ N n) x) y) = ((cupH0 S.X₁ N (n + 1)) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.δ hS n)) x)) y

The cup product with a degree-zero class commutes with the connecting homomorphism in the first variable: for a short exact sequence 0 → M₁ → M₂ → M₃ → 0 which stays short exact after tensoring with N (for instance one that splits k-linearly), δ (x ∪ y) = δ x ∪ y.