The cup product and the connecting maps of a short exact sequence

The Tate cup product is defined in the second variable by the rule x ∪ δ y = (-1)^p δ (x ∪ y) for the connecting maps δ of the upward dimension-shifting sequence when y has degree q ≥ 0, and of the downward one when q < 0 (TauCeti.TateCohomology.cup_dimensionShiftUpIso_hom, TauCeti.TateCohomology.cup_dimensionShiftDownIso_hom). This file extends the rule, in every degree q, to the connecting maps of every short exact sequence 0 → N₁ → N₂ → N₃ → 0 whose first map has a k-linear retraction (TauCeti.TateCohomology.cup_δ_of_leftInverse). This applies in particular to the tensor products of the dimension-shifting sequences with a representation, which are split k-linearly but in general not as sequences of representations.

When the first factor M is flat over k, the rule holds for every short exact sequence in the second variable (TauCeti.TateCohomology.cup_δ_of_flat). This covers sequences which do not split over k, such as 0 → ℤ → ℚ → ℚ/ℤ → 0 against classes of the trivial representation ℤ, whose connecting map produces the class δχ ∈ H²(G, ℤ) of a character χ in the Artin–Tate character formula.

In the first variable, the rule δ (x ∪ y) = δ x ∪ y holds for every short exact sequence whose first map has a k-linear retraction (TauCeti.TateCohomology.δ_cup_of_leftInverse), where the connecting map on the left is that of the tensor product of the sequence on the right with the second factor. It is proved by the same dimension shifting in the second variable, using that the connecting maps of the 3 × 3 diagram of tensor products of two k-split short exact sequences anticommute (TauCeti.TateCohomology.δ_comp_δ_eq_neg).

Main statements

• TauCeti.TateCohomology.cup_δ_of_leftInverse: for a short exact sequence whose first map has a k-linear retraction, x ∪ δ y = (-1)^p δ (x ∪ y) for x of degree p and y of any degree q.
• TauCeti.TateCohomology.cup_δ_of_flat: if the underlying module of M is flat over k, then x ∪ δ y = (-1)^p δ (x ∪ y) for every short exact sequence, x of degree p and y of any degree q.
• TauCeti.TateCohomology.δ_cup_of_leftInverse: the rule in the first variable: for a short exact sequence whose first map has a k-linear retraction, δ (x ∪ y) = δ x ∪ y for x and y of any degrees.

References

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

theorem TauCeti.TateCohomology.cup_δ_of_leftInverse {k G : Type u} [CommRing k] [Group G] [Fintype G] (M : Rep.{u, u, u} k G) {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) {r : ↑S.X₂ →ₗ[k] ↑S.X₁} (hr : Function.LeftInverse ⇑r ⇑(Rep.Hom.hom S.f)) {p q n : ℤ} (h : p + q = n) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology S.X₃ q)) : ((cup M S.X₁ p (q + 1) (n + 1) ⋯) x) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.δ hS q)) y) = p.negOnePow • (CategoryTheory.ConcreteCategory.hom (TateCohomology.δ ⋯ n)) (((cup M S.X₃ p q n h) x) y)

The cup product rule for a split short exact sequence in the second variable. For a short exact sequence S whose first map has a k-linear retraction, x of degree p and y of any degree q, x ∪ δ y = (-1)^p δ (x ∪ y), where the second δ is the connecting map of the tensor product of S with M, which is short exact by Rep.shortExact_map_tensorLeft_of_leftInverse.

theorem TauCeti.TateCohomology.cup_δ_of_flat {k G : Type u} [CommRing k] [Group G] [Fintype G] (M : Rep.{u, u, u} k G) [Module.Flat k ↑M] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) {p q n : ℤ} (h : p + q = n) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology S.X₃ q)) : ((cup M S.X₁ p (q + 1) (n + 1) ⋯) x) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.δ hS q)) y) = p.negOnePow • (CategoryTheory.ConcreteCategory.hom (TateCohomology.δ ⋯ n)) (((cup M S.X₃ p q n h) x) y)

The cup product rule for a flat first factor. If the underlying module of M is flat over k, then for every short exact sequence S, x of degree p and y of any degree q, x ∪ δ y = (-1)^p δ (x ∪ y), where the second δ is the connecting map of the tensor product of S with M, which is short exact by Rep.shortExact_map_tensorLeft_of_flat. Unlike TauCeti.TateCohomology.cup_δ_of_leftInverse, the sequence need not split k-linearly: for k = ℤ and M the trivial representation ℤ, this applies to 0 → ℤ → ℚ → ℚ/ℤ → 0.

The cup product rule in the first variable

theorem TauCeti.TateCohomology.δ_cup_of_leftInverse {k G : Type u} [CommRing k] [Group G] [Fintype G] {S : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} (hS : S.ShortExact) {r : ↑S.X₂ →ₗ[k] ↑S.X₁} (hr : Function.LeftInverse ⇑r ⇑(Rep.Hom.hom S.f)) (N : Rep.{u, u, u} k G) {p q n : ℤ} (h : p + q = n) (x : ↑(tateCohomology S.X₃ p)) (y : ↑(tateCohomology N q)) : (CategoryTheory.ConcreteCategory.hom (TateCohomology.δ ⋯ n)) (((cup S.X₃ N p q n h) x) y) = ((cup S.X₁ N (p + 1) q (n + 1) ⋯) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.δ hS p)) x)) y

The cup product rule in the first variable for a split short exact sequence. For a short exact sequence S whose first map has a k-linear retraction, x of degree p and y of any degree q, δ (x ∪ y) = δ x ∪ y, where the first δ is the connecting map of the tensor product of S on the right with N, which is short exact by Rep.shortExact_map_tensorRight_of_leftInverse. Together with the rule x ∪ δ y = (-1)^p δ (x ∪ y) in the second variable (TauCeti.TateCohomology.cup_δ_of_leftInverse), this is the compatibility of the cup product with connecting maps in both variables.