Theorems · Definition · group theory

Rep.barComplex

(k G : Type u) → [inst : CommRing k] → [inst_1 : Group G] → ChainComplex (Rep.{u, u, u} k G) ℕ

The projective resolution of k as a trivial k-linear G-representation with nth differential (Gⁿ⁺¹ →₀ k[G]) → (Gⁿ →₀ k[G]) sending (g₀, ..., gₙ) to g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁) for j = 0, ..., n - 1.

Defined in

Mathlib.RepresentationTheory.Homological.Resolution

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingGroup