English
The MultiInd.complex is the cochain complex in the functor category with objects F_n and differentials d_n, i.e. a cochain complex in Functor RG.
Русский
MultiInd.complex - когомологическое комплекс в категориe функторов с объектами F_n и дифференциалами d_n.
LaTeX
$$$\\text{MultiInd.complex} : \\text{CoChainComplex} (\\mathrm{Action}(\\mathrm{TopModuleCat}\\,R)\\ G \\;⥤\\; \\mathrm{Action}(\\mathrm{TopModuleCat}\\,R)\\ G)\\ \\mathrm{Nat}$$$
Lean4
/-- The complex of functors whose behaviour pointwise takes an `R`-linear `G`-representation `M`
to the complex `M → C(G, M) → ⋯ → C(G, C(G,...,C(G, M))) → ⋯`
The `G`-invariant submodules of it is the homogeneous cochains (shifted by one). -/
def complex : CochainComplex (Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G) ℕ :=
CochainComplex.of (functor R G) (d R G) (d_comp_d R G)
