Documentation

TauCeti.RepresentationTheory.Homological.TateCohomology.Cup.GradedComm

Graded commutativity of the Tate cup product #

For a finite group G, the tensor braiding identifies the two orders of the Tate cup product up to the Koszul sign: for classes x of degree p and y of degree q,

β (x ∪ y) = (-1)^(p * q) (y ∪ x) (TauCeti.TateCohomology.cup_gradedComm).

When one class has degree zero the sign is trivial, and the result is built into the construction of the all-degree product. The product in bidegree (p, 0) is cupH0, while the product in bidegree (0, p) is its opposite transported through the tensor braiding (cup0H). The symmetry identity for the braiding then gives both edge forms.

The general case follows by induction on the second degree q, through the upward and downward dimension-shifting sequences of the second coefficient representation. On the left, the cup product with a shifted class satisfies x ∪ δ y = (-1)^p δ (x ∪ y) by definition, and the braiding commutes with the connecting maps. On the right, δ y ∪ x = δ (y ∪ x) because the dimension-shifting sequences split k-linearly (TauCeti.TateCohomology.δ_cup_of_leftInverse). The extra sign (-1)^p is the change of the Koszul sign from (-1)^(p * q) to (-1)^(p * (q + 1)).

Main statements #

References #

source
@[simp]
theorem TauCeti.TateCohomology.cupH0_eq_flip_cup0H {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) (p : ℤ) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N 0)) :
(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor p).map (β_ M N).hom)) (((cupH0 M N p) x) y) = ((cup0H N M p) y) x

Graded commutativity in bidegree (p, 0): after braiding the coefficients, cupping a degree-p class with a degree-zero class agrees with cupping in the opposite order. The Koszul sign is trivial because the second degree is zero.

source
@[simp]
theorem TauCeti.TateCohomology.cup0H_eq_flip_cupH0 {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) (q : ℤ) (x : ↑(tateCohomology M 0)) (y : ↑(tateCohomology N q)) :
(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor q).map (β_ M N).hom)) (((cup0H M N q) x) y) = ((cupH0 N M q) y) x

Graded commutativity in bidegree (0, q): after braiding the coefficients, cupping a degree-zero class with a degree-q class agrees with cupping in the opposite order. The Koszul sign is trivial because the first degree is zero.

Graded commutativity in all bidegrees #

source
theorem TauCeti.TateCohomology.cup_gradedComm {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) {p q r : ℤ} (h : p + q = r) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N q)) :
(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor r).map (β_ M N).hom)) (((cup M N p q r h) x) y) = (p * q).negOnePow • ((cup N M q p r ⋯) y) x

Graded commutativity of the Tate cup product: after braiding the coefficients, cupping a class x of degree p with a class y of degree q agrees with cupping in the opposite order up to the Koszul sign, β (x ∪ y) = (-1)^(p * q) (y ∪ x), in all integer bidegrees.

source
theorem TauCeti.TateCohomology.cup_right_comm {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₂ : p + s = r₁') (h : r₁ + s = r) (h' : r₁' + q = r) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N q)) (z : ↑(tateCohomology P s)) :
(CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor r).map (CategoryTheory.MonoidalCategoryStruct.associator M P N).inv)) ((CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor r).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (β_ N P).hom))) ((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))) = (q * s).negOnePow • ((cup (CategoryTheory.MonoidalCategoryStruct.tensorObj M P) N r₁' q r h') (((cup M P p s r₁' h₂) x) z)) y

Right commutativity of the iterated cup product. Cupping x ∪ y with z and cupping x ∪ z with y agree up to the Koszul sign (-1) ^ (q * s) and the associators and braiding identifying the coefficient modules (M ⊗ N) ⊗ P and (M ⊗ P) ⊗ N.