Theorems · Definition · group theory

TateCohomology.tateComplex.evalNonneg

{R G : Type u} →
  [inst : CommRing R] →
    [inst_1 : Group G] →
      [inst_2 : Fintype G] →
        (n : ℕ) →
          (tateComplexFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℤ) ↑n) ≅
            (groupCohomology.cochainsFunctor R G).comp (HomologicalComplex.eval (ModuleCat R) (ComplexShape.up ℕ) n)

The natural isomorphism between the n-th index of the Tate complex and inhomogeneous n-cochains for 0 ≤ n.

Defined in

Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Cited by

1 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingGroupFintype