Theorems · Definition · group theory

TateCohomology.isoGroupHomology

{R G : Type u} →
  [inst : CommRing R] →
    [inst_1 : Group G] →
      [inst_2 : Fintype G] →
        (m : ℤ) → (n : ℕ) → m = -(↑n + 1) → [NeZero n] → tateCohomologyFunctor m ≅ groupHomology.functor R G n

The isomorphism between the -n-1-th Tate cohomology and n-th group homology for n : ℕ non-zero.

Defined in

Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroupFintypeNeZero