Documentation

TauCeti.RepresentationTheory.Homological.TateCohomology.Cup.ZeroLeft

The Tate cup product with a degree-zero class in the first factor #

The degree-zero cup product in the second factor also gives a product with a degree-zero class in the first factor. The symmetry of the tensor product of representations transports the existing product without introducing a second cohomological construction. Its value on classes represented by invariants is the class of the elementary tensor in the stated order.

This is the (0,n) edge of the all-bidegree Tate cup product used in Tate's theorem. Its compatibility with connecting maps is the left-factor/braided analogue of δ_cupH0.

References #

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

Cup product with a degree-zero class in the first factor. It is the degree-zero product in the second factor followed by the symmetry N ⊗ M ≅ M ⊗ N.

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

    The left degree-zero product is the right degree-zero product followed by the symmetry of coefficients.

    source
    @[simp]
    theorem TauCeti.TateCohomology.cup0H_H0π {k G : Type u} [CommRing k] [Group G] [Fintype G] {M N : Rep.{u, u, u} k G} (n : ℤ) (x : ↥M.ρ.invariants) (y : ↑(tateCohomology N n)) :
    ((cup0H M N n) ((CategoryTheory.ConcreteCategory.hom (H0π M)) x)) y = (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map (CategoryTheory.CategoryStruct.comp (N.tensorInvariant x) (β_ N M).hom))) y

    For an invariant x, the left cup product is induced by y ↦ x ⊗ y.

    source
    @[simp]
    theorem TauCeti.TateCohomology.cup0H_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) :
    ((cup0H 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 bidegree (0,0), the product is represented by the tensor of the two invariants in their original order.

    source
    theorem TauCeti.TateCohomology.cup0H_zero {k G : Type u} [CommRing k] [Group G] [Fintype G] (M N : Rep.{u, u, u} k G) :
    cup0H M N 0 = cupH0 M N 0

    In bidegree (0, 0) the product with a degree-zero class in the first factor is the product with a degree-zero class in the second factor.

    source
    theorem TauCeti.TateCohomology.cup0H_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 0)) (y : ↑(tateCohomology N n)) :
    ((cup0H M' N n) ((CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor 0).map f)) x)) y = (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f N))) (((cup0H M N n) x) y)

    Naturality of the left degree-zero product in its first coefficient.

    source
    theorem TauCeti.TateCohomology.cup0H_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 0)) (y : ↑(tateCohomology N n)) :
    ((cup0H M N' n) x) ((CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map g)) y) = (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor n).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M g))) (((cup0H M N n) x) y)

    Naturality of the left degree-zero product in its second coefficient.

    source
    theorem TauCeti.TateCohomology.δ_cup0H {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) (hMS : (S.map (CategoryTheory.MonoidalCategory.tensorLeft M)).ShortExact) (n : ℤ) (x : ↑(tateCohomology M 0)) (y : ↑(tateCohomology S.X₃ n)) :
    (CategoryTheory.ConcreteCategory.hom (TateCohomology.δ hMS n)) (((cup0H M S.X₃ n) x) y) = ((cup0H M S.X₁ (n + 1)) x) ((CategoryTheory.ConcreteCategory.hom (TateCohomology.δ hS n)) y)

    Cup product with a degree-zero class in the first factor commutes with the connecting map in the second factor, provided tensoring the short exact sequence with that first factor preserves exactness. This is the left-factor/braided analogue of δ_cupH0.