Documentation

TauCeti.RepresentationTheory.Homological.TateCohomology.Cup.Product

The Tate cup product in all bidegrees #

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

tateCohomology M p × tateCohomology N q → tateCohomology (M ⊗ N) r, r = p + q,

for all integers p and q, as a k-bilinear map. It extends the product cupH0 with a degree-zero class by dimension shifting in the second variable (Cassels–Fröhlich, Chapter IV, §7; Brown, Chapter VI, §5). Writing δ for the connecting maps of the dimension-shifting sequences 0 → N → Coind_⊥^G N → dimensionShiftUp N → 0 and 0 → dimensionShiftDown N → Ind_⊥^G N → N → 0, which are isomorphisms on Tate cohomology, and also for the connecting maps of the same sequences tensored on the left with M, the product is determined by its value cupH0 on degree-zero classes and by the rule

x ∪ δ y = (-1)^p δ (x ∪ y) for x of degree p.

The sign is the standard one for a bigraded product compatible with connecting homomorphisms in the second variable. For q ≥ 0 the rule is applied upwards, with the upward shift of N, and for q < 0 downwards, with the downward shift of N; in each range the rule holds by construction (cup_dimensionShiftUpIso_hom, cup_dimensionShiftDownIso_hom). That the rule holds for every k-split short exact sequence in the second variable, the compatibility with connecting maps in the first variable, associativity, graded commutativity and the compatibility with restriction are the further properties of the product; they are not proved here.

The target degree of cup is a parameter r together with a proof of p + q = r, in the style of Mathlib's ShortComplex.ShortExact.δ. The definition transports the degree produced by its recursion to r along this proof, once, so that consumers can supply the target degree they need together with the equality of degrees and never transport classes themselves.

In bidegree (0, q) the product is the existing product cup0H with a degree-zero class in the first factor (cup_zero_left), because both satisfy the same rule for the dimension shifts.

Main definitions #

Main statements #

References #

source
noncomputable def TauCeti.TateCohomology.cup {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) :
↑(tateCohomology M p) →ₗ[k] ↑(tateCohomology N q) →ₗ[k] ↑(tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) r)

The Tate cup product H^p(G, M) × H^q(G, N) → H^r(G, M ⊗ N) for p + q = r, in all integer bidegrees, as a k-bilinear map. In bidegree (p, 0) it is cupH0 (cup_zero_right), and it is determined from there by the rule x ∪ δ y = (-1)^p δ (x ∪ y) for the connecting maps of the dimension-shifting sequences of N and of their tensor products with M (cup_dimensionShiftUpIso_hom, cup_dimensionShiftDownIso_hom).

Instances For

    The unfolding lemmas below are stated with the target degree in the form in which the recursion produces it, so that the transport along an equality of degrees in the definition of cup is along a reflexivity proof and disappears definitionally. Where a proof needs them at a second degree such as (n : ℤ) + 1 or Int.negSucc n + 1, which is of the form the recursion matches on by definition but not syntactically, they are applied as terms through LinearMap.congr_fun₂, which unifies up to definitional equality, rather than by rw.

    source
    @[simp]
    theorem TauCeti.TateCohomology.cup_zero_right {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) (p : ℤ) (h : p + 0 = p) :
    cup M N p 0 p h = cupH0 M N p

    In bidegree (p, 0) the cup product is the product cupH0 with a degree-zero class.

    source
    theorem TauCeti.TateCohomology.cup_dimensionShiftUpIso_hom {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) {p q r' r : ℤ} (hq : 0 ≤ q) (h' : p + q = r') (h : r' + 1 = r) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N.dimensionShiftUp q)) :
    ((cup M N p (q + 1) r ⋯) x) ((CategoryTheory.ConcreteCategory.hom (dimensionShiftUpIso N q).hom) y) = p.negOnePow • (CategoryTheory.ConcreteCategory.hom (tensorDimensionShiftUpIso N M r' r h).hom) (((cup M N.dimensionShiftUp p q r' h') x) y)

    The defining rule of the cup product for the upward dimension shift: for x of degree p and y of nonnegative degree q in dimensionShiftUp N, x ∪ δ y = (-1)^p δ (x ∪ y), where the first δ is the shift H^q(G, dimensionShiftUp N) ≅ H^(q+1)(G, N) and the second is its tensor product with M.

    source
    theorem TauCeti.TateCohomology.cup_dimensionShiftDownIso_hom {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) {p q r' r : ℤ} (hq : q < 0) (h' : p + q = r') (h : r' + 1 = r) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N q)) :
    ((cup M N.dimensionShiftDown p (q + 1) r ⋯) x) ((CategoryTheory.ConcreteCategory.hom (dimensionShiftDownIso N q).hom) y) = p.negOnePow • (CategoryTheory.ConcreteCategory.hom (tensorDimensionShiftDownIso N M r' r h).hom) (((cup M N p q r' h') x) y)

    The defining rule of the cup product for the downward dimension shift: for x of degree p and y of negative degree q in N, x ∪ δ y = (-1)^p δ (x ∪ y), where the first δ is the shift H^q(G, N) ≅ H^(q+1)(G, dimensionShiftDown N) and the second is its tensor product with M.

    source
    theorem TauCeti.TateCohomology.cup_dimensionShiftUpTwoIso_hom {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) (p : ℤ) (x : ↑(tateCohomology M p)) (z : ↑(tateCohomology N.dimensionShiftUp.dimensionShiftUp 0)) :
    ((cup M N p 2 (p + 2) ⋯) x) ((CategoryTheory.ConcreteCategory.hom (dimensionShiftUpTwoIso N).hom) z) = (CategoryTheory.ConcreteCategory.hom (tensorDimensionShiftUpIso N M (p + 1) (p + 2) ⋯).hom) ((CategoryTheory.ConcreteCategory.hom (tensorDimensionShiftUpIso N.dimensionShiftUp M p (p + 1) ⋯).hom) (((cupH0 M N.dimensionShiftUp.dimensionShiftUp p) x) z))

    Cup product with a degree-two class obtained by shifting a degree-zero class z twice is the degree-zero cup product with z, followed by the two tensored dimension shifts. The two signs (-1)^p of the shifting rule cancel.

    source
    @[simp]
    theorem TauCeti.TateCohomology.cup_zero_left {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) (q : ℤ) (h : 0 + q = q) :
    cup M N 0 q q h = cup0H M N q

    In bidegree (0, q) the cup product is the product cup0H with a degree-zero class in the first factor: both are cupH0 in bidegree (0, 0) and both satisfy x ∪ δ y = δ (x ∪ y) for the dimension shifts of the second variable.

    source
    theorem TauCeti.TateCohomology.cup_map_left {k G : Type u} [CommRing k] [Group G] [Fintype G] {M N M' : Rep.{u, u, u} k G} (f : M ⟶ M') (p q r : ℤ) (h : p + q = r) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N q)) :
    ((cup M' N p q r h) ((CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor p).map f)) x)) y = (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor r).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N))) (((cup M N p q r h) x) y)

    The cup product is natural in the first coefficient representation.

    source
    theorem TauCeti.TateCohomology.cup_map_right {k G : Type u} [CommRing k] [Group G] [Fintype G] {M N N' : Rep.{u, u, u} k G} (f : N ⟶ N') (p q r : ℤ) (h : p + q = r) (x : ↑(tateCohomology M p)) (y : ↑(tateCohomology N q)) :
    ((cup M N' p q r h) x) ((CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor q).map f)) y) = (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor r).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M f))) (((cup M N p q r h) x) y)

    The Tate cup product is natural in the second coefficient representation.