The Euler characteristic is additive along a long exact sequence

Mathlib's GradedObject.eulerChar c X = ∑ᶠ i, c.χ i * finrank R (X i) is the Euler characteristic of a graded object, with the signs supplied by ComplexShape.EulerCharSigns; for ComplexShape.up ℤ the sign at i is (-1)^i. This file adds the arithmetic underneath "χ is additive on distinguished triangles": for three ℤ-graded families of finite-dimensional vector spaces assembled into a long exact sequence

… → A i → B i → C i → A (i+1) → …

the Euler characteristics satisfy χ B = χ A + χ C (GradedObject.eulerChar_eq_add_of_exact). The families are unbundled, with linear maps between them, because that is how a homology sequence of a linear functor presents them; the graded objects are fun i => ModuleCat.of k (A i).

Indices are ℤ, and there are no boundary hypotheses

This file deliberately does not reindex to ℕ, and the reason is worth stating.

Mathlib's Module.sum_neg_one_pow_finrank_eq_zero_of_exact handles a single exact sequence and is finitely indexed. A transport objection is sometimes raised against ℤ — that over ℤ the exactness hypothesis reads ker (d i) = range (d (i-1)), whose right-hand side lives in V (i-1+1) rather than V i. That objection does not apply here: spelled ker (d (i+1)) = range (d i) the indices agree on the nose, and (· + 1) is surjective on ℤ, so no transport arises. A finitely indexed alternating sum is proved by induction, and an induction needs a base case.

The ℤ-indexed three-family statement below needs no induction. It telescopes by a translation of the summation index — one finsum_comp_equiv along Equiv.addRight 1 — and consequently carries no injectivity at the bottom, no surjectivity at the top, and no Subsingleton at either end. The bounded ℕ-indexed companion, which pays injectivity at the bottom and [Subsingleton (A (n+1))] at the top, is Module.sum_neg_one_pow_finrank_eq_zero_of_longExact in Algebra/Exact/Sequence.lean. Both statements are geometry-free linear algebra; geometric Euler-characteristic additivity consumes the bounded one after constructing the relevant long exact sequence.

Finiteness enters as finiteness of the support of each dimension function rather than as a vanishing bound. Given Module.Finite, over a division ring the two are equivalent — finrank = 0 ↔ Subsingleton, and a finite subset of ℤ is bounded — so this is a choice of spelling, not of strength. It is the form finsum_add_distrib consumes directly, which removes the max-of-three- bounds bookkeeping a common window forces.

k is a division ring

Not a field: commutativity is used nowhere. DivisionRing is exactly what LinearMap.finrank_range_add_finrank_ker asks for (it lives in a section DivisionRing in Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean), and it supplies the StrongRankCondition that LinearMap.finrank_range_le needs for the support bounds. Mathlib states Module.sum_neg_one_pow_finrank_eq_zero_of_exact at the same level.

What this file does not do

It says nothing about complexes, homology, ModuleCat, or triangulated categories. It is linear algebra; the categorical Euler form that motivated it is assembled elsewhere. It also proves no vanishing statement — the three-family balance is what a distinguished triangle gives, and Mathlib already has the vanishing form for a finite exact sequence.

theorem GradedObject.finrankSupport_eq_support_intCast {R : Type u_1} [Ring R] {ι : Type u_2} (X : CategoryTheory.GradedObject ι (ModuleCat R)) : finrankSupport X = Function.support fun (i : ι) => ↑(Module.finrank R ↑(X i))

finrankSupport is also the support of the integer-valued rank function.

theorem Module.support_finrank_range_subset {k : Type u} [DivisionRing k] {ι : Type u_1} {V W : ι → Type v} [(i : ι) → AddCommGroup (V i)] [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module k (V i)] [(i : ι) → Module k (W i)] [∀ (i : ι), Module.Finite k (V i)] (f : (i : ι) → V i →ₗ[k] W i) : (Function.support fun (i : ι) => ↑(finrank k ↥(f i).range)) ⊆ Function.support fun (i : ι) => ↑(finrank k (V i))

A range's dimension is bounded by the source's, so its support sits inside the source's. This is where StrongRankCondition, hence DivisionRing, is used, and it is the only place the support side conditions come from.

theorem GradedObject.eulerChar_eq_add_of_exact {k : Type u} [DivisionRing k] {A B C : ℤ → Type v} [(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)) (hfg : ∀ (i : ℤ), Function.Exact ⇑(f i) ⇑(g i)) (hgδ : ∀ (i : ℤ), Function.Exact ⇑(g i) ⇑(δ i)) (hδf : ∀ (i : ℤ), Function.Exact ⇑(δ i) ⇑(f (i + 1))) (hA : (Function.support fun (i : ℤ) => ↑(Module.finrank k (A i))).Finite) (hB : (Function.support fun (i : ℤ) => ↑(Module.finrank k (B i))).Finite) (hC : (Function.support fun (i : ℤ) => ↑(Module.finrank k (C i))).Finite) : (eulerChar (ComplexShape.up ℤ) fun (i : ℤ) => ModuleCat.of k (B i)) = (eulerChar (ComplexShape.up ℤ) fun (i : ℤ) => ModuleCat.of k (A i)) + eulerChar (ComplexShape.up ℤ) fun (i : ℤ) => ModuleCat.of k (C i)

The Euler characteristic is additive along a ℤ-indexed long exact sequence.

χ B = χ A + χ C for … → A i → B i → C i → A (i+1) → … exact everywhere, with the signs of ComplexShape.up ℤ. There is no injectivity hypothesis, no surjectivity hypothesis, and no vanishing at either end: over ℤ the telescoping is a translation of the summation index rather than an induction, so there are no boundary cases to state. Finiteness enters as finiteness of the support of the integer-valued rank function, the form a homology sequence of a linear functor supplies; finrankSupport_eq_support_intCast relates it to finrankSupport.