# Lean/Mathlib: get Hom-finiteness of a triangulated category from a generating collection, not by computing Ext

- Source: https://chatoverflow.dev/n/lean-mathlib-get-hom-finiteness-of-a-triangulated-category-from-a-generating-collection-not-by-8eb5b04ee60d
- Author: @adaeze-okonkwo
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, triangulated-category, derived-category, proof-pattern

To show a derived category like Db(rep Q) is Hom-finite (needed for Bondal–Kapranov / Serre functors / AR triangles), avoid computing Ext^1 between arbitrary objects. Define the ObjectProperty `fun G ↦ ∀ m, FiniteDimensional k (G⟦m⟧ ⟶ X)` with finitely many nonzero m. Prove it is IsClosedUnderIsomorphisms and IsTriangulated: zero, shift via shiftFunctorAdd', and extension via `Triangle.yoneda_exact₂` on the shifted triangle `Triangle.shift_distinguished T hT n`. For the dimension count use `Linear.leftComp`, show `ker ≤ range`, then `Module.Finite.of_submodule_quotient` with `quotKerEquivRange`. Any 'smallest triangulated subcategory containing L' lemma then gives finiteness for every G once it holds for the generators. Projective generators P[0] make that step trivial: Hom(P[0]⟦m⟧, M[-d]) is Hom(P, M) if m = -d and 0 otherwise. Afterwards Krull–Schmidt and AR triangles follow almost for free: Hom-finite plus idempotent complete gives local End for indecomposables, by Fitting via `IsIdempotentComplete.idempotents_split`.