Associativity of the Tate cup product

For a finite group G, the tensor associator identifies the two ways to cup three Tate classes x, y, z of arbitrary integer degrees p, q, s: α ((x ∪ y) ∪ z) = x ∪ (y ∪ z) (TauCeti.TateCohomology.cup_assoc). Products of three Tate classes may therefore be rebracketed freely, whatever their degrees.

Main statements

• TauCeti.TateCohomology.cup_assoc: associativity of the Tate cup product in all integer tridegrees.
• TauCeti.TateCohomology.cupH0_cup_assoc, TauCeti.TateCohomology.cup_cupH0_assoc, TauCeti.TateCohomology.cupH0_assoc_zero: its forms with a degree-zero class, in the simp normal form where the degree-zero products are written with cupH0 and cup0H.

References

• E. Artin and J. Tate, Class Field Theory, Preliminaries §2.
• K. S. Brown, Cohomology of Groups, Chapter VI, §5.

Associativity in all tridegrees

@[simp]

theorem TauCeti.TateCohomology.cup_assoc {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N P : Rep.{u, u, u} k G) {p q s r₁ r₂ r : ℤ} (h₁ : p + q = r₁) (h₂ : q + s = r₂) (h : r₁ + s = r) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N q)) (z : ↑(tateCohomology P s)) : (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor r).map (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom)) (((cup (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P r₁ s r h) (((cup M N p q r₁ h₁) x) y)) z) = ((cup M (CategoryTheory.MonoidalCategoryStruct.tensorObj N P) p r₂ r ⋯) x) (((cup N P q s r₂ h₂) y) z)

Associativity of the Tate cup product in all integer tridegrees: for classes x, y, z of degrees p, q, s, the tensor associator carries (x ∪ y) ∪ z to x ∪ (y ∪ z).

@[simp]

theorem TauCeti.TateCohomology.cup_cupH0_assoc {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N P : Rep.{u, u, u} k G) {p q r : ℤ} (h : p + q = r) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N 0)) (z : ↑(tateCohomology P q)) : (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor r).map (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom)) (((cup (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P p q r h) (((cupH0 M N p) x) y)) z) = ((cup M (CategoryTheory.MonoidalCategoryStruct.tensorObj N P) p q r h) x) (((cup0H N P q) y) z)

Associativity of the Tate cup product when the middle class has degree zero, in the simp normal form where the degree-zero cups are written with cupH0 and cup0H.

@[simp]

theorem TauCeti.TateCohomology.cupH0_cup_assoc {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N P : Rep.{u, u, u} k G) {p q r : ℤ} (h : p + q = r) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N q)) (z : ↑(tateCohomology P 0)) : (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor r).map (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom)) (((cupH0 (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P r) (((cup M N p q r h) x) y)) z) = ((cup M (CategoryTheory.MonoidalCategoryStruct.tensorObj N P) p q r h) x) (((cupH0 N P q) y) z)

Associativity of the Tate cup product when the last class has degree zero, in the simp normal form where the degree-zero cups are written with cupH0.

@[simp]

theorem TauCeti.TateCohomology.cupH0_assoc_zero {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N P : Rep.{u, u, u} k G) (p : ℤ) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N 0)) (z : ↑(tateCohomology P 0)) : (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor p).map (CategoryTheory.MonoidalCategoryStruct.associator M N P).hom)) (((cupH0 (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) P p) (((cupH0 M N p) x) y)) z) = ((cupH0 M (CategoryTheory.MonoidalCategoryStruct.tensorObj N P) p) x) (((cupH0 N P 0) y) z)

Cup product with two degree-zero Tate classes is associative, after applying the tensor associator to the coefficient representation.