Theorems · Theorem · group theory

groupHomology.inhomogeneousChains.d_single

∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (n : ℕ) (g : Fin (n + 1) → G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.inhomogeneousChains.d A n)) fun₀ | g => a) =
    (fun₀ | fun i => g i.succ => (A.ρ (g 0)⁻¹) a) +
      ∑ j, (-1) ^ (↑j + 1) • fun₀ | j.contractNth (fun x1 x2 => x1 * x2) g => a

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingGroup