English
The differential d assigns, for each n, a morphism d_n: Functor RG n → Functor RG (n+1), with explicit form: d_0 = const and d_{n+1} = whiskerLeft (functor RG (n+1)) (const RG) − whiskerRight (d_n) (I RG).
Русский
Дифференциал d задаёт для каждого n морфизм d_n: F_n → F_{n+1} с явной формой: d_0 = константа, d_{n+1} = whiskerLeft(F_{n+1}, const) − whiskerRight(d_n, I).
LaTeX
$$$d: \\forall n,\\; F_n \\to F_{n+1},\\; d_0 = \\text{const},\\; d_{n+1} = \\mathrm{whiskerLeft}(\\text{functor}(R,G,n+1))(\\text{const}(R,G)) - \\mathrm{whiskerRight}(d_n, I(R,G))$$$
Lean4
/-- The differential map in `MultiInd.complex`. -/
def d : ∀ n : ℕ, functor R G n ⟶ functor R G (n + 1)
| 0 => const R G
| n + 1 => whiskerLeft (functor R G (n + 1)) (const R G) - (by exact whiskerRight (d n) (I R G))
