Alternating finite dimensions along a bounded long exact sequence

Mathlib's Module.sum_neg_one_pow_finrank_eq_zero_of_exact says that the alternating sum of dimensions along a finite exact sequence vanishes. The long exact sequence attached to a short exact sequence of complexes has the zig-zag shape

0 → A 0 → B 0 → C 0 → A 1 → B 1 → C 1 → ⋯ → C n → A (n + 1) = 0,

and this file states that theorem in that shape: the alternating sum of dim A i - dim B i + dim C i over i ≤ n vanishes. Injectivity of f 0 is the left end; the right end is stated as vanishing of A (n + 1), which makes the last connecting map surjective onto zero. Geometric Euler-characteristic additivity consumes it after constructing the long exact sequence of coherent cohomology.

The ℤ-indexed, boundary-free form is GradedObject.eulerChar_eq_add_of_exact in Algebra/Homology/EulerCharacteristic.lean.

theorem Module.sum_neg_one_pow_finrank_eq_zero_of_longExact {k : Type u_1} [DivisionRing k] (A : ℕ → Type u_2) (B : ℕ → Type u_3) (C : ℕ → Type u_4) [(i : ℕ) → AddCommGroup (A i)] [(i : ℕ) → AddCommGroup (B i)] [(i : ℕ) → AddCommGroup (C i)] [(i : ℕ) → Module k (A i)] [(i : ℕ) → Module k (B i)] [(i : ℕ) → Module k (C i)] [∀ (i : ℕ), Module.Finite k (A i)] [∀ (i : ℕ), Module.Finite k (B i)] [∀ (i : ℕ), Module.Finite k (C i)] (f : (i : ℕ) → A i →ₗ[k] B i) (g : (i : ℕ) → B i →ₗ[k] C i) (δ : (i : ℕ) → C i →ₗ[k] A (i + 1)) (hinj : Function.Injective ⇑(f 0)) (hexact₂ : ∀ (i : ℕ), Function.Exact ⇑(f i) ⇑(g i)) (hexact₃ : ∀ (i : ℕ), Function.Exact ⇑(g i) ⇑(δ i)) (hexact₁ : ∀ (i : ℕ), Function.Exact ⇑(δ i) ⇑(f (i + 1))) (n : ℕ) [Subsingleton (A (n + 1))] : ∑ i ∈ Finset.range (n + 1), (-1) ^ i * (↑(finrank k (A i)) - ↑(finrank k (B i)) + ↑(finrank k (C i))) = 0

Alternating dimensions cancel along a bounded long exact sequence of the zig-zag shape A i → B i → C i → A (i + 1): the form of Module.sum_neg_one_pow_finrank_eq_zero_of_exact attached to a short exact sequence of complexes. The endpoint hypothesis is stated as vanishing of the next A term, which makes the final connecting map surjective onto zero.