English
There is a natural isomorphism of complexes between the coinvariants of A tensored with the restricted projective resolution and the coinvariants of Ind_S^G(A) tensored with P.
Русский
Существует естественный изоморфизм резолюций комплексoв между коинвариантами A ⊗ Res_S(P) и Ind_S^G(A) ⊗ P.
LaTeX
$$$\\text{coinvariantsTensorObj } A\\big( (Action.res\\; S.subtype).mapProjectiveResolution P\\big) \\cong \\; P^{\\text{coinvariantsTensorObj}} (\\mathrm{Ind}_S^G(A))$.$$
Lean4
/-- Simpler expression for the differential in the standard resolution of `k` as a
`G`-representation. It sends `(g₀, ..., gₙ₊₁) ↦ ∑ (-1)ⁱ • (g₀, ..., ĝᵢ, ..., gₙ₊₁)`. -/
theorem d_eq (n : ℕ) : ((standardComplex k G).d (n + 1) n).hom = ModuleCat.ofHom (d k G (n + 1)) :=
by
refine ModuleCat.hom_ext <| Finsupp.lhom_ext' fun (x : Fin (n + 2) → G) => LinearMap.ext_ring ?_
simp [Action.ofMulAction_V, standardComplex, SimplicialObject.δ, ← Int.cast_smul_eq_zsmul k ((-1) ^ _ : ℤ),
SimplexCategory.δ, Fin.succAboveOrderEmb]
