English
Let k be a commutative ring, G a group, and A a k-linear G-representation. The inhomogeneous cochain complex of A is the natural complex whose nth term is the set of all functions from G^n to A, i.e. C^n(G,A) = Maps(G^n, A), and whose differentials are the standard coboundary maps; this complex computes the group cohomology H^*(G,A).
Русский
Пусть k — коммутативное кольцо, G — группа, A — k-линейное представление G. Неоднородная коцепная комплексность A — это естественный комплекс, где n-й член равен функции от G^n в A, то есть C^n(G,A) = Maps(G^n,A), и дифференциалы — стандартные кобоконические отображения; этот комплекс вычисляет когомологию группы H^*(G,A).
LaTeX
$$$$ 0 \\to C^0(G,A) \\to C^1(G,A) \\to C^2(G,A) \\to \\cdots, \\quad C^n(G,A) = \\operatorname{Maps}(G^n, A). $$$$
Lean4
/-- Given a `k`-linear `G`-representation `A`, this is the complex of inhomogeneous cochains
$$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$
which calculates the group cohomology of `A`. -/
noncomputable abbrev inhomogeneousCochains : CochainComplex (ModuleCat k) ℕ :=
CochainComplex.of (fun n => ModuleCat.of k ((Fin n → G) → A)) (fun n => inhomogeneousCochains.d A n) fun n => by
classical
simp only [d_eq]
slice_lhs 3 4 => {rw [Iso.hom_inv_id]}
slice_lhs 2 4 => {rw [Category.id_comp, ((barComplex k G).linearYonedaObj k A).d_comp_d]}
simp
