English
There is a canonical isomorphism of chain complexes between the inhomogeneous cochains and the Hom functor from the bar resolution, i.e. inhomogeneousCochains(A) ≅ (barComplex k G).linearYonedaObj k A.
Русский
Существует канонический изоморфизм комплексoв между неоднородными коцепами и Hom-функцией, связанной с bar-разложением: inhomogeneousCochains(A) ≅ (barComplex k G).linearYonedaObj k A.
LaTeX
$$$$ \\text{inhomogeneousCochains}(A) \\cong (\\bar{Complex}\\ kG).\\text{linearYonedaObj } kA. $$$$
Lean4
/-- Given a `k`-linear `G`-representation `A`, the complex of inhomogeneous cochains is isomorphic
to `Hom(P, A)`, where `P` is the bar resolution of `k` as a trivial `G`-representation. -/
def inhomogeneousCochainsIso [DecidableEq G] : inhomogeneousCochains A ≅ (barComplex k G).linearYonedaObj k A :=
by
refine HomologicalComplex.Hom.isoOfComponents (fun i => (Rep.freeLiftLEquiv (Fin i → G) A).toModuleIso.symm) ?_
rintro i j (h : i + 1 = j)
subst h
simp [d_eq, -LinearEquiv.toModuleIso_hom, -LinearEquiv.toModuleIso_inv]
