English
The differential d in the inhomogeneous cochains equals the conjugation of barComplex differential by the fixed isomorphisms freeLiftLEquiv and toModuleIso, i.e., d equals the conjugated differential.
Русский
Дифференциал d в несобирательных косинфках равен сопряжению дифференциала barComplex фиксированными изоморфизмами freeLiftLEquiv и toModuleIso; то есть d есть сопряжённый дифференциал.
LaTeX
$$$ d_A(n) = (\mathrm{freeLiftLEquiv}_{(Fin\ n\to G)} A)^{-1} \; \circ \; ((\mathrm{barComplex}\ k\ G).linearYonedaObj\ k A).d\; n\,(n+1) \; \circ \; (\mathrm{freeLiftLEquiv}_{(Fin\ (n+1) \to G)} A).toModuleIso.hom $$$
Lean4
/-- The differential in the complex of inhomogeneous cochains used to
calculate group cohomology. -/
@[simps! -isSimp]
def d [Monoid G] (A : Rep k G) (n : ℕ) : ModuleCat.of k ((Fin n → G) → A) ⟶ ModuleCat.of k ((Fin (n + 1) → G) → A) :=
ModuleCat.ofHom
{ toFun f
g :=
A.ρ (g 0) (f fun i => g i.succ) +
Finset.univ.sum fun j : Fin (n + 1) => (-1 : k) ^ ((j : ℕ) + 1) • f (Fin.contractNth j (· * ·) g)
map_add' f
g := by
ext
simp [Finset.sum_add_distrib, add_add_add_comm]
map_smul' r
f := by
ext
simp [Finset.smul_sum, ← smul_assoc, mul_comm r] }
