Linearity of Tate cohomology in the coefficient morphism

Mathlib shows that the Tate complex of a representation of a finite group is an additive functor of the representation. This file records that it is moreover k-linear, and deduces that Tate cohomology in each integer degree is an additive, k-linear functor: the map induced on tateCohomology · n by c • f is c times the map induced by f.

Main statements

• TauCeti.TateCohomology.tateComplex_map_smul: the chain map of Tate complexes induced by c • f is c • tateComplex.map f.
• The Functor.Linear instances on tateComplexFunctor k G and on tateCohomologyFunctor n, and the Functor.Additive instance on tateCohomologyFunctor n.
• TauCeti.TateCohomology.smul_bijective: a bijective scalar action on a representation induces a bijective scalar action on its Tate cohomology.

theorem TauCeti.TateCohomology.tateComplex_map_smul {k G : Type u} [CommRing k] [Group G] [Fintype G] {M N : Rep k G} (c : k) (f : M ⟶ N) : tateComplex.map (c • f) = c • tateComplex.map f

The chain map of Tate complexes induced by a scalar multiple of a morphism of representations is the scalar multiple of the induced chain map.

instance TauCeti.TateCohomology.instLinearRepCochainComplexModuleCatIntTateComplexFunctor_tauCeti {k G : Type u} [CommRing k] [Group G] [Fintype G] : CategoryTheory.Functor.Linear k (tateComplexFunctor k G)

The Tate complex is a k-linear functor of the representation.

instance TauCeti.TateCohomology.instAdditiveRepModuleCatTateCohomologyFunctor_tauCeti {k G : Type u} [CommRing k] [Group G] [Fintype G] (n : ℤ) : (tateCohomologyFunctor n).Additive

Tate cohomology in each degree is an additive functor of the representation.

instance TauCeti.TateCohomology.instLinearRepModuleCatTateCohomologyFunctor_tauCeti {k G : Type u} [CommRing k] [Group G] [Fintype G] (n : ℤ) : CategoryTheory.Functor.Linear k (tateCohomologyFunctor n)

Tate cohomology in each degree is a k-linear functor of the representation.

theorem TauCeti.TateCohomology.smul_bijective {k G : Type u} [CommRing k] [Group G] [Fintype G] (c : k) (A : Rep k G) (hA : Function.Bijective fun (x : ↑A) => c • x) (n : ℤ) : Function.Bijective fun (x : ↑(tateCohomology A n)) => c • x

A scalar acting bijectively on a representation acts bijectively on its Tate cohomology.