Theorems · Definition · group theory

Rep.barComplex.isoStandardComplex

(k G : Type u) → [inst : CommRing k] → [inst_1 : Group G] → Rep.barComplex k G ≅ Rep.standardComplex k G

Isomorphism between the bar resolution and standard resolution, with nth map (Gⁿ →₀ k[G]) → k[Gⁿ⁺¹] sending (g₁, ..., gₙ) ↦ (1, g₁, g₁g₂, ..., g₁...gₙ).

Defined in

Mathlib.RepresentationTheory.Homological.Resolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroup