Theorems · Theorem · group theory

groupHomology.iCycles_mk

∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {m n : ℕ}
  (h : (ComplexShape.down ℕ).next m = n) (f : (Fin m → G) →₀ ↑A)
  (hf : (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains A).d m n)) f = 0),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.iCycles A m)) (groupHomology.cyclesMk m n h f hf) = f

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingGroup