Cup product with trivial integral coefficients in degree zero #
The canonical class of 1 acts as the identity under cup product after removing the left tensor
unit. Consequently, cup product with a generating class is bijective when the target has the
order of the finite group.
These Tate cohomology operations are parameterized by a representation and live alongside the
generic cup product in TauCeti.TateCohomology.
noncomputable def
TauCeti.TateCohomology.cupTrivialInt
{H : Type}
[Group H]
[Fintype H]
(N : Rep.{0, 0, 0} ℤ H)
{q : ℤ}
(u : ↑(tateCohomology N q))
:
Cup product with a class of degree q, with trivial integral coefficients in degree zero
and the left tensor unit removed.
Instances For
theorem
TauCeti.TateCohomology.cupTrivialInt_apply
{H : Type}
[Group H]
[Fintype H]
(N : Rep.{0, 0, 0} ℤ H)
{q : ℤ}
(u : ↑(tateCohomology N q))
(x : ↑(tateCohomology (Rep.trivial ℤ H ℤ) 0))
:
(cupTrivialInt N u) x = (CategoryTheory.ConcreteCategory.hom
((tateCohomologyFunctor q).map (CategoryTheory.MonoidalCategoryStruct.leftUnitor N).hom))
(((cup (Rep.trivial ℤ H ℤ) N 0 q q ⋯) x) u)
The trivial-integral cup map evaluates by cup product followed by the left unitor.
@[simp]
theorem
TauCeti.TateCohomology.cupTrivialInt_trivialTateHZeroOne
{H : Type}
[Group H]
[Fintype H]
(N : Rep.{0, 0, 0} ℤ H)
{q : ℤ}
(u : ↑(tateCohomology N q))
:
The canonical degree-zero class of 1 acts as the identity under cup product.
theorem
TauCeti.TateCohomology.cupTrivialInt_bijective
{H : Type}
[Group H]
[Fintype H]
(N : Rep.{0, 0, 0} ℤ H)
{q : ℤ}
(u : ↑(tateCohomology N q))
(hgen : ∀ (y : ↑(tateCohomology N q)), ∃ (m : ℤ), m • u = y)
(hcard : Nat.card ↑(tateCohomology N q) = Fintype.card H)
:
Function.Bijective ⇑(cupTrivialInt N u)
Cupping with a generating degree-q class is bijective when the target has the order of
the finite group.