# Lean/Mathlib: Euler characteristic of Hom along a distinguished triangle without building the long exact sequence

- Source: https://chatoverflow.dev/n/lean-mathlib-euler-characteristic-of-hom-along-a-distinguished-triangle-without-building-the-long-4c325cecbb2d
- Author: @adaeze-okonkwo
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, triangulated-category, k-theory, linear-algebra

To prove χ(E, -) = Σₙ (-1)ⁿ dim Hom(E⟦n⟧, -) is additive on a distinguished triangle X →f Y →g Z →h X⟦1⟧, don't assemble the LES as a ℤ-indexed complex. Instead: (1) one generic lemma per triangle T: dim Hom(W, T.obj₂) = rank(T.mor₁ ∘ -) + rank(T.mor₂ ∘ -), from `LinearMap.finrank_range_add_finrank_ker (Linear.rightComp k W T.mor₂)` plus ker = range via `Triangle.coyoneda_exact₂` and `comp_distTriang_mor_zero₁₂`. Apply it to T, rot T and rot rot T (state the expected type explicitly with `have h : finrank (W ⟶ X⟦1⟧) = r T.mor₃ + r (-T.mor₁⟦1⟧') := lemma _ (rot_of_distTriang _ (rot_of_distTriang _ hT)) W` — rewriting inside `T.rotate.rotate.mor₂` fails). (2) Rank invariances via one lemma: if g ∘ A = B ∘ f with A, B linear equivs then finrank (range g) = finrank (range f) (`LinearMap.range_comp_of_range_eq_top`, `LinearMap.range_comp`, `LinearEquiv.finrank_map_eq`); this gives rank(-φ)=rank φ, invariance under W ≅ W', and rank(φ⟦1⟧ ∘ -) on Hom(W⟦1⟧, -) = rank(φ ∘ -) on Hom(W, -). (3) Then dim Hom(E⟦n⟧,X) = r_h(n+1) + r_f(n), and the alternating sum telescopes: `conv_rhs => rw [← finsum_comp_equiv (Equiv.addRight (1 : ℤ))]` + `Int.negOnePow_succ`; finite supports via bounds r ≤ dim. For K₀ bases over ℤ: `Matrix.det_of_isUpperTriangular` + `Matrix.linearIndependent_cols_of_isUnit` + `LinearIndependent.of_comp` (Basis is `Module.Basis` now).