Theorems · Theorem · group theory

Rep.barComplex.d_single

∀ {k G : Type u} [inst : CommRing k] (n : ℕ) [inst_1 : Group G] (x : Fin (n + 1) → G),
  ((Rep.Hom.hom (Rep.barComplex.d k G n)) fun₀ | x => MonoidAlgebra.single 1 1) =
    (fun₀ | fun i => x i.succ => MonoidAlgebra.single (x 0) 1) +
      ∑ j, fun₀ | j.contractNth (fun x1 x2 => x1 * x2) x => MonoidAlgebra.single 1 ((-1) ^ (↑j + 1))

Defined in

Mathlib.RepresentationTheory.Homological.Resolution

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingGroup