Theorems · Definition · group theory

Rep.barResolution.extIso

(k G : Type u) →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (V : Rep.{u, u, u} k G) →
        (n : ℕ) →
          ((Ext k (Rep.{u, u, u} k G) n).obj (Opposite.op (Rep.trivial k G k))).obj V ≅
            HomologicalComplex.homology ((Rep.barComplex k G).linearYonedaObj k V) n

Given a k-linear G-representation V, Extⁿ(k, V) (where k is the trivial k-linear G-representation) is isomorphic to the nth cohomology group of Hom(P, V), where P is the bar resolution of k.

Defined in

Mathlib.RepresentationTheory.Homological.Resolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroup