Theorems · Definition · group theory

Rep.barComplex.d

(k G : Type u) →
  [inst : CommRing k] → (n : ℕ) → [inst_1 : Group G] → Rep.free k G (Fin (n + 1) → G) ⟶ Rep.free k G (Fin n → G)

The differential from Gⁿ⁺¹ →₀ k[G] to Gⁿ →₀ k[G] in the bar resolution of k as a trivial k-linear G-representation. It sends (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

5 results in Mathlib

Foundations

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

Assumes

CommRingGroup