inhomogeneousCochains.d_eq

theorem inhomogeneousCochains.d_eq : ∀ {k G : Type u} [inst : CommRing k] (n : ℕ) [inst_1 : Group G] (A : Rep k G), inhomogeneousCochains.d n A = CategoryTheory.CategoryStruct.comp (Rep.diagonalHomEquiv n A).toModuleIso.inv (CategoryTheory.CategoryStruct.comp ((groupCohomology.linearYonedaObjResolution A).d n (n + 1)) (Rep.diagonalHomEquiv (n + 1) A).toModuleIso.hom)

This theorem states that for any commutative ring `k`, a group `G`, a natural number `n`, and a `k`-linear representation of `G` denoted by `A`, the differential (`inhomogeneousCochains.d`) in the complex of inhomogeneous cochains is equal to the composition of certain morphisms. More specifically, it is equivalent to the composition of the inverse of the isomorphism `Rep.diagonalHomEquiv n A` (which maps functions from `Gⁿ` to `A` to homomorphisms from `k[Gⁿ⁺¹]` to `A`), the differential of the complex `groupCohomology.linearYonedaObjResolution A` at `n` and `n+1`, and the homomorphism `Rep.diagonalHomEquiv (n + 1) A`. This asserts that the said isomorphism commutes with the differentials in both the complex of inhomogeneous cochains and the homogeneous `linearYonedaObjResolution`, where the latter is the standard resolution of `k` as a trivial `k`-linear `G`-representation.

More concisely: The differential in the complex of inhomogeneous cochains of a commutative ring `k`, a group `G`, and a `k`-linear representation `A`, is equal to the composition of the inverse of `Rep.diagonalHomEquiv n A`, the differential of `groupCohomology.linearYonedaObjResolution A` at `n` and `n+1`, and `Rep.diagonalHomEquiv (n + 1) A`.