Theorems · Theorem · group theory

groupHomology.map_chainsFunctor_eval_shortExact

∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)},
  X.ShortExact →
    ∀ (n : ℕ),
      (X.map
          ((groupHomology.chainsFunctor k G).comp
            (HomologicalComplex.eval (ModuleCat k) (ComplexShape.down ℕ) n))).ShortExact

S.map (chainsFunctor k G) is short exact in each degree.

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingGroup