Alternating sum of front-moves is (n+1)·f

Open

ContWeatherall.alternating_sum_cons_removeNth

by Alien60 · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

category-theorydifferential-formsgauge-theoryphilosophy-of-physicspoincare-lemma

For an alternating map $f$ of $n+1$ arguments over a commutative ring and any $v$ , $\sum_{i=0}^n(-1)^i f(v_i,v_0,\dots,\widehat{v_i},\dots,v_n)=(n+1)f(v)$ .

Preamble

import Mathlib
import Definitions.Def_ContWeatherall_defs

open CategoryTheory ContinuousAlternatingMap
open scoped ContDiff

Formal statement

namespace ContWeatherall

/-- Moving the `i`-th vector of `v` to the front with sign `(-1)^i` and summing over `i`
multiplies an alternating map of `n + 1` arguments by `n + 1`. -/
theorem alternating_sum_cons_removeNth {R M N : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→ₗ[R] N) (v : Fin (n + 1) → M) :
    ∑ i : Fin (n + 1), (-1 : ℤ) ^ (i : ℕ) • f (Fin.cons (v i) (i.removeNth v)) = (n + 1) • f v := by
  sorry

end ContWeatherall

Source

M. Spivak, Calculus on Manifolds (W. A. Benjamin, 1965), Theorem 4-11 (Poincaré lemma) and its proof (sign bookkeeping in the computation of d(Iω))

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $R$ be a commutative ring, $M,N$ be $R$ -modules, $n\in\mathbb{N}$ , $f$ an alternating $R$ -multilinear map $M^{n+1}\to N$ (purely algebraic), and $v=(v_0,\dots,v_n)\in M^{n+1}$ . Then

\sum_{i=0}^{n}(-1)^i\, f\big(v_i,v_0,\dots,\widehat{v_i},\dots,v_n\big)=(n+1)\,f(v_0,\dots,v_n),

where $(-1)^i$ is an integer acting by integer scalar multiplication on $N$ , the right side is the natural-number multiple $(n+1)\cdot f(v)$ in $N$ , and $\widehat{v_i}$ means the $i$ -th entry is removed with the others kept in order.

View graph